The Coq mailing list

[Maxime Dénès <mail AT maximedenes.fr>]

Hi,

Indeed, that's what I meant by "in general".

Note that Coq doesn't allow positive types that are not strictly 
positive even when they are small, which probably makes it more 
conservative than it could be. On the other hand, I don't know if there 
are many use cases that are impacted.

Best,

Maxime.

On 09/04/2014 09:04 AM, Frédéric Blanqui wrote:
> Hello.
>
> Le 11/08/2014 23:23, Maxime Dénès a écrit :
> > Coq does reject non strictly positive types, even if they are 
> > positive. Otherwise it would be inconsistent in general, as you could 
> > encode the argument given in [1].
> Non-strictly positive types are not necessarily inconsistent. In 
> Inductively defined types 
> <http://dx.doi.org/10.1007/3-540-52335-9_47>, COLOG'88, Thierry 
> Coquand and Christine Paulin show that a particular "big" non-strictly 
> positive type is inconsistent (section 3.1, page 59). I call it "big" 
> for it has a constructor having a type argument that is not a 
> parameter. The constructor has type ((X->Prop)->Prop)->X. However, 
> "small" (e.g. replace Prop by bool) non-strictly positive types are 
> harmless.
>
> Best regards,
>
> Frédéric.
>
>
> > I don't know of any flag to disable this check but a patch should not 
> > be too hard to write. What's your use case?
> >
> > Maxime.
> >
> > [1] A new paradox in type theory, T. Coquand - Proceedings 9th Int. 
> > Congress of Logic, Methodology, 1991
> >
> > On 08/11/2014 05:04 PM, Luke Maurer wrote:
> > > AFAIK, Coq always accepts types that are positive but not strictly 
> > > so. And it never accepts non-positive occurrences (unlike with Agda, 
> > > Coq's termination checking is mandatory).
> > >
> > > - Luke
> > >
> > > > On Aug 11, 2014, at 1:54 PM, 
> > > > <elilobo.v AT gmail.com>
> > > >  wrote:
> > > >
> > > > How to force Coq to accept non-strictly positive inductive types? 
> > > > Is there a
> > > > flag like --no-positivity-check in Agda, to do it?