113

There are path dependent types and I think it is possible to express almost all the features of such languages as Epigram or Agda in Scala, but I'm wondering why Scala does not support this more explicitly like it does very nicely in other areas (say, DSLs) ? Anything I'm missing like "it is not necessary" ?

3

4 Answers 4

159

Syntactic convenience aside, the combination of singleton types, path-dependent types and implicit values means that Scala has surprisingly good support for dependent typing, as I've tried to demonstrate in shapeless.

Scala's intrinsic support for dependent types is via path-dependent types. These allow a type to depend on a selector path through an object- (ie. value-) graph like so,

scala> class Foo { class Bar }
defined class Foo

scala> val foo1 = new Foo
foo1: Foo = Foo@24bc0658

scala> val foo2 = new Foo
foo2: Foo = Foo@6f7f757

scala> implicitly[foo1.Bar =:= foo1.Bar] // OK: equal types
res0: =:=[foo1.Bar,foo1.Bar] = <function1>

scala> implicitly[foo1.Bar =:= foo2.Bar] // Not OK: unequal types
<console>:11: error: Cannot prove that foo1.Bar =:= foo2.Bar.
              implicitly[foo1.Bar =:= foo2.Bar]

In my view, the above should be enough to answer the question "Is Scala a dependently typed language?" in the positive: it's clear that here we have types which are distinguished by the values which are their prefixes.

However, it's often objected that Scala isn't a "fully" dependently type language because it doesn't have dependent sum and product types as found in Agda or Coq or Idris as intrinsics. I think this reflects a fixation on form over fundamentals to some extent, nevertheless, I'll try and show that Scala is a lot closer to these other languages than is typically acknowledged.

Despite the terminology, dependent sum types (also known as Sigma types) are simply a pair of values where the type of the second value is dependent on the first value. This is directly representable in Scala,

scala> trait Sigma {
     |   val foo: Foo
     |   val bar: foo.Bar
     | }
defined trait Sigma

scala> val sigma = new Sigma {
     |   val foo = foo1
     |   val bar = new foo.Bar
     | }
sigma: java.lang.Object with Sigma{val bar: this.foo.Bar} = $anon$1@e3fabd8

and in fact, this is a crucial part of the encoding of dependent method types which is needed to escape from the 'Bakery of Doom' in Scala prior to 2.10 (or earlier via the experimental -Ydependent-method types Scala compiler option).

Dependent product types (aka Pi types) are essentially functions from values to types. They are key to the representation of statically sized vectors and the other poster children for dependently typed programming languages. We can encode Pi types in Scala using a combination of path dependent types, singleton types and implicit parameters. First we define a trait which is going to represent a function from a value of type T to a type U,

scala> trait Pi[T] { type U }
defined trait Pi

We can than define a polymorphic method which uses this type,

scala> def depList[T](t: T)(implicit pi: Pi[T]): List[pi.U] = Nil
depList: [T](t: T)(implicit pi: Pi[T])List[pi.U]

(note the use of the path-dependent type pi.U in the result type List[pi.U]). Given a value of type T, this function will return a(n empty) list of values of the type corresponding to that particular T value.

Now let's define some suitable values and implicit witnesses for the functional relationships we want to hold,

scala> object Foo
defined module Foo

scala> object Bar
defined module Bar

scala> implicit val fooInt = new Pi[Foo.type] { type U = Int }
fooInt: java.lang.Object with Pi[Foo.type]{type U = Int} = $anon$1@60681a11

scala> implicit val barString = new Pi[Bar.type] { type U = String }
barString: java.lang.Object with Pi[Bar.type]{type U = String} = $anon$1@187602ae

And now here is our Pi-type-using function in action,

scala> depList(Foo)
res2: List[fooInt.U] = List()

scala> depList(Bar)
res3: List[barString.U] = List()

scala> implicitly[res2.type <:< List[Int]]
res4: <:<[res2.type,List[Int]] = <function1>

scala> implicitly[res2.type <:< List[String]]
<console>:19: error: Cannot prove that res2.type <:< List[String].
              implicitly[res2.type <:< List[String]]
                    ^

scala> implicitly[res3.type <:< List[String]]
res6: <:<[res3.type,List[String]] = <function1>

scala> implicitly[res3.type <:< List[Int]]
<console>:19: error: Cannot prove that res3.type <:< List[Int].
              implicitly[res3.type <:< List[Int]]

