Recursive types and the empty type

Question

In John Mitchell's book "The Foundations of Programming Languages", he considers a typed lambda calculus with unit, exponential, product, (binary) coproduct types, and arbitrary recursive types (p126). Later in the book he shows how to construct models of all these types. (I'm pretty new to all of this, but I assume this is a pretty standard system.)

It looks as though it is not possible to extend this system with a 0 type for the following reason:

Let $\sigma$ be $\mu t.t\to 0$. $\mbox{unfold}: \sigma \to \sigma \to 0$ and $\mbox{fold}: (\sigma \to 0)\to \sigma$. Then $W(\mbox{unfold})(\mbox{fold}(W(\mbox{unfold}))): 0$, where $W = \lambda xy.xyy$.

From this you can prove all equations between terms (e.g. from the existence of a closed term $t:0$, $\lambda x.t:A \to 0$ is an isomorphism between any type $A$ and $0$.)

A natural thought would be to work in a linear or affine type theory where the $W$ combinator isn't allowed, and which therefore might allow solutions to type equations like $\sigma = \sigma \to 0$.

My questions is: Is the resulting type theory consistent, and can anyone explain to me how to go about constructing models? (References would also be welcome, but the papers I've looked at so far have generally presupposed more knowledge than I have).

Answer 1

1. First, note that nothing turns on the presence or absence of the empty type: if you have a nonlinear calculus with function types and unrestricted recursive types, then it is inconsistent. Indeed, your derivation works regardless of the type of the answer -- the very same term you have works for $\mu a.\; a \to X$ for any $X$.

   This is known as Curry's Paradox, and is also known as the Y combinator. There is a nice discussion of this in Greg Restall's paper Curry's Revenge: the costs of non-classical solutions to the paradoxes of self-reference.

2. Next, your observation that the fixed point combinators rely upon contraction is astute. Curry's paradox depends on all three of contraction, unrestricted recursive types, and a function space, and removing any one of them suffices to block it.

   For example, I asked a very similar question here a few years back, and learned that multiplicative-additive linear logic with recursive types is not Turing-complete. This is called the "Small Normalization Theorem" (Theorem 4.22) in Girard's original paper on linear logic.

3. You can still construct models of this language (with or without units) using domain theory. The main technical difficulty is the interpretation of recursive types. I don't know a good introduction to how to solve recursive domain equations. I learned it from Plotkin and Smyth's The Category-Theoretic Solution of Recursive Domain Equations, but that was really not a good tutorial for me: I needed a fair amount of help to understand it. The critical intuitions are all there, but it's quite dense. Maybe Abramsky and Jung's handbook chapter might be more accessible? I don't really have any great suggestions.