"Guarded" negative occurrences in definition of inductive types, always bad?

Question

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.

Answer 1

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 and here) tells me that a good place to look for the story is:

• Structural Induction and Coinduction in a Fibrational Setting, Claudio Hermida and Bart Jacobs 1997.
• Fibrational Induction Rules for Initial Algebras, 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, Pierre America and Jan J. M. M. Rutten 1989.
• The Category-Theoretic Solution of Recursive Metric-space Equations, 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, Hiroshi Nakano, 2000.
• Ultrametric Semantics of Reactive Programs, Nick Benton and Neel Krishnaswami, 2011.
• A metric model of guarded recursion, Lars Birkedal, Jan Schwinghammer, and Kristian Støvring, 2010.

Answer 2

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:

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

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