What is a positive coinductive type and why are they so bad?

Question

What is a positive coinductive type and why are they so bad?

---

This question is specifically within the context of Coq and is inspired by this question, the opening lines of which are:

Since positive coinductive types in Coq are evil and break subject reduction, I am trying to develop the theory of the conatural numbers using the following negative formulation (within a module CoNat).

I don't really understand the question that I linked to, so if there's a mismatch between what I'm asking about here and what the question is about, that's why.

Subject reduction, as far as I can tell, is the property that evaluating a term of type t can never cause it to stop being of type t, as explained in this answer. I have never seen any examples of features that break subject reduction in any proof assistant or programming language though in a way that was obvious enough for me to understand what was happening, so I have no intuition about what subject reduction is or what a proof assistant designer has to give up in order to obtain it.

I'm guessing that the following thing is a positive coinductive type for the conatural numbers.

CoInductive conat :=
| cozero : conat
| coS : conat -> conat
.

If I had to bet money, I'd wager the thing that makes it positive is the fact that the two constructors both return an instance of this type so our coinductive type conat does not exclusively appear in contravariant positions (i.e. under the left side of an odd number of implications).

However, I don't understand why this is so bad.

In my mind, a coinductive type like the naive conat above is just like a Haskell data type (which is really a codata type, as someone told me in a bar in Oregon once). It might be infinite, so if you naively recurse over it your function is now partial, and therefore a total language would have to prohibit unbounded recursion over codata.

This doesn't seem so bad, though. To a casual glance, it seems to pose no larger of a problem than totality checking in general does.

Answer 1

Allow me to supplement Pierre-Marie Pédrot's excellent answer with trivial observations that show very concretely what the problem is.

Consider the following coinductive definitions:

CoInductive serpent : Type := cons : serpent -> serpent.

CoFixpoint jormundgandr := cons jormundgandr.

Is jormundgandr equal to cons jormundgandr? Yes, certainly, that's how jormundgandr is defined. Therefore, we would expect the following to work:

Lemma expected : jormundgandr = cons jormundgandr.
Proof.
  reflexivity. (* Does not work. *)
Qed.

It does not work because the normal forms of jormundgandr and cons jormundgandr are not syntactically equal:

Eval compute in jormundgandr.
(* output:
     = cofix jormundgandr : serpent := cons jormundgandr
     : serpent
*)

Eval compute in cons jormundgandr.
(* output:
     = cons (cofix jormundgandr : serpent := cons jormundgandr)
     : serpent
*)

For some reason Coq does not understand that we could just unfold cofix once, like this:

  jormundgandr ≡
  cofix jormundgandr : serpent := cons jormundgandr ≡
  cons (cofix jormundgandr : serpent := cons jormundgandr) ≡
  cons jormundgandr

We can read the above derivation bottom-up in which case we see that we could fold the cofix once. What would be a general strategy for proving such equalities involving cofix?

We shouldn't unfold every cofix blindly because it will go on forever. Coq has a rule: cofix may only be unfolded if an eliminator (for instance a match) is applied to it, because the eliminator will immediately consume whatever cofix produces, thereby guaranteeing progress. (Symmetrically, it is safe to unfold a fix so long as it is applied to a constructor.)

We could try to fold cofix when we see an unfolded one, and that would help in very simple cases, but not in general. For example, given

CoFixpoint boa := cons (cons (cons (cons boa))).
CoFixpoint viper := cons (cons (cons (cons (cons (cons boa))))).

how do we fold and unfold to show that boa ≡ viper? And even if we answer this particular question, we still do not know what to do in general.

We could try all possibilities using some sort of breadth-first search, but that will cause the equality checker to run forever in some cases.

The moral of the story is that there just isn't any good way of dealing with this sort of problem. Because Coq does not unfold cofix in the most intelligent way possible, it fails to prove some equations that hold in the type theory, which means that completeness of subject reduction is broken in Coq.

Now, let us look at the other possibility:

CoInductive serpent : Type := { cons : serpent }.

CoFixpoint midgar := {| cons := midgar |}.

Lemma expected : midgar = cons midgar.
Proof.
  reflexivity. (* It works! *)
