See Recursive Types for supplementary material.

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