The Coq mailing list

[Andrei Popescu <A.Popescu AT mdx.ac.uk>]

Greetings, 

It may be useful to point out how we resolved the problem (mutatis mutandis) in Isabelle/HOL, as discussed in the following papers: 

http://andreipopescu.uk/pdf/LICS2012.pdf 

http://andreipopescu.uk/pdf/codat-impl.pdf

Main idea: Incremental bookkeeping of additional structure for polymorphic types, which replaces the need for guessing the right predicates when nesting.        

For each datatype or codatatype, say, C, polymorphic in n arguments, we store additional information, including on how to lift any predicate from the component types to the type C: 

forall_C : forall U_1 ... U_n : Type. (U_1 -> Prop) -> ... -> (U_n -> Prop) -> C U_1 ... U_n -> Prop

This is essentially the unary relator associated to C. (In Isabelle/HOL, we actually use a different, set-based concept as primitive, but this is not important here.)

This way, a (co)datatype declaration that nests C will know how to induct/recurse through C. For example, if C is polymorphic in one argument, the declaration 

Inductive ty: Set :=
| tvar : id -> ty
| tpoly : id -> C ty -> ty

will produce something like this as an induction principle:

induct : 

  forall (P : ty -> Type) 

     (forall x : id. P (tvar x)) 

     (forall x : id, c : C ty. P x -> forall_C P c  -> P (tpoly x c))

     ->

     forall x, P x.  

If C is 'list', then forall_list gives the desired induction principle advocated on this thread. If the defined (co)datatype is itself polymorphic, then it will get its own 'forall' predicate, thus becoming smoothly nestable in further (co)datatypes. 

Please pardon my ignorance with Coq syntax -- I hope the idea is clear though.   

In the mentioned papers, we (like others on this thread) argue that reducing nested (co)datatypes to mutual (co)datatypes is far from ideal. This is because: 

(1) it breaks abstraction

(2) it doesn't scale to more complex nesting, in particular, doesn't work for nesting datatypes in codatatypes or vice versa. 

All the best, 

 Andrei