<p>Sometimes you can solve recursive equations "by luck".</p>

<p>I presume you want to do this in sets (as opposed to some sort of domain theory) If we unfold your definition and write down the equation directly without Haskell annotations, we get
$$A \cong (A \to \emptyset) \to A.$$
Let us consider two cases:</p>

<ol>
<li><p>If $A$ is inhabited, i.e., it contains something, then $A \to \emptyset \cong \emptyset$, therefore the equation reduces to $$A \cong \emptyset \to A \cong 1.$$ And indeed, the singleton set $1$ solves the equation.</p></li>
<li><p>If $A$ is empty then we get $\emptyset \cong (\emptyset \to \emptyset) \to \emptyset \cong 1 \to \emptyset \cong \emptyset$.</p></li>
</ol>

<p>Conclusion: there are two solutions, the empty type (which you called <code>False</code>) and the unit type <code>()</code>.</p>

<p>Here is another interesting example:
$$A \cong (A \to 2) \to 2,$$
or in Haskell</p>

<pre><code>data Cow a = Moo ((a -&gt; Bool) -&gt; Bool)
</code></pre>

<p>In terms of sets this is $A \cong 2^{2^A}$. By Cantor's theorem there is no solution, as $A$ has fewer elements than $2^{2^A}$. However, if we look at this equation in topological spaces, there is a solution, namely
$$\mathbb{N} \cong 2^{2^\mathbb{N}}.$$
This is so because $2^\mathbb{N}$ is the Cantor space, $2^{2^\mathbb{N}}$ is the space of its clopen subsets, of which there are countably many (and you have to think to see that they form a discrete space). Similarly, you can <a href="http://math.andrej.com/2009/10/12/constructive-gem-double-exponentials/">exhibit a bijection</a> between <code>Integer</code> and <code>(Integer -&gt; Bool) -&gt; Bool</code> in Haskell.</p>

CC BY-SA 3.0
2012-11-21T14:56:41.300Z
2012-11-21T14:56:41.300Z
Andrej Bauer
<p>It's hard to add anything to Andrej's or Neel's explanations, but I'll give it a shot. I'm going to try to address the syntactic point of view, rather than try to uncover underlying semantics, because the explanation is more elementary and my give a more straightforward answer to your question.</p>

<p>I am going to work in the <em>simply-typed</em> $\lambda$-calculus rather than the more complex system underlying Haskell. I believe in particular that the presence of type variables may be confusing you to a certain extent.</p>

<p>The crucial reference is the following:</p>

<p>Mendler, N. (1991). Inductive types and type constraints in the second-order lambda calculus. I haven't found a reference online I'm afraid. The statements and proofs can however be found in Nax's <a href="http://www.nuprl.org/documents/Mendler/InductiveDefinition.html" rel="nofollow">PhD dissertation</a> (a highly recommended read!).</p>

<p>Mendler explains that positivity is a <em>necessary</em> and <em>sufficient</em> condition for termination in the presence of non-recursive case definitions (and structurally decreasing recursive ones). He states it using an <em>equational</em> formulation. I give a simple example, which is a simplification of your $\mathrm{Bad}$ type.</p>

<p>$$ \mathrm{Bad} = \mathrm{Bad}\rightarrow A$$</p>

<p>Where $A$ is any type. We then have</p>

<p>$$ \lambda x:\mathrm{Bad}.x\ x: \mathrm{Bad}\rightarrow A$$</p>

<p>and so</p>

<p>$$ (\lambda x:\mathrm{Bad}.x\ x)\ (\lambda x:\mathrm{Bad}.x\ x): A $$</p>

<p>Mendler shows that this can be carried out for <em>any</em> type
$$ \mathrm{Bad} = F(\mathrm{Bad})$$
where $F(X)$ is a type with at least one negative occurrence of $X$ (there may be positive occurrences as well). He gives an explicit term which fails to terminate for a given $F(X)$ (pages 39-40 of his thesis).</p>

<p>Of course you are working not with equationally defined types but with <em>constructors</em>, i.e. you have</p>

<pre><code>data Bad = Pack (Bad -&gt; A)
</code></pre>

