# Does Types and Programming Languages use a recursive equation to define a recursive type or its generator?

In Types and Programming Languages by Pierce et al:

The recursive equation specifying the type of lists of numbers is similar to the equation specifying the recursive factorial function on page 52:

factorial = λn. if n=0 then 1 else n * factorial(n-1)


Here, as there, it is convenient to make this equation into a proper deﬁnition by moving the “loop” over to the right-hand side of the =. We do this by introducing an explicit recursion operator µ for types:

NatList = µX. <nil:Unit, cons:{Nat,X}>;


Intuitively, this deﬁnition is read, “Let NatList be the inﬁnite type satisfying the equation X = <nil:Unit, cons:{Nat,X}>.”

I have some questions for understanding it:

1. What does the “loop” mean?

2. Does the recursion operator µ for types play similar role as operator λ for abstractions?

3. Doesn't NatList defined by NatList = µX. <nil:Unit, cons:{Nat,X}> look more like the generator of the recursive type X, i.e. a type mapping so that X = NatList X?

4. How can NatList as the generator of the recursive type X be the inﬁnite type X satisfying the equation X = <nil:Unit, cons:{Nat,X}>?

Thanks.

You've stumbled across the difference between isorecursive and equirecursive types.

Equi-recursive types say "types are (possibly) infinite trees, and a recursive type is the solution to a recursive equation". Specifically, $$\mu x\ldotp T = [\mu x \ldotp T/x]T$$. These are conceptually simple, but in practice difficult to work with, since deciding whether two types are equal (or worse, subtypes of one another) or not is tricky.

Conversely, isorecursive types say that recursive types are just syntax. You are allowed to unroll them according to the equation above, but $$\mu x\ldotp T$$ and $$[\mu x \ldotp T/x]T$$ are fundamentally different types, and must use the explicit fold and unfold instructions.

If you keep reading Pierce, he will explain this in the book.

2. Yes, $$\mu$$ is similar to $$\lambda$$ in the sense that they both bind variables. However, it's different in that there's always a very specific thing that gets plugged in for the bound variable with $$\mu$$, whereas $$\lambda$$ is useful precisely because we can plug the variable with anything. Also, the bound variable of $$\mu$$ denotes a type, whereas with $$\lambda$$ it denotes a term.
3. Yes, and that's the point of the $$\mu$$ operator. It says "I am the syntax that takes the generator for a type, and turns it into an actual type you can use like any other type in your program." And it make explicit the role of $$X$$ in the equation your outline.
4. Again, this is the job of $$\mu$$ by definintion. It is the piece of syntax that says "given the generator, tie the knot and make it an actual type."
The thing is, you can't really understand $$\mu$$-types on their own. Otherwise it's just syntax. The key is in the type rules for $$\mu$$ types. For isorecursive types, there are fold and unfold rules that allow us to "run the generator" one step. For equirecursive types, there are special rules in how type equality is determined that allow us to treat $$\mu x \ldotp T$$ as actually being the solution generated by the recurrence equation. But, these type rules will change depending on the specific language or calculus you're using.