The Coq mailing list

[Ralph Matthes <Ralph.Matthes AT irit.fr>]

Maybe there are only very few use cases since there is no support. In 
plain system F, there is no problem at all with positive but not 
strictly positive inductive types. I exploited this in my TLCA 2001 
paper "Parigot's Second Order lambda-mu-Calculus and Inductive Types", 
with the inductive type #rho that has a constructor S of type ((#rho -> 
bot) -> bot) -> #rho (i.e., elimination of double negation - as I 
understood later, the very idea of such a constructor is already found 
in Section 4.3.2 of Christine Paulin's habilitation thesis of 1996). In 
system F^omega, one can have positive inductive families that are not 
recognized as strictly positive in the Coq system. There, this is not a 
question of being twice on the left of an arrow but rather of nesting of 
type transformations. This has been studied in several papers, in 
particular profoundly in "Iteration and coiteration schemes for 
higher-order and nested datatypes. Theor. Comput. Sci. 333(1-2): 3-66 
(2005)" by Andreas Abel, Tarmo Uustalu and myself.

I would be happy to see "natural" algorithmic examples involving 
non-strictly positive inductive types and families. As I wrote above, 
people might not be encouraged to search for them if tool support is 
missing.

Best,    Ralph


Le 04/09/2014 15:32, Maxime Dénès a écrit :
> 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?