5. Types and Programs

Using the Curry-Howard-Isomorphism, we reuse proof terms to write programs and we introduce isomorphic constructs to propositions as the types of our programs: product `*', disjoint sum `+', function space `->', unit type `1' and empty type `0'. Note that there are no isomorphic constructs to negation and equivalence.

Furthermore we introduce the three inductive types `nat' (Natural numbers), `bool' (Booleans) and `list' (Polymorphic lists). The constructors and destructors are

0, s t

nat: Zero and successor

rec r of f 0 => s | f (s x) => t end

nat: Primitive recursion

true, false

bool: The two truth values

if r then s else t

bool: Case distinction

nil, s :: t

tau list: Empty list and cons.

rec r of f nil => s | f (x::xs) => t end

tau list: Primitive recursion

Note that `0' can both mean the number zero and the empty type. `1 + 1' may look like an arithmetical expression, but denotes a sum type here. Be careful not to mistake `1' for a number and to use it in your programs. Tutch will parse it as a type and give you a strange error message.

The two terms for primitive recursion define locally a function f and describe its behaviour for all possible cases of input by the step terms s and t. The use of f within the step terms s and t underlies strong syntactic restrictions that guarantee termination of the function on all inputs: In s no recursive calls are allowed at all. In t, for nat a recursive call can only look like f x (or f(x)), where x is the variable defined in the pattern matching f (s x) => .... For list, the recursive call must be f xs (or with parentheses as above).

Here is one example for primitive recursion over nat:

val double : nat -> nat = fn x => rec x of d 0 => 0 | d (s x') => s (s (d x')) end;

The keyword `val' indicates the definition of a program of a given type. Another example is subtraction on nat:

val minus : nat -> nat -> nat = fn x => rec x of m 0 => fn y => 0 | m (s x') => fn y => rec y of p 0 => s x' | p (s y') => m x' y' end end;

The types of the locally defined functions are m : nat -> (nat -> nat) and p : nat -> nat. To be able to apply two arguments to m we have used the trick to move the second lambda abstraction fn y => into the outer recursion. Thus m, applied to 0 or s x', returns a function from nat to nat, to which we can apply the second argument.

The inner recursion is just a case distinction, since p does not occur on a right hand side.

val rev : tau list -> tau list -> tau list = fn l => rec l of r nil => fn a => a | r (x::l') => fn a => r l' (x :: a) end; val reverse : tau list -> tau list = fn l => rev l nil;

This is an implementation of the reverse function by an auxiliary function with an accumulator argument. We use the same trick as for minus.

For more documentation look up the reference.