(note that here we use Scala's <:< subtype-witnessing operator rather than =:= because res2.type and res3.type are singleton types and hence more precise than the types we are verifying on the RHS).

In practice, however, in Scala we wouldn't start by encoding Sigma and Pi types and then proceeding from there as we would in Agda or Idris. Instead we would use path-dependent types, singleton types and implicits directly. You can find numerous examples of how this plays out in shapeless: sized types, extensible records, comprehensive HLists, scrap your boilerplate, generic Zippers etc. etc.

The only remaining objection I can see is that in the above encoding of Pi types we require the singleton types of the depended-on values to be expressible. Unfortunately in Scala this is only possible for values of reference types and not for values of non-reference types (esp. eg. Int). This is a shame, but not an intrinsic difficulty: Scala's type checker represents the singleton types of non-reference values internally, and there have been a couple of experiments in making them directly expressible. In practice we can work around the problem with a fairly standard type-level encoding of the natural numbers.

In any case, I don't think this slight domain restriction can be used as an objection to Scala's status as a dependently typed language. If it is, then the same could be said for Dependent ML (which only allows dependencies on natural number values) which would be a bizarre conclusion.

14
  • 8
    Miles, thanks for this very detailed answer. I'm a bit curious about one thing, though. None of your examples seem at first glance particularly impossible to express in Haskell; are you then claiming that Haskell is also a dependently-typed language? Oct 21, 2012 at 18:26
  • 8
    I downvoted because I can't distinguish the techniques here in essence from the techniques described in McBride's "Faking It" citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.22.2636 -- i.e. these are ways to simulate dependent types, not provide them directly.
    – sclv
    Oct 22, 2012 at 0:12
  • 3
    @sclv I think you've missed that Scala has dependent types without any form of encoding: see the first example above. You're quite right that my encoding of Pi types uses some of the same techniques as Connor's paper, but from a substrate that already includes path-dependent types and singleton types. Oct 22, 2012 at 7:37
  • 4
    Nope. Sure you can have types tied to objects (this is a consequence of objects as modules). But you can't have computation on these types without using value-level witnesses. In fact =:= itself is a value-level witness! You're still faking it, just like you have to in Haskell, or perhaps more so.
    – sclv
    Oct 22, 2012 at 14:52
  • 9
    Scala's =:= isn't value-level, it's a type constructor - a value for that is here: github.com/scala/scala/blob/v2.10.3/src/library/scala/…, and doesn't seem particularly different than a witness for an equality proposition in dependently-typed languages like Agda and Idris: refl. (See www2.tcs.ifi.lmu.de/~abel/Equality.pdf section 2, and eb.host.cs.st-andrews.ac.uk/writings/idris-tutorial.pdf section 8.1, respectively.)
    – pdxleif
    Nov 14, 2013 at 9:30
6

I would assume it is because (as I know from experience, having used dependent types in the Coq proof assistant, which fully supports them but still not in a very convenient way) dependent types are a very advanced programming language feature which is really hard to get right - and can cause an exponential blowup in complexity in practice. They're still a topic of computer science research.

2
  • would you be kind enough to give me some theoretical background to dependant types (a link perhaps) ? Oct 18, 2012 at 11:31
  • 3
    @ashy_32bit if you can get access to "Advanced Topics in Types and Programming Languages" by Benjamin Pierce, there is a chapter in that which gives a reasonable introduction to dependent types. You could also read some papers by Conor McBride who has a particular interest in dependent types in practice rather than in theory.
    – iainmcgin
    Oct 18, 2012 at 12:09
3

I believe that Scala's path-dependent types can only represent Σ-types, but not Π-types. This:

trait Pi[T] { type U }

is not exactly a Π-type. By definition, Π-type, or dependent product, is a function which result type depends on argument value, representing universal quantifier, i.e. ∀x: A, B(x). In the case above, however, it depends only on type T, but not on some value of this type. Pi trait itself is a Σ-type, an existential quantifier, i.e. ∃x: A, B(x). Object's self-reference in this case is acting as quantified variable. When passed in as implicit parameter, however, it reduces to an ordinary type function, since it is resolved type-wise. Encoding for dependent product in Scala may look like the following:

trait Sigma[T] {
  val x: T
  type U //can depend on x
}

// (t: T) => (∃ mapping(x, U), x == t) => (u: U); sadly, refinement won't compile
def pi[T](t: T)(implicit mapping: Sigma[T] { val x = t }): mapping.U 

The missing piece here is an ability to statically constraint field x to expected value t, effectively forming an equation representing the property of all values inhabiting type T. Together with our Σ-types, used to express the existence of object with given property, the logic is formed, in which our equation is a theorem to be proven.

On a side note, in real case theorem may be highly nontrivial, up to the point where it cannot be automatically derived from code or solved without significant amount of effort. One can even formulate Riemann Hypothesis this way, only to find the signature impossible to implement without actually proving it, looping forever or throwing an exception.

4
  • 1
    Miles Sabin has above shown an example of using Pi to create types depending on values. Oct 2, 2017 at 0:42
  • In the example, depList extracts type U from the Pi[T], selected for type (not value) of t. This type just happens to be singleton type, currently available on Scala singleton objects and representing their exact values. Example creates one implementation of Pi per singleton object type, thus pairing type with value as in Σ-type. Π-type, on the other hand, is a formula that matches over the structure of its input parameter. Possibly, Scala don't have them because Π-types require every parameter type to be GADT, and Scala don't distinguish GADTs from other types.
    – P. Frolov
    Oct 3, 2017 at 8:55
  • Okay, I am a bit confused. Wouldn't pi.U in Miles' example count as dependent type? It's on the value pi. Oct 3, 2017 at 18:57
  • 2
    It indeed counts as dependent type, but there's different flavors of those: Σ-type ("there exists x such that P(x)", logic-wise) and Π-type ("for all x, P(x)"). As you noted, type pi.U is dependent on value of pi. Problem that preventing trait Pi[T] from becoming a Π-type is that we can't make it dependent on value of an arbitrary argument (for example, t in depList) without lifting that argument at type level.
    – P. Frolov
    Oct 4, 2017 at 18:57
1

The question was about using dependently typed feature more directly and, in my opinion, there would be a benefit in having a more direct dependent typing approach than what Scala offers.
Current answers try to argue the question on type theoretical level. I want to put a more pragmatic spin on it. This may explain why people are divided on the level of support of dependent types in the Scala language. We may have somewhat different definitions in mind. (not to say one is right and one is wrong).

This is not an attempt to answer the question how easy would it be to turn Scala into something like Idris (I imagine very hard) or to write a library offering more direct support for Idris like capabilities (like singletons tries to be in Haskell).

Instead, I want to emphasize the pragmatic difference between Scala and a language like Idris.
What are code bits for value and type level expressions? Idris uses the same code, Scala uses very different code.

Scala (similarly to Haskell) may be able to encode lots of type level calculations. This is shown by libraries like shapeless. These libraries do it using some really impressive and clever tricks. However, their type level code is (currently) quite different from value level expressions (I find that gap to be somewhat closer in Haskell). Idris allows to use value level expression on the type level AS IS.

The obvious benefit is code reuse (you do not need to code type level expressions separately from value level if you need them in both places). It should be way easier to write value level code. It should be easier to not have to deal with hacks like singletons (not to mention performance cost). You do not need to learn two things you learn one thing. On a pragmatic level, we end up needing fewer concepts. Type synonyms, type families, functions, ... how about just functions? In my opinion, this unifying benefits go much deeper and are more than syntactic convenience.

Consider verified code. See:
https://github.com/idris-lang/Idris-dev/blob/v1.3.0/libs/contrib/Interfaces/Verified.idr
Type checker verifies proofs of monadic/functor/applicative laws and the proofs are about actual implementations of monad/functor/applicative and not some encoded type level equivalent that may be the same or not the same. The big question is what are we proving?

The same can me done using clever encoding tricks (see the following for Haskell version, I have not seen one for Scala)
https://blog.jle.im/entry/verified-instances-in-haskell.html
https://github.com/rpeszek/IdrisTddNotes/wiki/Play_FunctorLaws
except the types are so complicated that it is hard to see the laws, the value level expressions are converted (automatically but still) to type level things and you need to trust that conversion as well. There is room for error in all of this which kinda defies the purpose of compiler acting as a proof assistant.

(EDITED 2018.8.10) Talking about proof assistance, here is another big difference between Idris and Scala. There is nothing in Scala (or Haskell) that can prevent from writing diverging proofs:

case class Void(underlying: Nothing) extends AnyVal //should be uninhabited
def impossible() : Void = impossible()

while Idris has total keyword preventing code like this from compiling.

A Scala library that tries to unify value and type level code (like Haskell singletons) would be an interesting test for Scala's support of dependent types. Can such library be done much better in Scala because of path-dependent types?

I am too new to Scala to answer that question myself.

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.