O'Reilly logo

Practical Foundations for Programming Languages by Robert Harper

Stay ahead with the world's most comprehensive technology and business learning platform.

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, tutorials, and more.

Start Free Trial

No credit card required

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. x1 : τ1 image e2 : τ2, and

2. x2 : τ2 image e1 : τ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 · x2 ⇒ s(x2)} : nat, and

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

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, interactive tutorials, and more.

Start Free Trial

No credit card required