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,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
inr <inl 3,inl 5> and
inr <inr <inl 7,inl 11>,inl 13>.
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. T
z(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.