10.2.1 Dependent Types
TBoS 261-262
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.
(0-) (datatype my-prover-types
P : Type;
_______________________
(myprog Type P) : Type;)
type#my-prover-types
(1-)(define myprog
Type P -> P)
(fn myprog)
(2-) (tc +)
true
(3+) (myprover symbol p)
p : symbol
(4+) (myprog number p)
type error
|
|
