1
$\begingroup$

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 definition 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 definition is read, “Let NatList be the infinite 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 infinite type X satisfying the equation X = <nil:Unit, cons:{Nat,X}>?

Thanks.

$\endgroup$
2
$\begingroup$

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.

Answering your specific questions:

  1. The "loop" is that the definition on the RHS or the = is allowed to reference the name defined on the left. This is awkward for theory, because we don't want to treat top-level definitions as special.

  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.

$\endgroup$
  • $\begingroup$ Thanks. " since deciding whether two types are equal (or worse, subtypes of one another) is not tricky", do you mean "trivial" by "tricky"? $\endgroup$ – Tim Aug 30 at 18:59
  • $\begingroup$ @Tim yep, typo on my part. Fixed now! $\endgroup$ – jmite Aug 30 at 19:31

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.