The Coq mailing list

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

Hi,

On 09/04/2014 01:24 PM, J. Ian Johnson wrote:
> Non-strictly positive types are definitely a natural occurrence. I give this 
> example everywhere when I'm frustrated with Coq's limitations, so I'll give 
> it again.
>
> Closures. Closures are the pair of a lambda term and an explicit 
> substitution. A substitution is a finite function - a dictionary. You can't 
> define closures with an abstract dictionary due to the self-reference, even 
> though it's well-founded. You have to lock in a representation that will be a 
> pain to work with.
>
> Inductive Closure : Set :=
>   clos : Lam -> dict Variable Closure -> Closure.
>
> Say we decided to represent the finite function with just a function. This is 
> a positive but not strictly positive type.
>
> Inductive Closure : Set :=
>   clos : Lam -> (Variable -> Closure) -> Closure.

I'm probably missing something because your example is not 
self-contained, but why wouldn't it be strictly positive? The following 
is accepted by Coq:

Variable Lam : Set.
Variable Var : Set.

Inductive Closure : Set :=
 clos : Lam -> (Var -> Closure) -> Closure.

> More recently, I've been modeling a language for automatically abstracting reduction 
> semantics, where some values are allowed to be "external."
> An external value is a pair of an external space descriptor (contains 
> functions implementing important operations like join, equality, 
> cardinality), and a value of the type the descriptor states is the type of 
> that space's values.
>
> Operations for join, equality and cardinality all get the context of where 
> they're being called from, to make informed decisions, but this means a big 
> mutual recursive knot to tie, since states contain stores, which map to 
> values, of which external values are a member.
>
> I'd prefer to define the descriptor as a dependent record, but I can't.
> Inductive ExternalDescriptor : Set :=
>   ex_desc : forall t : Set, (* carrier type *)
>               (* join *) (State -> Store -> t -> t -> t) ->
>               (* equal *) (State -> Store -> t -> t -> EqRes) ->
>               (* cardinality *) (t -> AbsN) -> ExternalDescriptor
> with
> PreTerm : Set :=
> ...stuff...
> | External : forall E : ExternalDescriptor, match E with ex_desc t _ _ _ => t 
> end -> PreTerm (* oops, can't do induction/non-recursion *)
> with
> TAbs_ty : Set :=
> | TAbs : set PreTerm -> (* and some way to have a "dependent dictionary" of 
> external descriptors to values of the descriptor's carried type *) -> TAbs_ty
> with
> Term : Set :=
> pre : PreTerm -> Term
> | abs : TAbs_ty -> Term
> with
> EqRes : Set :=
>    Equal : set Refinement -> set (Term * Term) -> EqRes
> | Disequal : set Refinement -> set (Term * Term) -> EqRes
> | May : set (Term * Term) -> EqRes
> | Both : set Refinement -> set Refinement -> set (Term * Term) -> EqRes
> (* Term sets are to stop cyclic equality checking since terms can contain 
> pointers into the store. *)
> (* Also, can't have "set"s here in Coq, even though it's well-founded *)
> with Refinement := dict Address Term (* nope, not allowed *)
> with Store := dict Address TAbs_ty (* nope *).
>
> Just having an s-expression-like thing with sets or maps instead of lists is 
> just impossible in Coq. Also in OCaml because functors for maps or sets don't 
> make sense in a lot of cases.
> I'm pretty sure Agda's termination checker would also barf at this type too, 
> but I haven't tried it.

You seem to mix several issues here. When you say the termination 
checker, do you mean that you could define the type but not a fixpoint 
over it?

As for the definition of the type itself, it is very possible that the 
positivity checker is more restrictive than it could be, in particular 
with nested and mutual inductive types. On the other hand, your example 
is hard to follow because it is again not self contained: how is "set" 
defined? and "dict"?

The criterion used by Coq is syntactic, which makes it very hard to 
provide any useful hints without the precise definitions.

Best,

Maxime.

> -Ian
>
> ----- Original Message -----
> From: "Randy Pollack" 
> <rpollack AT inf.ed.ac.uk>
> To: "Coq-Club Club" 
> <coq-club AT inria.fr>
> Sent: Thursday, September 4, 2014 12:45:25 PM GMT -05:00 US/Canada Eastern
> Subject: Re: [Coq-Club] Strictly positive inductive types
>
> 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?