10.2.1 Dependent Types
We'll now look at types not readily formalised in some of the Hindley-Milner languages.
In mainstream functional languages, terms to the left of : and types to the right of :
are disjoint. In dependent types, types either incorporate terms or terms types. Here's
an example; I want a dependently typed function myprog that takes a type as an input and
enforces that type on the input. myprog does nothing special in this example; it simply
returns the input.
P : Type;
(myprog Type P) : Type;)
Type P -> P)
(myprover symbol p)
p : symbol
(myprog number p)