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)?