Polymorphism and Inductive datatypes

Question

I'm curious. I've been working on this datatype in OCaml:

type 'a exptree =
  | Epsilon
  | Delta of 'a exptree * 'a exptree
  | Omicron of 'a
  | Iota of 'a exptree exptree

Which can be manipulated using explicitly typed recursive functions (a feature that has been added quite recently). Example:

let rec map : 'a 'b. ('a -> 'b) -> 'a exptree -> 'b exptree =
  fun f ->
    begin function
    | Epsilon -> Epsilon
    | Delta (t1, t2) -> Delta (map f t1, map f t2)
    | Omicron t -> Omicron (f t)
    | Iota tt -> Iota (map (map f) tt)
    end

But I've never been able to define it in Coq:

Inductive exptree a :=
  | epsilon : exptree a
  | delta : exptree a -> exptree a -> exptree a
  | omicron : a -> exptree a
  | iota : exptree (exptree a) -> exptree a
.

Coq is whining. It doesn't like the last constructor, and says something I don't completely understand or agree with:

Error: Non strictly positive occurrence of "exptree" in "exptree (exptree a) -> exptree a".

What I can understand is that inductive types using a negation inside their definition like type 'a term = Constructor ('a term -> …) are rejected, because they would lead to ugly non well-founded beasts like (untyped) λ-terms. However this particular exptree datatype seems innocuous enough: looking at its OCaml definition, its argument 'a is never used in negative positions.

It seems that Coq is overcautious here. So is there really a problem with this particular inductive datatype? Or could Coq be slightly more permissive here?

Also, what about other proof assistants, are they able to cope with such an inductive definition (in a natural way)?

Answer 1

This has come up on the Coq mailing list several times, but I never saw a conclusive answer. Coq isn't as general as it could be; the rules in (Coquand, 1990) and (Giménez, 1998) (and his PhD thesis) are more general and do not require strict positivity. Positivity enough is not enough, however, when you go outside Set; this example came up in several discussions:

Inductive Big : Type := B : ((B -> Prop) -> Prop) -> Big.

With plain data structures such as yours, the inductive type would not cause problems other than making the implementation more complex.

There is a general way to define types such as this defined as the fixpoint of a polynomial: $$F = \epsilon + \delta\, (F \times F) + \omicron\, \mathrm{id} + F \circ F$$

Instead of attempting to define the function $\mathrm{exptree} : a \mapsto \mathrm{exptree}(a)$, define the family of types $\mathrm{exptree}, \mathrm{exptree} \circ \mathrm{exptree}, \mathrm{exptree} \circ \mathrm{exptree} \circ \mathrm{exptree}, \ldots$. This means adding an integer parameter to the type that encodes the number of self-compositions ($\mathrm{exptree}^0(a) = a$, $\mathrm{exptree}^1(a) = \mathrm{exptree}(a)$, $\mathrm{exptree}^2(a) = \mathrm{exptree}(\mathrm{exptree}(a))$, etc), and a supplementary injection constructor to turn $a$ into $\mathrm{exptree}^0(a) = a$.

Inductive et : nat -> Type -> Type :=
  | alpha : forall a, a -> et 0 a                      (*injection*)
  | omicron : forall n a, et n a -> et (S n) a         (**)
  | epsilon : forall (S n) a, et (S n) a
  | delta : forall n a, et (S n) a -> et (S n) a -> et (S n) a
  | iota : forall n a, et (S (S n)) a -> et (S n) a
.

You can proceed to define values and work on them. Coq will often be able to infer the exponent. Set Implicit Arguments would make these definitions prettier.

Definition exptree := et 1.
Definition et1 : exptree nat :=
  delta _ _ (omicron _ _ (alpha _ 42)) (epsilon _ _).
Definition et2 : exptree nat := iota _ _ (omicron _ _ et1).

You may prefer to decrease the argument by 1, so that exptree is et 0. This removes a lot of S n in the definition, which may make some proofs easier, but it requires splitting the initial case from the recurrence case in every constructor that takes an $a$ in an argument (instead of adding a single injection constructor for $a$). In this example, there's only a single constructor to split, so this should be a good choice.

Inductive et : nat -> Type -> Type :=
  | omicron_0 : forall a, a -> et 0 a
  | omicron_S : forall n a, et n a -> et (S n) a
  | epsilon : forall n a, et n a
  | delta : forall n a, et n a -> et n a -> et n a
  | iota : forall n a, et (S n) a -> et n a
.
Definition exptree := et 0.
Definition et1 : exptree nat :=
  delta _ _ (omicron_0 _ 42) (epsilon _ _).
Definition et2 : exptree nat :=
  (iota _ _ (omicron_S _ _ et1)).

I think this is the same principle proposed in a more general form by Ralph Mattes.

References

Thierry Coquand and Christine Paulin. Inductively defined types. In Proceedings of COLOG'88, LNCS 417, 1990. [Springer] [Google]

Eduardo Giménez. Structural Recursive Definitions in Type Theory. In ICALP'98: Proceedings of the 25th International Colloquium on Automata, Languages and Programming. Springer-Verlag, 1998. [PDF]

Answer 2

Ralph Matthes describes how to simulate types like this in Coq in "A Datastructure for Iterated Powers" (code, paper).

Answer 3

One of the first things Coq does is building the induction principle associated with the inductive type you just defined and understanding the underlying induction principle is a good exercise.

For example O : nat | S : nat -> nat will generate the induction principle P O -> (∀ n, P n -> P (S n)) -> ∀ n, P n.

What would be the induction principle corresponding to iota? It seems that there is no predicate P that would be able to talk about P t and P (iota t), because it should talk about exptree a, exptree (exptree a), exptree (exptree (exptree a)) ...

Also the Omicron does the same thing but the type is smaller each time. You should feel that having a reference to both a smaller type and a bigger type would make things messy. (That said, Omicron is the right way)

That is not the exact criteria that says why the definition should not be accepted but this explains why it feels wrong to me.

exptree seems like you are building a grammar for expressions, thing that generally aren't that recursive. Do you want some help with that?