Yao Li on Dependent Types in Scala

Dependent Types in Scala

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

Abstract:

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.