See Recursive Types for supplementary material.


next up previous contents index
Next: Expressiveness and Elegance Up: Recursive Definition Previous: Recursive Definition

Inductive Types

As an introduction to the rec types, consider the inductive type of integer trees, defined informally as

In the language of rec  types this type may be defined as

     rec(z. int | z#z).
Its elements include
inl 2,
inr <inl 3,inl 5> and
inr <inr <inl 7,inl 11>,inl 13>.
An inductive type may also be parameterized; generalizing the above definition of binary integer trees to general binary trees over a specified type, the example rephrased as

is denoted

     rec(z,x. x | z(x)#z(x); int),
and the predicate function dom,
asserting f has a root is denoted
     \x. rec(dom,x. int_eq(f(x); 0; true; dom(x+1)); x).
The elim form, rec_ind, is  analogous to the list_ind and integer ind forms. If t is of type rec(z. int | z#z) then the following term computes the sum of the values at t's leaves.
     rec_ind(t;  sum,x.
       decide(x;
         leaf. leaf;
         pair. spread(pair; left_son,right_son.
                 sum(left_son)+sum(right_son))))
The simpler rec(z.T) form is not formally part of the extension since it can be mimicked by rec(z,x. Tz(0)z;0), for example, so consider any rec(z.T) term in what follows to be just an abbreviation. Inductive types can also be defined in a mutually recursive fashion, but we will not pursue that possibility here.





Richard Eaton
Thu Sep 14 08:45:18 EDT 1995