<p>rather than strict equality. However you can define</p>

<pre><code>unpack :: Bad -&gt; (Bad -&gt; A)
unpack (Pack f) = f
</code></pre>

<p>which is sufficient for this result to continue to hold:</p>

<pre><code> (\x:Bad -&gt; unpack x x) (Pack (\x:Bad -&gt; unpack x x))
</code></pre>

<p>This term is still well typed of type $A$.</p>

<hr>

<p>In your second example, things are a bit more tricky, as you have somethings along the lines of</p>

<p>$$ \mathrm{Bad} = \mathrm{Bad}' \rightarrow A$$</p>

<p>where $\mathrm{Bad}'$ is <em>related</em>, but <em>not</em> equal, to $\mathrm{Bad}$ (in your case they are equal to $\mathrm{Bad}\ a$ and $\mathrm{Bad}\ (\mathrm{Not}\ a)$ respectively). I'll admit that I could not build a straightforward isomorphism between the two. The same problem is present if you replace</p>

<pre><code>type Not a = a -&gt; False
</code></pre>

<p>with</p>

<pre><code>data Not a = Not a
</code></pre>

<p>It would be easily solved if Haskell allowed such type definitions:</p>

<pre><code>type Acc = Not Acc
</code></pre>

<p>In this case, you could build a looping combinator in exactly the same manner as before. I suspect you can carry a similar (but more complex) construction using</p>

<pre><code>data Acc = D (Not Acc)
</code></pre>

<p>The trouble here is that to build an isomorphism</p>

<pre><code>Bad Acc &lt;-&gt; Bad (Not Acc)
</code></pre>

<p>you have to deal with mixed variance.</p>

