The Coq mailing list

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

But this example is no longer positive. For all positive inductive types 
mu T, one can get the impredicative encoding with constructor and 
iterator in system F. One even only needs the existence of a "functorial 
action" of type forall A forall B. (A -> B) -> T A -> T B. Such a term 
can exists for trivial reasons even if A appears at negative positions 
in T A. But there may be no reasonable way to define a destructor. 
Similar observations can be made for system F^omega and inductive 
families, but there, the type of the "functorial action" has to be 
chosen properly since there are several possibilities, often with bad 
operational behaviour.

Ralph

Le 04/09/2014 18:45, Randy Pollack a écrit :
> Ralph Matthes wrote:
> [...] the very idea of such a constructor is already found in Section
> 4.3.2 of Christine Paulin's habilitation thesis of 1996).
>
> That's Chapter 4, Section 4.3.2 .
>
> Since Ralph brought up plain system F, recall that
>
> Definition lam: forall (X:Prop), ((X -> X)-> X) -> (X -> X -> X) -> X.
>
> checks in system F.  I'm echoing Thorsten in pointing this out.
> However, unlike strictly positive impredicative intersections, no
> constructor is definable for the "constructor" (X -> X)-> X.
>
> --Randy
>
> On Thu, Sep 4, 2014 at 10:27 AM, Ralph Matthes 
> <Ralph.Matthes AT irit.fr>
>  wrote:
> > 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?