The Coq mailing list

[Pierre-Evariste Dagand <pedagand AT gmail.com>]

Hi Edward!

> I thought it would be fun to port the Chapman-Dagand-McBride-Morris closed
> theory of datatypes to Coq. [1]  (I was on a plane and reading their recent
> ornaments paper [2], [...]

Looks like one of those 'torture taxi' I heard about. I should
emphasize more often that my papers are a dry alternative to
water-boarding :-)

> If we look at interp, it's easy to see: X is never used in a non
> strictly positive occurrence. But Coq seems to throw its hands up
> in the air and give up, when a Fixpoint is involved!

Which is fair enough, I guess: checking the positivity is part of the
TCB, so the simpler, the better.

> After which the authors proceed to convert the moral equivalent of interp
> into an inductive datatype all by itself, which is very not nice.

I'm not sure to understand your point about 'convert[ing] the moral
equivalent of interp to an inductive datatype by itself': muU is more
than interp, it is its unfolding when it's argument is 'mu D'. For
sure, we would love this unfolding to be avoided but how costly would
it be to extend the positivity checker to handle that? I don't know.
The Agda people might have a clue (these definitions go through in
Agda).

To summarize, here is what my intents were when writing this file: one
should define Desc as an Inductive, interp as a Fixpoint. This gives
you the endofunctors on Set, always a good thing to have. Then, one
should *refrain* from using interp to define the fixpoint: instead,
manually unfold 'interp' to build mu. This gives you MuU (the
construction is not new, I believe that Ralph Matthes used this sort
of impredicative encoding for his nested data-types). Finally, you
need to implement induction, etc. It should work out more or less
painfully, see the Agda model for inspiration.

I'm afraid that it's the best I have to offer. Still, if anyone has a
nicer solution, I'd be glad to hear it!


Out of curiosity, were you flying to Copenhagen? I'm there myself
right now, so if you want to talk about these things around a rotten
fish (local specialty, they said), feel free to get in touch.


Cheers,

-- 
Pierre-Evariste