<html><head></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; color: rgb(0, 0, 0); font-size: 14px; font-family: Calibri, sans-serif;"><div><br></div><div><br></div><span id="OLK_SRC_BODY_SECTION"><blockquote style="margin:0 0 0 40px; border:none; padding:0px;"><div style="font-family:Calibri; font-size:11pt; text-align:left; color:black; BORDER-BOTTOM: medium none; BORDER-LEFT: medium none; PADDING-BOTTOM: 0in; PADDING-LEFT: 0in; PADDING-RIGHT: 0in; BORDER-TOP: #b5c4df 1pt solid; BORDER-RIGHT: medium none; PADDING-TOP: 3pt"><span style="font-weight:bold">From: </span> Dan Doel <<a href="mailto:dan.doel@gmail.com">dan.doel@gmail.com</a>><br><span style="font-weight:bold">Date: </span> Friday, 10 April 2015 21:41<br><span style="font-weight:bold">To: </span> Thorsten Altenkirch <<a href="mailto:thorsten.altenkirch@nottingham.ac.uk">thorsten.altenkirch@nottingham.ac.uk</a>><br><span style="font-weight:bold">Cc: </span> Frédéric Blanqui <<a href="mailto:frederic.blanqui@inria.fr">frederic.blanqui@inria.fr</a>>, "<a href="mailto:agda@lists.chalmers.se">agda@lists.chalmers.se</a>" <<a href="mailto:agda@lists.chalmers.se">agda@lists.chalmers.se</a>><br><span style="font-weight:bold">Subject: </span> Re: [Agda] Positive but not strictly positive types<br></div><div><br></div></blockquote><div dir="ltr"><blockquote style="margin:0 0 0 40px; border:none; padding:0px;"><div class="gmail_default" style="font-family:arial,helvetica,sans-serif">When you asked this in a coq-club thread on the same subject, I gave this example:</div></blockquote></div></span><div><br></div><div>Ah indeed, I thought this was a bit of a dejavue. I have to admit that I haven’t digested your code. I always thought that Church encodings are not very practical.</div><span id="OLK_SRC_BODY_SECTION"><div dir="ltr"><blockquote style="margin:0 0 0 40px; border:none; padding:0px;"><div class="gmail_default" style="font-family:arial,helvetica,sans-serif"><br><div class="gmail_default" style="font-family:arial,helvetica,sans-serif">It is possible to use <span class="">positive</span> (but non strict-<span class="">positive</span>) types to zip together two Church encoded lists in linear instead of quadratic time. Here is a (GHC) Haskell implementation:<br><br></div><div class="gmail_default" style="font-family:arial,helvetica,sans-serif">---- snip ----<br><br></div>{-# LANGUAGE RankNTypes #-}<br><br>module ZipFold where<br><br>newtype List a = List { foldR :: forall r. (a -> r -> r) -> r -> r }<br><br>nil :: List a<br>nil = List $ \_ n -> n<br><br>cons :: a -> List a -> List a<br>cons x (List e) = List $ \c n -> x `c` e c n<br><br>toList :: List a -> [a]<br>toList xs = foldR xs (:) []<br><br>fromList :: [a] -> List a<br>fromList xs = List $ \c n -> foldr c n xs<br><br>-- The original idea:<br>-- newtype Left a b c = Left { feedLeft :: b -> Right a b c -> List c }<br>-- newtype Right a b c = Right { feedRight :: Left a b c -> List c }<br><br>newtype Zipping a b c = Z { feed :: (b -> Zipping a b c -> List c) -> List c }<br>type Left a b c = b -> Zipping a b c -> List c<br>type Right a b c = Zipping a b c<br><br>-- Mimicking the original idea<br>left :: (b -> Right a b c -> List c) -> Left a b c<br>left k = k<br>feedLeft :: Left a b c -> b -> Right a b c -> List c<br>feedLeft l = l<br><br>right :: (Left a b c -> List c) -> Right a b c<br>right = Z<br>feedRight :: Right a b c -> Left a b c -> List c<br>feedRight = feed<br><br>nilL :: Left a b c<br>nilL = left $ \_ _ -> nil<br><br>nilR :: Right a b c<br>nilR = right $ \_ -> nil<br><br>zipl :: (a -> b -> c) -> List a -> Left a b c<br>zipl f xs = foldR xs (\a l -> left $ \b r -> f a b `cons` feedRight r l) nilL<br><br>zipr :: List b -> Right a b c<br>zipr ys = foldR ys (\b r -> right $ \l -> feedLeft l b r) nilR<br><br>zipW :: (a -> b -> c) -> List a -> List b -> List c<br>zipW f xs ys = feedRight (zipr ys) (zipl f xs)<br><br>-- [(1,1), (2,2), ..., (10,10)]<br>ex1 = toList $ zipW (,) (fromList [1..10]) (fromList [1..10])<br>-- [(1,1), (2,2), ..., (9,9)]<br>ex2 = toList $ zipW (,) (fromList [1..10]) (fromList [1..9])<br>-- [(1,1), (2,2), ..., (9,9)]<br>ex3 = toList $ zipW (,) (fromList [1..9]) (fromList [1..10])<br><br></div><div class="gmail_default" style="font-family:arial,helvetica,sans-serif">---- snip ----<br><br></div><div class="gmail_extra">I don't really understand what, "the only justification is classical," means. System F has non-strict positive types. Is it classical?</div></blockquote></div></span><div><br></div><div>I’d say so because the only justification for impredicativity is that Prop is small because Bool=Prop.</div><span id="OLK_SRC_BODY_SECTION"><div dir="ltr"><blockquote style="margin:0 0 0 40px; border:none; padding:0px;"><div class="gmail_extra"><br><span style="font-family: arial, helvetica, sans-serif;">I care about them inasmuch as I'd be interested in seeing a system that allowed them, so I could see what kinds of programs they'd be useful for, and what tradeoffs would have to be made to avoid breaking various properties of the system. From the above, it seems like they have uses when you're doing things with continuation passing.</span><br><div class="gmail_default" style="font-family:arial,helvetica,sans-serif"><br></div><div class="gmail_default" style="font-family:arial,helvetica,sans-serif">And if "justification" refers to the existence of some particular sort of model, I basically don't care about that at all. So positive types would automatically win that fight for me.<br></div></div></blockquote></div></span><div><br></div><div>If you just want to program you can switch off positivity checking.</div><div><br></div><div>I didn’t refer to “some sort of model” but just some naïve understanding. Strictly positive types model some sort of trees, I have no idea what non-strict positive one are. The justification seems just formalistic.</div><div><br></div><div>Usually we get non-strict positivity when we apply the negative translation (aka CPS translation) to an inductive (or coinductive) definition. It is not clear to my why those should exist from a constructive point of view.</div><div><br></div><div>Thorsten </div><div><br></div><div><br></div><span id="OLK_SRC_BODY_SECTION"><div dir="ltr"><blockquote style="margin:0 0 0 40px; border:none; padding:0px;"><div class="gmail_extra"><br>--<div class="gmail_default" style="font-family:arial,helvetica,sans-serif;display:inline"> Dan</div><br><br><div class="gmail_quote">On Fri, Apr 10, 2015 at 3:16 PM, Thorsten Altenkirch <span dir="ltr"><<a href="mailto:Thorsten.Altenkirch@nottingham.ac.uk" target="_blank">Thorsten.Altenkirch@nottingham.ac.uk</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Why do you want non-strict positive types? They don't make any sense to me. The only justification is classical.<br><br>
Thorsten<br><br>
Sent from my iPhone<br><div><div class="h5"><br>
> On 10 Apr 2015, at 18:22, Frédéric Blanqui <<a href="mailto:frederic.blanqui@inria.fr">frederic.blanqui@inria.fr</a>> wrote:<br>
><br>
> Hello.<br>
><br>
> Le 10/04/2015 17:19, Aaron Stump a écrit :<br>
>> Hello, Frédéric. Thanks for this interesting information about Coq.<br>
>> I have a couple follow-up questions if you don't mind:<br>
>><br>
>> -- So are you saying that Coq could allow nonstrictly positive small<br>
>> inductive types?<br>
> Yes. You can have a look at:<br>
> <a href="http://iospress.metapress.com/content/tf54nwg673hvgk5d/" target="_blank">http://iospress.metapress.com/content/tf54nwg673hvgk5d/</a><br>
> or <a href="https://who.rocq.inria.fr/Frederic.Blanqui/fi05-pdf.html" target="_blank">https://who.rocq.inria.fr/Frederic.Blanqui/fi05-pdf.html</a><br>
><br>
>> It seems it currently does not, as this one is rejected, for example:<br>
>><br>
>> Inductive Cont (A:Prop) : Prop :=<br>
>> D : Cont A<br>
>> | C : ((Cont A -> A) -> A) -> Cont A.<br>
> Unfortunately, yes, mainly for technical reasons I guess. This would<br>
> require to restrict pattern-matching definitions so that they can be<br>
> encoded into recursors, or upgrade the Coq termination checker to<br>
> size-based termination since the structural subterm ordering is defined<br>
> for strictly positive types only and cannot handle non-strictly positive<br>
> types...<br>
><br>
>> -- is it necessary to forbid large eliminations with big inductive<br>
>> types due to the Coquand-Paulin example we have been discussing (in<br>
>> addition to forbidding nonstrictly positive big inductive types)?<br>
>> Or is there another example that shows the problem with large<br>
>> eliminations and big inductive types?<br>
>> Sorry if these things are already explained somewhere in<br>
>> theories/Logic/ in the Coq library...<br>
> I know no other counter-example but current (sufficient) termination<br>
> conditions require so.<br>
><br>
> Frédéric.<br>
><br>
>> Thanks,<br>
>> Aaron<br>
>><br>
>>> On 04/10/2015 01:40 AM, Frédéric Blanqui wrote:<br>
>>> Hello.<br>
>>><br>
>>> Speaking of Coq: because Prop is impredicative, one usually<br>
>>> distinguishes between:<br>
>>> 1. small inductive types where Type-level constructor arguments are<br>
>>> parameters<br>
>>> 2. big inductive types<br>
>>><br>
>>> Coquand's counter-example is a big inductive type.<br>
>>><br>
>>> For this reason, strong elimination on big inductive types is<br>
>>> forbidden in Coq.<br>
>>><br>
>>> Adding small inductive types preserves termination and logical<br>
>>> consistency in system F or Fomega. A reference to Mendler's work has<br>
>>> already been given. For some more recent works, see Abel et al. More<br>
>>> generally, you can consider monotone types (positivity is a syntactic<br>
>>> condition ensuring monotony): see Matthes and Uustalu works. Adding<br>
>>> dependent types doesn't change anything.<br>
>>><br>
>>> So, there should be no problem in Agda.<br>
>>><br>
>>> Frédéric.<br>
>>><br>
>>><br>
>>> Le 09/04/2015 18:07, Vilhelm Sjöberg a écrit :<br>
>>>> On 2015-04-09 11:49, Andrés Sicard-Ramírez wrote:<br>
>>>>> Retaking the discussion in<br>
>>>>> <a href="http://thread.gmane.org/gmane.comp.lang.agda/6008" target="_blank">http://thread.gmane.org/gmane.comp.lang.agda/6008</a>, it's known that<br>
>>>>> using *negative* types it's possible<br>
>>>>><br>
>>>>> a) to prove absurdity or<br>
>>>>> b) to write non-terminating terms.<br>
>>>>><br>
>>>>> Is there some example in *Agda* of a positive but not strictly<br>
>>>>> positive type which allows a) or b)?<br>
>>>> I'm interested in the answer to this question also. If I correctly<br>
>>>> understand what Thierry Coquand wrote in the thread you mention, the<br>
>>>> answer is no; because Agda is predicative allowing positive<br>
>>>> datatypes would be sound. But it would be interesting to see this<br>
>>>> fleshed out more.<br>
>>>><br>
>>>> I wrote up a blog post about using non-strictly positive datatypes<br>
>>>> to get a paradox in Coq:<br>
>>>> <a href="http://vilhelms.github.io/posts/why-must-inductive-types-be-strictly-positive/" target="_blank">http://vilhelms.github.io/posts/why-must-inductive-types-be-strictly-positive/</a><br>
>>>><br>
>>>> Vilhelm<br>
>>>> _______________________________________________<br>
>>>> Agda mailing list<br>
>>>> <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
>>>> <a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
>>><br>
>>> _______________________________________________<br>
>>> Agda mailing list<br>
>>> <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
>>> <a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
><br>
> _______________________________________________<br>
> Agda mailing list<br>
> <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>> <a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br><br><br><br><br></div></div>This message and any attachment are intended solely for the addressee<br>
and may contain confidential information. If you have received this<br>
message in error, please send it back to me, and immediately delete it.<br><br>
Please do not use, copy or disclose the information contained in this<br>
message or in any attachment. Any views or opinions expressed by the<br>
author of this email do not necessarily reflect the views of the<br>
University of Nottingham.<br><br>
This message has been checked for viruses but the contents of an<br>
attachment may still contain software viruses which could damage your<br>
computer system, you are advised to perform your own checks. Email<br>
communications with the University of Nottingham may be monitored as<br>
permitted by UK legislation.<br><br><br>_______________________________________________<br>
Agda mailing list<br><a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br><a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br><br></blockquote></div><br></div></blockquote></div></span><PRE>
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.
</PRE></body></html>