Qed.

What's the difference? The normal forms are equal this time:

Eval compute in midgar.
(* output:
     = cofix midgar : serpent := {| cons := midgar |}
     : serpent
*)

Eval compute in cons midgar.
(* output:
     = cofix midgar : serpent := {| cons := midgar |}
     : serpent
*)

Coq used the fact that cons is an elimnator, so it unfolded cofix, like this:

  cons midgar ≡
  cons (cofix midgar : serpent := {| cons := midgar |}) ≡
  cons {| cons := (cofix midgar : serpent := {| cons := midgar |}) |} ≡
  cofix midgar : serpent := {| cons := midgar |}.

(In the case of jormundgandr the same trick does not work because there cons was a constructor.)

However, we do have to pay a price. Is midgar equal to {| cons := midgar |}? Not by reflexivity:

Lemma expectedToo : midgar = {| cons := midgar |}.
Proof.
  reflexivity. (* Does not work. *)
Qed.

This is not failure of subject reduction! The principle that would allow us to prove expectedToo by reflexivity is known as extensionality for record types. It is not part of Coq's type theory.

Let me just mentioned that extensionality of record types holds for propositional equality, so we have the following:

Lemma loki (s t : serpent) : cons s = cons t -> s = t.
Proof.
  case s as [s'].
  case t as [t'].
  simpl.
  intros [].
  reflexivity.
Qed.

Lemma expectedToo : midgar = {| cons := midgar |}.
Proof.
  now apply loki.
Qed.

However, because this is not a proof by reflexivity, it won't be used automagically by Coq normalization. You will have to apply it manually.

I hope this gives you an idea on how the positive and negative co-inductive types differ, and what the problem with subject reduction is.

Answer 2

In Haskell, we tend to care only about weak normalization. For a given term, there are often "wrong" evaluation paths that go on forever without arriving at a value. For example:

head (repeat 1) = head (1 : repeat 1) = head (1 : 1 : repeat 1) = ...

For this particular expression, there are of course "correct" evaluation paths that do arrive at a value, such as

head (repeat 1) = head (1 : repeat 1) = 1 -- 1 is a weak head normal form; actually even a normal form, period

The Haskell specification requires that if there is a "correct" evaluation path (a path that brings an expression to weak head normal form) then the implementation must find a correct evaluation path. This gives power to the programmer: as long as there is some imaginable way to evaluate an expression correctly, it will evaluate correctly. But it also complicates reasoning about code. Some expressions act a little like bombs, which work when you use them in certain contexts but blow up in others (for example, repeat 1 is okay in head (repeat 1) but blows up in last (repeat 1)). It also might not be obvious why a certain expression does or does not evaluate. Finally, it also complicates/pessimizes the implementation: lazy evaluation is the "default" evaluation order of Haskell because it is guaranteed to find a correct evaluation order if one exists, unlike eager evaluation, but the overhead can be catastrophic.

In Coq, we choose to be stricter about evaluation. Coq is designed with strong normalization in mind. Where weak normalization is about at least one evaluation path ending in a WHNF, strong normalization is about all evaluation paths ending in a normal form. The first strengthening (from "at least one" to "all") simplifies reasoning about the language, since you no longer have to worry about choosing the right or wrong way to evaluate an expression. The second strengthening (from getting to WHNFs to getting to NFs) is important for dependent types. A dependently typed system needs to be able to compare terms for equality. (If f : P n -> Q and H : P m for n m : nat, checking f H : Q requires checking n = m, which may be arbitrary expressions.) In a strongly normalizing system, this is in principle easy: just take both sides to normal form and check if you get syntactically equal terms. This works because normal forms are unique. In a weakly normalizing system, this is not so easy, since weak head normal forms are not unique (e.g. 1 : repeat 1 and 1 : 1 : repeat 1 are syntactically different weak head normal forms of the same value).

So, when we have coinductive data in Coq, such as

CoInductive stream := cons (x : nat) (xs : stream).
CoFixpoint repeat (x : nat) : stream := cons x (repeat x).

we must be careful about how we reduce. In particular, we cannot just admit the reduction rule repeat 1 ~> 1 : repeat 1 as exists in Haskell. This would immediately break strong normalization. But then we find that we have an incompatibility with the principle of dependent case analysis!

Definition head xs := match xs with cons x _ => x end.
Definition tail xs := match xs with cons _ xs => xs end.
Definition stream_eta xs : xs = cons (head xs) (tail xs) :=
  match xs return xs = cons (head xs) (tail xs) with (* the whole match has the type specified in the return clause, *)
  | cons x xs => eq_refl (cons x xs) (* but in the branch the expected type has the pattern substituted in for the scrutinee *)
  end.
Eval compute in (stream_eta (repeat 1)).
(* The above line reports, with some prettifying, eq_refl (cons 1 (repeat 1)) : repeat 1 = cons 1 (repeat 1) *)
Fail Check (eq_refl (cons 1 (repeat 1)) : repeat 1 = cons 1 (repeat 1)).
(* huh?!#&?!#?!?!!!!!!???? *)

A well-typed term reduces to a term that no longer checks with the same type! This is very bad. The reason eq_refl (cons 1 (repeat 1)) (which trivially has type cons 1 (repeat 1) = cons 1 (repeat 1)) does not check at type repeat 1 = cons 1 (repeat 1) is that Coq cannot show that repeat 1 and cons 1 (repeat 1) are equal. This is precisely because, to protect strong normalization, we banned the rule repeat 1 ~> 1 : repeat 1. The alternative, allowing repeat 1 ~> 1 : repeat 1, is not better either, since now type checking becomes undecidable (because choosing the right evaluation path is too hard).

Making a coinductive definition negative means, essentially, getting rid of case analysis. "Positive" in this context means "defined by the way elements are constructed". E.g. sum types are considered positive, since A + B is primarily defined by the existence of inl : A -> A + B and inr : B -> A + B, with case analysis as a consequence. Conversely, function types are considered "negative", since A -> B is primarily defined by the ability to combine with an A to give a B. The ability to construct functions via lambda abstraction is just a means to that end. Just as you can't match a function against fun x => body, you can't match negatively defined codata against its constructor.

#[projections(primitive)] CoInductive stream := cons { head : nat; tail : stream }.
Fail Definition stream_eta xs : xs = cons (head xs) (tail xs) :=
  match xs return xs = cons (head xs) (tail xs) with
  | cons x xs => eq_refl (cons x xs)
  end.

Note that you can still have a constructor (here cons : nat -> stream -> stream), and stream perfectly well appears as its return type (i.e. in a "positive" position, for a different meaning of "positive" than above). What changes is that you are not given that all elements of your coinductive are generated from the constructors. You can't assume an arbitrary stream to be cons x xs for some x, xs (which is exactly what match does).

Answer 3

Regarding the question "what is positive vs negative", one answer is that positive types are eliminated by patterns, negative types are introduced by copatterns.

The terminology "positive/negative" actually goes further back to linear logic and focusing (the Copatterns paper is sprinkled with allusions to it), but I hope that the pattern/copattern symmetry is at least a good way to remember it.

A positive type is defined by its constructors, in pseudo-code:

data nat :=
  | Z : nat
  | S : nat -> nat.

and a syntax for elimination can be inferred from that: pattern matching.

double : nat -> nat
double Z = Z
double (S n) = S (S (double n))

A negative type is defined by its destructors:

codata stream :=
  | head : stream -> nat
  | tail : stream -> stream

and a syntax for introduction can be inferred from that: copattern matching.

count : nat -> stream  (* construct a stream by defining its head and tail *)
head (count n) = n
tail (count n) = count (S n)

(Copattern matching may just be another syntax for records, but the point is to remember the symmetry as a mnemonic for this positive/negative distinction.)

Note also the duality extends to recursion:

• fixpoints (recursive pattern-matching functions) eliminate positive types (correspondingly, values of inductive types must be finite/well-founded),
• cofixpoints (recursive copattern-matching functions) introduce negative types (correspondingly, values of coinductive types may be infinite).

So an answer to "what's wrong with positive coinductive types" other than "subject reduction" is aesthetics: in light of the symmetry between patterns and copatterns, making coinductive types negative is the elegant choice.