Recursive types

Read TAPL 20.1-2.

Pierce presents recursive types and then describes two ways of formalizing them, equi-recursive types and iso-recursive types. Equi-recursive types are easier to program with, so he starts off with them; iso-recursive types are easier to implement.

You’ve used recursive types in OCaml. For example, if you wanted to define your own linked list type, you would do:

type int_list = Nil | Cons of int * int_list

In our extended λ-calculus, we can’t just write

NatList ≡ <nil:Unit, cons:Nat×NatList>

because you can’t define something in terms of itself. So we introduce some new notation,

NatList ≡ μX. <nil:Unit, cons:Nat×X>

where μ is kind of like fix for types. It binds a type variable X that stands for the type μX. ... itself.

See the book for definitions of nil, cons, isnil, head, tail, etc.

Fold and unfold

With isorecursive types, the types NatList (≡ μX. <nil:Unit, cons:Nat×X>) and <nil:Unit, cons:Nat×NatList> are not the same. To go back and forth between them, we need two new operators, fold and unfold:

fold[NatList] : <nil:Unit, cons:Nat×NatList> → NatList
unfold[NatList] : NatList → <nil:Unit, cons:Nat×NatList>

These operators don’t really do anything; they’re like casts.

Note: Don’t confuse fold with the list operation by the same name.

Isorecursive types are easier to implement, and OCaml uses them. So why don’t we have to write fold and unfold everywhere? The answer is that in OCaml,

Every constructor (e.g., Cons) has an implicit fold in it.
Every pattern-match on a variant type (e.g., match l with...) has an implicit unfold in it.

So in our extended λ-calculus, any time you want to construct something of recursive type, you must use fold. For example, define cons like this:

cons ≡ λx:Nat. λy:NatList. fold[NatList] <cons={x, y}>

And every time you want to use something of recursive type, you must use unfold. For example, define car like this:

car ≡ λl:NatList. case unfold[NatList] l of
                    <nil=u> ⇒ 0,
                    <cons=p> ⇒ p.1

With arrows

So far we have built recursive types out of just sums and products, but it’s also allowed to use →. Sometimes a distinction is made between whether the recursion occurs in positive or negative position; a position is positive if it occurs to the left of an even number of arrows (including 0), negative otherwise (p. 428-429). For example, in

μA. Nat→A
μX. <nil:Unit, cons:{Nat,X}>
μX. (X→Nat)→Nat

the recursion is in positive position; in

μX. X→X

the first X occurs in negative position.

The reason for the distinction is that recursion in positive positions doesn’t break strong normalization, but recursion in negative positions does.