CC BY-SA 3.0
2012-11-26T19:13:47.297Z
2012-11-26T19:13:47.297Z
cody
<p>The reason for the ban on negative occurrences can be understood by analogy with the Knaster-Tarski theorem. This theorem says that</p>
<blockquote>
<p>if <span class="math-container">$L$</span> is a complete lattice and <span class="math-container">$f : L \to L$</span> is a monotone function on <span class="math-container">$L$</span>, then the set of fixed points of <span class="math-container">$f$</span> is also a complete lattice. In particular, there is a least fixed point <span class="math-container">$\mu{f}$</span> and a greatest fixed point <span class="math-container">$\nu f$</span>.</p>
</blockquote>
<p>In traditional model theory, lattices <span class="math-container">$L$</span> can be viewed as propositions, and the order relation <span class="math-container">$p \leq q$</span> can be understood as entailment (i.e., that <span class="math-container">$q$</span>'s truth is entailed by <span class="math-container">$p$</span>'s truth).</p>
<p>When we move from model theory to proof theory, lattices generalize to categories. Types can be seen as the objects of a category <span class="math-container">$\mathbb{C}$</span>, and a map <span class="math-container">$e : P \to Q$</span> represents a <em>proof</em> that <span class="math-container">$Q$</span> can be derived from <span class="math-container">$Q$</span>.</p>
<p>When we try to interpret types defined by recursive equations, e.e., <span class="math-container">$\mathbb{N} = \mu \alpha.\;1 + \alpha$</span>, the obvious thing to do is to look for a generalization of the Knaster-Tarski theorem. So instead of a monotone function on a lattice, we know want a <em>functor</em> <span class="math-container">$F : \mathbb{C} \to \mathbb{C}$</span>, which sends objects to objects, but generalizes the monotonicity condition so that every map <span class="math-container">$e : P \to Q$</span> gets a map <span class="math-container">$F(e) : F(P) \to F(Q)$</span> (with the coherence conditions that <span class="math-container">$F$</span> sends identities to identities and preserves compositions so that <span class="math-container">$F(g \circ f) = F(g) \circ F(f)$</span>).</p>
<p>So if you want an inductive datatype <span class="math-container">$\mu \alpha.\;F(\alpha)$</span>, you also need to supply a functorial action on terms for the type operator <span class="math-container">$F$</span> in order to be assured that the fixed point you want exists. The strict positivity condition in Agda and Coq is a <em>syntactic</em> condition that implies this <em>semantic</em> constraint. Loosely speaking, it says that if you build a type operator from sums and products, then you can always cook up the functorial action, and so any type formed in this way should have a fixed point.</p>
<p>In dependently-typed languages, you also have indexed and parameterized types, so your real task is more complicated. Bob Atkey (who has blogged about this <a href="https://bentnib.org/posts/2011-04-22-structural-recursion.html" rel="nofollow noreferrer">here</a> and <a href="https://bentnib.org/posts/2011-04-28-folds-and-induction.html" rel="nofollow noreferrer">here</a>) tells me that a good place to look for the story is:</p>
<ul>
<li><a href="http://citeseer.ist.psu.edu/viewdoc/download?doi=10.1.1.36.7400&amp;rep=rep1&amp;type=pdf" rel="nofollow noreferrer"><em>Structural Induction and Coinduction in a Fibrational Setting</em></a>,  Claudio Hermida and Bart Jacobs 1997.</li>
<li><a href="https://cs.appstate.edu/%7Ejohannp/csl2010.pdf" rel="nofollow noreferrer"><em>Fibrational Induction Rules for Initial Algebras</em></a>, Neil Ghani, Patricia Johann, and Clement Fumex 2010.</li>
</ul>
<p>As Andrej notes, fundamentally whether or not a negative occurence is okay or not depends on what your model of type theory. Basically, when you have a recursive definition, you are looking for a fixed point, and there are a <em>lot</em> of fixed-point theorems in mathematics.</p>
<p>One which I, personally, have made a lot of use of is Banach's fixed point theorem, which says that if you have a strictly contractive function on a metric space, then it has a unique fixed point. This idea was introduced into semantics by (IIRC) Maurice Nivat, and was extensively studied by America and Rutten, and was recently connected by Birkedal and his collaborators to a popular operational technique called &quot;step-indexing&quot;.</p>
<ul>
<li><a href="https://homepages.cwi.nl/%7Ejanr/papers/files-of-papers/1989-JCSS.pdf" rel="nofollow noreferrer"><em>Solving Reflexive Domain Equations in a Category of Complete Metric Spaces</em></a>, Pierre America and Jan J. M. M. Rutten 1989.</li>
<li><a href="https://cs.au.dk/%7Ebirke/papers/metric-enriched-journal.pdf" rel="nofollow noreferrer"><em>The Category-Theoretic Solution of Recursive Metric-space Equations</em></a>, Lars Birkedal, Kristian Støvring, and Jacob Thamsborg. 2010.</li>
</ul>
<p>This gives rise to type theories where negative occurences in recursive types are permitted, but only when the negative occurences occur under a special &quot;guardedness&quot; type constructor. This idea was introduced by Hiroshi Nakano, and the connection to Banach's theorem was made both by myself and Nick Benton, as well as Lars Birkedal and his coauthors.</p>
<ul>
<li><a href="http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.22.7573" rel="nofollow noreferrer"><em>A Modality for Recursion</em></a>, Hiroshi Nakano, 2000.</li>
<li><a href="http://www.mpi-sws.org/%7Eneelk/frp-lics11.pdf" rel="nofollow noreferrer"><em>Ultrametric Semantics of Reactive Programs</em></a>, Nick Benton and Neel Krishnaswami, 2011.</li>
<li><a href="https://cs.au.dk/%7Ebirke/papers/nakano-conf.pdf" rel="nofollow noreferrer"><em>A metric model of guarded recursion</em></a>, Lars Birkedal, Jan Schwinghammer, and Kristian Støvring, 2010.</li>
</ul>

CC BY-SA 4.0
2023-07-08T20:22:52.353Z
> when the negative occurences occur under a special "guardedness" type constructor

Is it enough to guard *negative* occurrences? E.g., intuitively, I'd say that $D \equiv (\blacktriangleright D \to D) + 1$ should work, but that there is an unguarded positive occurrence. In https://arxiv.org/pdf/1208.3596.pdf they write

> For example, it might be possible to show the existence of recursive types in which only negative occurrences of the recursion variable were guarded

