Presented by Dave Herman
Transcribed by Dale Vaillancourt
In the 70's and 80's, Martin-Lšf pioneered a program in constructive type theory whose goal was to provide a unified foundation for constructive mathematics. In the 80's and 90's, Barendregt pursued the idea of pure type systems, and his goal was to unify type theory by demonstrating that various type systems are instances of the same general type theory parameterized over a few axioms. Dependent types are emphasized in both pieces of work.
To understand dependent types, we will look at some simple type systems and then generalize. The simply typed lambda calculus allows us to write expressions such as (\x:int.x+1) : int -> int. The lambda term is a value, and the (int -> int) is its type. When it comes to functions such as the identity, however, the simple type system forces us to type \x.x at a less general type than it deserves.
System F allows us to express polymorphic functions by permitting abstraction over the types of the bound variables. Working in the Church style, we must ascribe a type to every bound variable. If we say that a type is a member of some other type, however, we are left with an impredicative system. In order to avoid Girard's paradox (much like Russell's paradox in set theory), we employ stratification: objects in the value universe U_0 are members of a type in the type universe U_1, types are members of an object "*" in the kind universe U_2, kinds are members of an object in universe U_3, ad infinitum. (Care must be taken to avoid off-by-one type errors!)
Within this framework, the identity function is expressed as (/\a : *. \x : a. x) : (All a. a -> a). We note here that the use of "/\" is rather arbitrary. The abstraction mechanism that we use for types, kinds, and indeed all of the universes, is the very same one that we use in the value universe. So we simply write (\a : *.\x : a. x) : (All a. a -> a). Be aware that the polymorphism here actually introduces another level of stratification _within_ the type universe U_1! (All a. a -> a) is an element of *.
So far we have used abstraction to parameterize values over values and types and to parameterize types over types, but we can generalize a step further. We can parameterize types over values. This is the notion of a dependent type: it is a type which depends on a value. The canonical example is a list whose length is encoded in the type: [5,6,7] : int list(3). The dependent type "integer list of length n" is written "Pi n : Nat. int list(n)", and this term is itself an object of (Nat -> *).
A dependent type, interpreted as a proposition about a program, is simply an assertion about a value that is parameterized on another value. In this sense, dependent types let us make "more specific" assertions about values than do run-of-the-mill type systems (like Hindley-Milner). An interesting consequence is that type checking with dependent types is undecidable in general. When types depend on values, type checking involves comparison of arbitrary terms, and therefore termination cannot be guaranteed. A philosophical question can be then be posed: if the type checker does not terminate, what are the chances that your program is correct? If chances are slim, does the risk of nontermination matter, pragmatically speaking?
Now let's practice typing some useful functions. Functions such as reverse and append are more or less straighforward:
reverse : Pi n : Nat. int list(n) -> int list(n) append : Pi n : Nat. Pi m : Nat. int list(n) -> int list(m) -> int list (n + m)Pop quiz: Can you move the (Pi m : Nat) to the right of the first arrow? (Hint: Think Curry-Howard!)
Let's try filter:
filter : Pi m: Nat. (int -> bool) -> int list(m) -> int list (???)
Uh oh. We don't know, a priori, how long the resulting list will be!
Pop quiz 2: Why is the following type for filter nonsensical? filter : Pi m : Nat. Pi n : Nat. (int -> bool) -> int list(m) -> int list (n)
Let's use existential types to express the uncertainty of the length of the result list:
filter : Pi n : Nat. (int -> bool) -> int list(n) -> E m : Nat. int list (m) (NB: "E" is written as a capital sigma.)
Pop quiz 3: Does it make sense to write the following?
filter : Pi n : Nat. E m : Nat. (int -> bool) -> int list(n) -> int list(m)(Hint: Think back to Curry-Howard again.)
(Aside: In '85 Mitchell & Plotkin wrote "ADTs have existential type". Read this for more background on existential types.)
Cayenne, by Augustson: This is a language with the full power of dependent types. Of note is the ability to keep the type checking phase separated from the run time phase. This feature is enabled by the lack of a language construct that lets you branch based on the value of some type variable. Also of note is the fact that you cannot even trust the type checker's proofs.
Dependent ML by Hongwei Xi: This is a conservative extension of ML that introduces indices into the type language. Xi is able to perform optimizations such as bounds check elimination on array accesses as well as null check elimination when taking the cdr of lists.