The Coq mailing list

[Dan Doel <dan.doel AT gmail.com>]

It is possible to use positive (but non strict-positive) types to zip together two Church encoded lists in linear instead of quadratic time. Here is a (GHC) Haskell implementation:

---- snip ----

{-# LANGUAGE RankNTypes #-}

module ZipFold where

newtype List a = List { foldR :: forall r. (a -> r -> r) -> r -> r }

nil :: List a
nil = List $ \_ n -> n

cons :: a -> List a -> List a
cons x (List e) = List $ \c n -> x `c` e c n

toList :: List a -> [a]
toList xs = foldR xs (:) []

fromList :: [a] -> List a
fromList xs = List $ \c n -> foldr c n xs

-- The original idea:
-- newtype Left a b c = Left { feedLeft :: b -> Right a b c -> List c }
-- newtype Right a b c = Right { feedRight :: Left a b c -> List c }

newtype Zipping a b c = Z { feed :: (b -> Zipping a b c -> List c) -> List c }
type Left a b c = b -> Zipping a b c -> List c
type Right a b c = Zipping a b c

-- Mimicking the original idea
left :: (b -> Right a b c -> List c) -> Left a b c
left k = k
feedLeft :: Left a b c -> b -> Right a b c -> List c
feedLeft l = l

right :: (Left a b c -> List c) -> Right a b c
right = Z
feedRight :: Right a b c -> Left a b c -> List c
feedRight = feed

nilL :: Left a b c
nilL = left $ \_ _ -> nil

nilR :: Right a b c
nilR = right $ \_ -> nil

zipl :: (a -> b -> c) -> List a -> Left a b c
zipl f xs = foldR xs (\a l -> left $ \b r -> f a b `cons` feedRight r l) nilL

zipr :: List b -> Right a b c
zipr ys = foldR ys (\b r -> right $ \l -> feedLeft l b r) nilR

zipW :: (a -> b -> c) -> List a -> List b -> List c
zipW f xs ys = feedRight (zipr ys) (zipl f xs)

-- [(1,1), (2,2), ..., (10,10)]
ex1 = toList $ zipW (,) (fromList [1..10]) (fromList [1..10])
-- [(1,1), (2,2), ..., (9,9)]
ex2 = toList $ zipW (,) (fromList [1..10]) (fromList [1..9])
-- [(1,1), (2,2), ..., (9,9)]
ex3 = toList $ zipW (,) (fromList [1..9]) (fromList [1..10])

---- snip ----

Implementation in Coq/Agda/etc. is left as an exercise to the reader.

On Fri, Sep 5, 2014 at 5:26 AM, Thorsten Altenkirch <Thorsten.Altenkirch AT nottingham.ac.uk> wrote:

Sorry, I don¹t get it.

If you want to abstract over strictly positive types, you should abstract
over containers which are given by a shape : Set and a family positions :
shape -> Set, which give rise to fun X:Set => Sigma (s : S) (P xs -> X).

What is an example of a use of positive (but non strict positive)
inductive types? Please make it self-contained and short.

Thorsten

On 04/09/2014 20:11, "J. Ian Johnson" <ianj AT ccs.neu.edu> wrote:

>I have in mind that set and dict are the type constructors in Lescuyer's
>containers contrib's SetInterface and MapInterface. But they abstract
>over the concept of their respective containers, and that's the point.
>I hadn't checked the Var -> Closure example, since it's not what I would
>want to use (I can't recur over it). Apologies for the noise there.
>
>I don't have a solution, only a use case, that I would like to see strict
>positivity relaxed enough to allow mutual recursion through what could be
>classified as first-order containers (or first-order up to parametrically
>polymorphic contents). I don't know how to make this classification
>either :(
>-Ian
>----- Original Message -----
>From: "Maxime Dénès" <mail AT maximedenes.fr>
>To: coq-club AT inria.fr
>Sent: Thursday, September 4, 2014 2:36:23 PM GMT -05:00 US/Canada Eastern
>Subject: Re: [Coq-Club] Strictly positive inductive types
>
>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?
>>>>>>
>>>

This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please send it back to me, and immediately delete it.   Please do not use, copy or disclose the information contained in this message or in any attachment.  Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham.

This message has been checked for viruses but the contents of an attachment
may still contain software viruses which could damage your computer system, you are advised to perform your own checks. Email communications with the University of Nottingham may be monitored as permitted by UK legislation.