Yao Li on Dependent Types in Scala


Dependent Types in Scala

Speaker: Yao Li, Ph.D. student from the University of Pennsylvania


Dependent types can help prevent bugs and guide programmers to construct correct implementations, by enabling using extremely expressive types as specifications.

For example, in a language with full dependent type support like Gallina, you can write something like this:
Fixpoint rep (A: Type) (n: nat) (a: A): Vector A n:=
match n with
| O => VNil A
| S n’ => VCons A n’ a (rep A n’ a) end.
where Vector A n is a vector of As and its length is n. The program would not type check if the function implementation returns a list whose length is not n and therefore rejects bogus implementations.

Unfortunately, the above example is typically not directly available in most mainstream programming languages including Scala because these languages usually enforce a phase separation between runtime values and compile-time values.

Nevertheless, I will show you in this talk that by using a trick called singleton types and features from Scala such as subtyping and path dependent types, we can encode the above example in Scala.