The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

On 27/09/2013 10:03, David Monniaux wrote:
> Let us now try to generalize this to binary constructors, like with a
> datatype Bin with A as leaf and C as binary constructor.
> Bin ~ (unit + Bin*Bin), then (Bin -> X) ~ (unit * ((Bin*Bin)->X)) ~
> (unit * (Bin->(Bin->X))) by currying.
> 
> This yields
> (foo X) ~ X * (foo (foo X))
> 
> Thus the declaration:
> 
> CoInductive foo (X : Type) :=
>   | Moo : X -> (foo (foo X)) -> foo X.
> 
> But then I get:
> 
> Error: Non strictly positive occurrence of "foo" in
>  "X -> foo (foo X) -> foo X".
> 
> Isn't this check a bit too strict? My remembrances on the positivity
> check in (co)inductive datatypes is hazy, but I don't see how this
> construction could create inconsistencies.

[Disclaimer: this is pure hand-waving.]

Although your type seems quite legit, your analogy through isomorphism
does not. Indeed, coinductives introduce lazy-like behaviour to prevent
infinite reductions. Looks like a (co)monad M somehow, similarly to Agda
coinductive connectives.

Then (Bin * Bin) -> M X is definitely not the same thing as (Bin -> M
(Bin -> M X)). I assume that in the coinductive cases, this matters...

PMP

P.S. : The defect of the positivity condition checker is another issue...

Attachment: signature.asc
Description: OpenPGP digital signature