Take the 2-minute tour ×
Theoretical Computer Science Stack Exchange is a question and answer site for theoretical computer scientists and researchers in related fields. It's 100% free, no registration required.

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.

share|improve this question
1  
Is this Coq? Haskell? Pseudo-type theory? What do you mean by "go wrong"? –  Dave Clarke Nov 21 '12 at 12:05
    
@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 Nov 21 '12 at 15:47

3 Answers 3

up vote 9 down vote accepted

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:

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

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.

share|improve this answer

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.

share|improve this answer

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.

share|improve this answer

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

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