But I haven't found that future work so far ...
Sebastian Graf
CC BY-SA 4.0
2012-11-22T09:23:05.157Z
2021-03-22T09:38:13.753Z
2021-03-22T09:38:13.753Z
Neel Krishnaswami
<p>I know how some negative occurrences can definitively be bad:</p>

<pre><code>data False

data Bad a = C (Bad a -&gt; a)

selfApp :: Bad a -&gt; a
selfApp (x@(C x')) = x' x

yc :: (a -&gt; a) -&gt; a
yc f = selfApp $ C (\x -&gt; f (selfApp x))

false :: False
false = yc id
</code></pre>

<p>However, I am not sure whether:</p>

<ul>
<li><p>all inductive types with negative occurences can turn wrong ;</p></li>
<li><p>if so, there is a known mechanical way of doing so ;</p></li>
</ul>

<p>For instance, I've been fighting trying to make this type go wrong:</p>

<pre><code>type Not a = a -&gt; False

data Bad2 a = C2 (Bad2 (Not a) -&gt; a)
</code></pre>

<p>Any pointer to literature on this subject would be appreciated.</p>

CC BY-SA 3.0
2012-11-21T12:05:28.907Z
Is this Coq? Haskell? Pseudo-type theory? What do you mean by "go wrong"?
Dave Clarke
CC BY-SA 3.0
2012-11-21T15:47:11.737Z
@DaveClarke Sorry, the code is Haskell, but the concern is more about languages like Coq or Agda where negative occurences are forbidden. By "go wrong", I mean being able to write a term that diverges, thus being able to inhabit False as I did in my example in Haskell.
Ptival
<lo.logic><type-theory><soundness>
"Guarded" negative occurrences in definition of inductive types, always bad?
Ptival
# "Guarded" negative occurrences in definition of inductive types, always bad?

(Asked by: username_0 on 2012-11-21)

I know how some negative occurrences can definitively be bad:
data False

data Bad a = C (Bad a -> a)

selfApp :: Bad a -> a
selfApp (x@(C x')) = x' x

yc :: (a -> a) -> a
yc f = selfApp $ C (\x -> f (selfApp x))

false :: False
false = yc id

However, I am not sure whether:

all inductive types with negative occurences can turn wrong ;
if so, there is a known mechanical way of doing so ;

For instance, I've been fighting trying to make this type go wrong:
type Not a = a -> False

data Bad2 a = C2 (Bad2 (Not a) -> a)

Any pointer to literature on this subject would be appreciated.

**Tags:** lo.logic, type-theory, soundness

> **Comments:**
> **username_1**: Is this Coq? Haskell? Pseudo-type theory? What do you mean by "go wrong"?  
> **username_0**: @DaveClarke Sorry, the code is Haskell, but the concern is more about languages like Coq or Agda where negative occurences are forbidden. By "go wrong", I mean being able to write a term that diverges, thus being able to inhabit False as I did in my example in Haskell.  

---

## 3 answers

### Answer by username_4 on 2012-11-22. Score: 13 | Accepted answer

The reason for the ban on negative occurrences can be understood by analogy with the Knaster-Tarski theorem. This theorem says that

> if $L$ is a complete lattice and $f : L \to L$ is a monotone function on $L$, then the set of fixed points of $f$ is also a complete lattice. In particular, there is a least fixed point $\mu{f}$ and a greatest fixed point $\nu f$.

In traditional model theory, lattices $L$ can be viewed as propositions, and the order relation $p \leq q$ can be understood as entailment (i.e., that $q$'s truth is entailed by $p$'s truth).

When we move from model theory to proof theory, lattices generalize to categories. Types can be seen as the objects of a category $\mathbb{C}$, and a map $e : P \to Q$ represents a *proof* that $Q$ can be derived from $Q$.

When we try to interpret types defined by recursive equations, e.e., $\mathbb{N} = \mu \alpha.\;1 + \alpha$, the obvious thing to do is to look for a generalization of the Knaster-Tarski theorem. So instead of a monotone function on a lattice, we know want a *functor* $F : \mathbb{C} \to \mathbb{C}$, which sends objects to objects, but generalizes the monotonicity condition so that every map $e : P \to Q$ gets a map $F(e) : F(P) \to F(Q)$ (with the coherence conditions that $F$ sends identities to identities and preserves compositions so that $F(g \circ f) = F(g) \circ F(f)$).

So if you want an inductive datatype $\mu \alpha.\;F(\alpha)$, you also need to supply a functorial action on terms for the type operator $F$ in order to be assured that the fixed point you want exists. The strict positivity condition in Agda and Coq is a *syntactic* condition that implies this *semantic* constraint. Loosely speaking, it says that if you build a type operator from sums and products, then you can always cook up the functorial action, and so any type formed in this way should have a fixed point.

In dependently-typed languages, you also have indexed and parameterized types, so your real task is more complicated. Bob Atkey (who has blogged about this [here](https://bentnib.org/posts/2011-04-22-structural-recursion.html) and [here](https://bentnib.org/posts/2011-04-28-folds-and-induction.html)) tells me that a good place to look for the story is:

* [*Structural Induction and Coinduction in a Fibrational Setting*](http://citeseer.ist.psu.edu/viewdoc/download?doi=10.1.1.36.7400&rep=rep1&type=pdf), Claudio Hermida and Bart Jacobs 1997.
* [*Fibrational Induction Rules for Initial Algebras*](https://cs.appstate.edu/%7Ejohannp/csl2010.pdf), Neil Ghani, Patricia Johann, and Clement Fumex 2010.

As Andrej notes, fundamentally whether or not a negative occurence is okay or not depends on what your model of type theory. Basically, when you have a recursive definition, you are looking for a fixed point, and there are a *lot* of fixed-point theorems in mathematics.

One which I, personally, have made a lot of use of is Banach's fixed point theorem, which says that if you have a strictly contractive function on a metric space, then it has a unique fixed point. This idea was introduced into semantics by (IIRC) Maurice Nivat, and was extensively studied by America and Rutten, and was recently connected by Birkedal and his collaborators to a popular operational technique called "step-indexing".

* [*Solving Reflexive Domain Equations in a Category of Complete Metric Spaces*](https://homepages.cwi.nl/%7Ejanr/papers/files-of-papers/1989-JCSS.pdf), Pierre America and Jan J. M. M. Rutten 1989.
* [*The Category-Theoretic Solution of Recursive Metric-space Equations*](https://cs.au.dk/%7Ebirke/papers/metric-enriched-journal.pdf), Lars Birkedal, Kristian Støvring, and Jacob Thamsborg. 2010.

This gives rise to type theories where negative occurences in recursive types are permitted, but only when the negative occurences occur under a special "guardedness" type constructor. This idea was introduced by Hiroshi Nakano, and the connection to Banach's theorem was made both by myself and Nick Benton, as well as Lars Birkedal and his coauthors.

* [*A Modality for Recursion*](http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.22.7573), Hiroshi Nakano, 2000.
* [*Ultrametric Semantics of Reactive Programs*](http://www.mpi-sws.org/%7Eneelk/frp-lics11.pdf), Nick Benton and username_4, 2011.
* [*A metric model of guarded recursion*](https://cs.au.dk/%7Ebirke/papers/nakano-conf.pdf), Lars Birkedal, Jan Schwinghammer, and Kristian Støvring, 2010.

> **Comments:**
> **username_5**: > when the negative occurences occur under a special "guardedness" type constructor  Is it enough to guard *negative* occurrences? E.g., intuitively, I'd say that $D \equiv (\blacktriangleright D \to D) + 1$ should work, but that there is an unguarded positive occurrence. In https://arxiv.org/pdf/1208.3596.pdf they write  > For example, it might be possible to show the existence of recursive types in which only negative occurrences of the recursion variable were guarded  But I haven't found that future work so far ...  

---

### Answer by username_2 on 2012-11-21. Score: 8

Sometimes you can solve recursive equations "by luck".
I presume you want to do this in sets (as opposed to some sort of domain theory) If we unfold your definition and write down the equation directly without Haskell annotations, we get
$$A \cong (A \to \emptyset) \to A.$$
Let us consider two cases:

If $A$ is inhabited, i.e., it contains something, then $A \to \emptyset \cong \emptyset$, therefore the equation reduces to $$A \cong \emptyset \to A \cong 1.$$ And indeed, the singleton set $1$ solves the equation.
If $A$ is empty then we get $\emptyset \cong (\emptyset \to \emptyset) \to \emptyset \cong 1 \to \emptyset \cong \emptyset$.

Conclusion: there are two solutions, the empty type (which you called False) and the unit type ().
Here is another interesting example:
$$A \cong (A \to 2) \to 2,$$
or in Haskell
data Cow a = Moo ((a -> Bool) -> Bool)

In terms of sets this is $A \cong 2^{2^A}$. By Cantor's theorem there is no solution, as $A$ has fewer elements than $2^{2^A}$. However, if we look at this equation in topological spaces, there is a solution, namely
$$\mathbb{N} \cong 2^{2^\mathbb{N}}.$$
This is so because $2^\mathbb{N}$ is the Cantor space, $2^{2^\mathbb{N}}$ is the space of its clopen subsets, of which there are countably many (and you have to think to see that they form a discrete space). Similarly, you can exhibit a bijection between Integer and (Integer -> Bool) -> Bool in Haskell.


---

### Answer by username_3 on 2012-11-26. Score: 3

It's hard to add anything to Andrej's or Neel's explanations, but I'll give it a shot. I'm going to try to address the syntactic point of view, rather than try to uncover underlying semantics, because the explanation is more elementary and my give a more straightforward answer to your question.
I am going to work in the simply-typed $\lambda$-calculus rather than the more complex system underlying Haskell. I believe in particular that the presence of type variables may be confusing you to a certain extent.
The crucial reference is the following:
Mendler, N. (1991). Inductive types and type constraints in the second-order lambda calculus. I haven't found a reference online I'm afraid. The statements and proofs can however be found in Nax's PhD dissertation (a highly recommended read!).
Mendler explains that positivity is a necessary and sufficient condition for termination in the presence of non-recursive case definitions (and structurally decreasing recursive ones). He states it using an equational formulation. I give a simple example, which is a simplification of your $\mathrm{Bad}$ type.
$$ \mathrm{Bad} = \mathrm{Bad}\rightarrow A$$
Where $A$ is any type. We then have
$$ \lambda x:\mathrm{Bad}.x\ x: \mathrm{Bad}\rightarrow A$$
and so
$$ (\lambda x:\mathrm{Bad}.x\ x)\ (\lambda x:\mathrm{Bad}.x\ x): A $$
Mendler shows that this can be carried out for any type
$$ \mathrm{Bad} = F(\mathrm{Bad})$$
where $F(X)$ is a type with at least one negative occurrence of $X$ (there may be positive occurrences as well). He gives an explicit term which fails to terminate for a given $F(X)$ (pages 39-40 of his thesis).
Of course you are working not with equationally defined types but with constructors, i.e. you have
data Bad = Pack (Bad -> A)

rather than strict equality. However you can define
unpack :: Bad -> (Bad -> A)
unpack (Pack f) = f

which is sufficient for this result to continue to hold:
 (\x:Bad -> unpack x x) (Pack (\x:Bad -> unpack x x))

This term is still well typed of type $A$.

In your second example, things are a bit more tricky, as you have somethings along the lines of
$$ \mathrm{Bad} = \mathrm{Bad}' \rightarrow A$$
where $\mathrm{Bad}'$ is related, but not equal, to $\mathrm{Bad}$ (in your case they are equal to $\mathrm{Bad}\ a$ and $\mathrm{Bad}\ (\mathrm{Not}\ a)$ respectively). I'll admit that I could not build a straightforward isomorphism between the two. The same problem is present if you replace
type Not a = a -> False

with
data Not a = Not a

It would be easily solved if Haskell allowed such type definitions:
type Acc = Not Acc

In this case, you could build a looping combinator in exactly the same manner as before. I suspect you can carry a similar (but more complex) construction using
data Acc = D (Not Acc)

The trouble here is that to build an isomorphism
Bad Acc <-> Bad (Not Acc)

you have to deal with mixed variance.


---

