16 | Recursive Types |

Inductive and coinductive types, such as natural numbers and streams, may be seen as examples of *fixed points* of type operators *up to isomorphism.* An isomorphism between two types, *τ*_{1} and *τ*_{2}, is given by two expressions,

1. *x*_{1} : *τ*_{1} *e*_{2} : *τ*_{2}, and

2. *x*_{2} : *τ*_{2} *e*_{1} : *τ*_{1}

which are mutually inverse to each other.^{1} For example, the types nat and unit + nat are isomorphic, as witnessed by the following two expressions:

1. *x* : unit + nat case *x*{l · _ ⇒ z | r · *x*_{2} ⇒ s(*x*_{2})} : nat, and

2. *x* : nat ifz *x* {z ⇒ l · | s(*x*_{2}) ⇒ r · *x*_{2}} : unit ...

Start Free Trial

No credit card required