A resursive type has the form
where may appear free in type .
The resursive type is subject to the following introduction and elimination rules:
where denote the type with every free occurrence of substituted by .
Recursive types allows us to express "infinite" types such as .