[Agda] Positive but not strictly positive types
effectfully
effectfully at gmail.com
Sat Apr 11 01:35:00 CEST 2015
Dan Doel, then it's simpler to use Scott-encoded lists as an example:
{-# LANGUAGE Rank2Types #-}
import Data.Maybe
newtype List a = List { runList :: forall r. (List a -> a -> r -> r) -> r -> r }
snil :: List a
snil = List $ \_ z -> z
scons :: a -> List a -> List a
scons x xs = List $ \f z -> f xs x (runList xs f z)
split :: List a -> Maybe (a, List a)
split xs = runList xs (\t h _ -> Just (h, t)) Nothing
sfoldr :: (a -> r -> r) -> r -> List a -> r
sfoldr f z xs = runList xs (\_ -> f) z
szipWith :: (a -> a -> b) -> List a -> List a -> List b
szipWith f xs ys = fromMaybe snil $ do
(x, xs') <- split xs
(y, ys') <- split ys
return $ f x y `scons` szipWith f xs' ys'
szip = szipWith (,)
fromList :: [a] -> List a
fromList = foldr scons snil
toList :: List a -> [a]
toList = sfoldr (:) []
main = do
print $ toList $ szip (fromList [1..10]) (fromList [1..10])
-- [(1,1),(2,2),(3,3),(4,4),(5,5),(6,6),(7,7),(8,8),(9,9),(10,10)]
print $ toList $ szip (fromList [1..10]) (fromList [1..9 ])
-- [(1,1),(2,2),(3,3),(4,4),(5,5),(6,6),(7,7),(8,8),(9,9)]
print $ toList $ szip (fromList [1..9 ]) (fromList [1..10])
-- [(1,1),(2,2),(3,3),(4,4),(5,5),(6,6),(7,7),(8,8),(9,9)]
2015-04-11 0:41 GMT+04:00, Dan Doel <dan.doel at gmail.com>:
> When you asked this in a coq-club thread on the same subject, I gave this
> example:
>
> 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 ----
>
> I don't really understand what, "the only justification is classical,"
> means. System F has non-strict positive types. Is it classical?
>
> 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.
>
> 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.
>
> --
> Dan
>
>
> On Fri, Apr 10, 2015 at 3:16 PM, Thorsten Altenkirch <
> Thorsten.Altenkirch at nottingham.ac.uk> wrote:
>
>> Why do you want non-strict positive types? They don't make any sense to
>> me. The only justification is classical.
>>
>> Thorsten
>>
>> Sent from my iPhone
>>
>> > On 10 Apr 2015, at 18:22, Frédéric Blanqui <frederic.blanqui at inria.fr>
>> wrote:
>> >
>> > Hello.
>> >
>> > Le 10/04/2015 17:19, Aaron Stump a écrit :
>> >> Hello, Frédéric. Thanks for this interesting information about Coq.
>> >> I have a couple follow-up questions if you don't mind:
>> >>
>> >> -- So are you saying that Coq could allow nonstrictly positive small
>> >> inductive types?
>> > Yes. You can have a look at:
>> > http://iospress.metapress.com/content/tf54nwg673hvgk5d/
>> > or https://who.rocq.inria.fr/Frederic.Blanqui/fi05-pdf.html
>> >
>> >> It seems it currently does not, as this one is rejected, for example:
>> >>
>> >> Inductive Cont (A:Prop) : Prop :=
>> >> D : Cont A
>> >> | C : ((Cont A -> A) -> A) -> Cont A.
>> > Unfortunately, yes, mainly for technical reasons I guess. This would
>> > require to restrict pattern-matching definitions so that they can be
>> > encoded into recursors, or upgrade the Coq termination checker to
>> > size-based termination since the structural subterm ordering is defined
>> > for strictly positive types only and cannot handle non-strictly
>> > positive
>> > types...
>> >
>> >> -- is it necessary to forbid large eliminations with big inductive
>> >> types due to the Coquand-Paulin example we have been discussing (in
>> >> addition to forbidding nonstrictly positive big inductive types)?
>> >> Or is there another example that shows the problem with large
>> >> eliminations and big inductive types?
>> >> Sorry if these things are already explained somewhere in
>> >> theories/Logic/ in the Coq library...
>> > I know no other counter-example but current (sufficient) termination
>> > conditions require so.
>> >
>> > Frédéric.
>> >
>> >> Thanks,
>> >> Aaron
>> >>
>> >>> On 04/10/2015 01:40 AM, Frédéric Blanqui wrote:
>> >>> Hello.
>> >>>
>> >>> Speaking of Coq: because Prop is impredicative, one usually
>> >>> distinguishes between:
>> >>> 1. small inductive types where Type-level constructor arguments are
>> >>> parameters
>> >>> 2. big inductive types
>> >>>
>> >>> Coquand's counter-example is a big inductive type.
>> >>>
>> >>> For this reason, strong elimination on big inductive types is
>> >>> forbidden in Coq.
>> >>>
>> >>> Adding small inductive types preserves termination and logical
>> >>> consistency in system F or Fomega. A reference to Mendler's work has
>> >>> already been given. For some more recent works, see Abel et al. More
>> >>> generally, you can consider monotone types (positivity is a syntactic
>> >>> condition ensuring monotony): see Matthes and Uustalu works. Adding
>> >>> dependent types doesn't change anything.
>> >>>
>> >>> So, there should be no problem in Agda.
>> >>>
>> >>> Frédéric.
>> >>>
>> >>>
>> >>> Le 09/04/2015 18:07, Vilhelm Sjöberg a écrit :
>> >>>> On 2015-04-09 11:49, Andrés Sicard-Ramírez wrote:
>> >>>>> Retaking the discussion in
>> >>>>> http://thread.gmane.org/gmane.comp.lang.agda/6008, it's known that
>> >>>>> using *negative* types it's possible
>> >>>>>
>> >>>>> a) to prove absurdity or
>> >>>>> b) to write non-terminating terms.
>> >>>>>
>> >>>>> Is there some example in *Agda* of a positive but not strictly
>> >>>>> positive type which allows a) or b)?
>> >>>> I'm interested in the answer to this question also. If I correctly
>> >>>> understand what Thierry Coquand wrote in the thread you mention, the
>> >>>> answer is no; because Agda is predicative allowing positive
>> >>>> datatypes would be sound. But it would be interesting to see this
>> >>>> fleshed out more.
>> >>>>
>> >>>> I wrote up a blog post about using non-strictly positive datatypes
>> >>>> to get a paradox in Coq:
>> >>>>
>> http://vilhelms.github.io/posts/why-must-inductive-types-be-strictly-positive/
>> >>>>
>> >>>> Vilhelm
>> >>>> _______________________________________________
>> >>>> Agda mailing list
>> >>>> Agda at lists.chalmers.se
>> >>>> https://lists.chalmers.se/mailman/listinfo/agda
>> >>>
>> >>> _______________________________________________
>> >>> Agda mailing list
>> >>> Agda at lists.chalmers.se
>> >>> https://lists.chalmers.se/mailman/listinfo/agda
>> >
>> > _______________________________________________
>> > Agda mailing list
>> > Agda at lists.chalmers.se
>> > https://lists.chalmers.se/mailman/listinfo/agda
>>
>>
>>
>>
>> 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.
>>
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>>
>
More information about the Agda
mailing list