Dependent Types

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

4. The Core Language

4.6 Sequences

5 Defining Functions

6. Packages

7. Shen-YACC

8. Shen Prolog

9. Types

10 Sequent Calculus

10.2 Exotic Types