See Recursive Types for supplementary material.
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>.
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
tis of type
rec(z. int | z#z)then the following term computes the sum of the values at
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.