<ol>
<li><p>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 <span class="math-container">$\mu a.\; a \to X$</span> for any <span class="math-container">$X$</span>.</p>
<p>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 <a href="http://consequently.org/papers/costing.pdf" rel="noreferrer"><em>Curry's Revenge: the costs of non-classical solutions to the paradoxes of self-reference</em></a>.</p>
</li>
<li><p>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.</p>
<p>For example, I asked a very similar question here a few years back, and learned that <a href="https://cstheory.stackexchange.com/questions/15009/is-mall-unrestricted-recursive-types-turing-complete">multiplicative-additive linear logic with recursive types is <em>not</em> Turing-complete.</a> This is called the &quot;Small Normalization Theorem&quot; (Theorem 4.22) in Girard's original paper on linear logic.</p>
</li>
<li><p>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 <a href="http://homepages.inf.ed.ac.uk/gdp/publications/Category_Theoretic_Solution.pdf" rel="noreferrer"><em>The Category-Theoretic Solution of Recursive Domain Equations</em></a>, 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 <a href="https://www.cs.bham.ac.uk/%7Eaxj/pub/papers/handy1.pdf" rel="noreferrer"><em>Abramsky and Jung's handbook chapter</em></a> might be more accessible? I don't really have any great suggestions.</p>
</li>
</ol>

CC BY-SA 3.0
2017-06-02T20:07:08.480Z
"I don't know a good introduction to how to solve recursive domain equations." I agree and it's really unacceptable given how old the techniques are at this point. I would recommend Abramsky & Jung but also "Domains and Lambda Calculi" (Curien and Amadio) helped me to understand the constructions.
Max New
CC BY-SA 3.0
2017-06-02T21:59:10.777Z
Thanks Neel. Regarding 1: I should have been clearer. There are two senses of inconsistency that should be kept apart: it's true that the propositional logic characterized by the inhabited types is inconsistent whether or not you have a 0 type. But in the system Mitchell describes you can't prove all equations between terms. The version with the 0 type does prove all equations: that's what I was worried about.
Andrew Bacon
CC BY-SA 3.0
2017-06-02T22:11:00.600Z
Regarding 3: similarly, the cpo models with the 0 type are presumably going to all be trivial (each type with 1 element). (Because in non-trivial Henkin models, 0 must be interpreted as the empty set. If $\sigma$ is empty, then $\sigma \to 0$ is non-empty, and conversely, so $\sigma = \sigma \to 0$ has no solution.) I will definitely check out those references for my own edification, but they seem to be using CPOs. My hope was to find solutions of $\sigma = \sigma \to 0$ (and other domain equations) in models of linear or affine type theory.
Andrew Bacon
CC BY-SA 3.0
2017-06-02T22:51:51.880Z
Regarding 2: That looks interesting. I'm not very familiar with these things: Is there some connection between Turing completeness and the set of inhabited types being inconsistent?
Andrew Bacon
CC BY-SA 3.0
2017-06-04T16:20:34.730Z
@AndrewBacon: the "second type" of inconsistency (every term can be proven equal) can be refuted without any type consideration, it suffices to prove confluence of the operational semantics of the system (as in the pure $\lambda$-calculus. Of course, domain models as Neel describes are a more semantic way of proving consistency in this sense.
cody
CC BY-SA 3.0
2017-06-05T16:56:02.333Z
Personally, I found Bos&Hemerik - "An Introduction to the Category-theoretic Solution of Recursive Domain Equations" very useful, since it really shows the full proof step-by-step.
chi
CC BY-SA 3.0
2017-06-02T17:20:28.863Z
2017-06-02T17:20:28.863Z
2020-06-17T09:38:08.363Z
Neel Krishnaswami
<p>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.)</p>

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

<p>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$. </p>

<p>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$.)</p>

<p>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$. </p>

<p>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).</p>

<type-systems><type-inference><typed-lambda-calculus><linear-logic>
Recursive types and the empty type
Andrew Bacon
# Recursive types and the empty type

(Asked by: username_0 on 2017-06-02)

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).

**Tags:** type-systems, type-inference, typed-lambda-calculus, linear-logic

---

## 1 answers

### Answer by username_1 on 2017-06-02. Score: 9 | Accepted answer

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*](http://consequently.org/papers/costing.pdf).
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.](https://cstheory.stackexchange.com/questions/15009/is-mall-unrestricted-recursive-types-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*](http://homepages.inf.ed.ac.uk/gdp/publications/Category_Theoretic_Solution.pdf), 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*](https://www.cs.bham.ac.uk/%7Eaxj/pub/papers/handy1.pdf) might be more accessible? I don't really have any great suggestions.

> **Comments:**
> **username_2**: "I don't know a good introduction to how to solve recursive domain equations." I agree and it's really unacceptable given how old the techniques are at this point. I would recommend Abramsky & Jung but also "Domains and Lambda Calculi" (Curien and Amadio) helped me to understand the constructions.  
> **username_0**: Thanks Neel. Regarding 1: I should have been clearer. There are two senses of inconsistency that should be kept apart: it's true that the propositional logic characterized by the inhabited types is inconsistent whether or not you have a 0 type. But in the system Mitchell describes you can't prove all equations between terms. The version with the 0 type does prove all equations: that's what I was worried about.  
> **username_0**: Regarding 3: similarly, the cpo models with the 0 type are presumably going to all be trivial (each type with 1 element). (Because in non-trivial Henkin models, 0 must be interpreted as the empty set. If $\sigma$ is empty, then $\sigma \to 0$ is non-empty, and conversely, so $\sigma = \sigma \to 0$ has no solution.) I will definitely check out those references for my own edification, but they seem to be using CPOs. My hope was to find solutions of $\sigma = \sigma \to 0$ (and other domain equations) in models of linear or affine type theory.  
> **username_0**: Regarding 2: That looks interesting. I'm not very familiar with these things: Is there some connection between Turing completeness and the set of inhabited types being inconsistent?  
> **username_3**: @AndrewBacon: the "second type" of inconsistency (every term can be proven equal) can be refuted without any type consideration, it suffices to prove confluence of the operational semantics of the system (as in the pure $\lambda$-calculus. Of course, domain models as Neel describes are a more semantic way of proving consistency in this sense.  
> **username_4**: Personally, I found Bos&Hemerik - "An Introduction to the Category-theoretic Solution of Recursive Domain Equations" very useful, since it really shows the full proof step-by-step.  

---

