On a more inane front, does this give a path to either making $ less magical, or better user facing errors when folks use compose (.) style code instead and hit impredicativtity issues that $ magic would have handled ?
On Sunday, October 2, 2016, Ganesh Sittampalam <gan...@earth.li> wrote: > Elsewhere in the thread, you said > > 1) ImpredicativeTypes enables types like `Maybe (forall a. a)`. Do those > just disappear, or are they also enabled anyway? (I would guess the former.) > Yes, they’d disappear. > > > but here you're talking about 'xs :: [forall a . a->a]' being possible > with VTA - is the idea that such types will be possible but only with both > explicit signatures and VTA? > > On 30/09/2016 16:29, Simon Peyton Jones via ghc-devs wrote: > > Alejandro: excellent point. I mis-spoke before. In my proposal we WILL > allow types like (Tree (forall a. a->a)). > > > > I’m trying to get round to writing a proposal (would someone else like to > write it – it should be short), but the idea is this: > > > > *When you have -XImpredicativeTypes* > > · *You can write a polytype in a visible type argument; eg. f > @(forall a. a->a)* > > · *You can write a polytype as an argument of a type in a > signature e.g. f :: [forall a. a->a] -> Int* > > > > *And that’s all. A unification variable STILL CANNOT be unified with a > polytype. The only way you can call a polymorphic function at a polytype > is to use Visible Type Application.* > > > > *So using impredicative types might be tiresome. E.g.* > > * type SID = forall a. a->a* > > > > * xs :: [forall a. a->a]* > > * xs = (:) @SID id ( (:) @SID id ([] @ SID))* > > > > *In short, if you call a function at a polytype, you must use VTA. > Simple, easy, predictable; and doubtless annoying. But possible*. > > > > Simon > > > > *From:* Alejandro Serrano Mena [mailto:trup...@gmail.com > <javascript:_e(%7B%7D,'cvml','trup...@gmail.com');>] > *Sent:* 26 September 2016 08:13 > *To:* Simon Peyton Jones <simo...@microsoft.com> > <javascript:_e(%7B%7D,'cvml','simo...@microsoft.com');> > *Cc:* ghc-us...@haskell.org > <javascript:_e(%7B%7D,'cvml','ghc-us...@haskell.org');>; > ghc-devs@haskell.org > <javascript:_e(%7B%7D,'cvml','ghc-devs@haskell.org');> > *Subject:* Re: Getting rid of -XImpredicativeTypes > > > > What would be the story for the types of the arguments. Would I be allowed > to write the following? > > > f (lst :: [forall a. a -> a]) = head @(forall a. a -> a) lst 3 > > Regards, > > Alejandro > > > > 2016-09-25 20:05 GMT+02:00 Simon Peyton Jones via ghc-devs < > ghc-devs@haskell.org > <javascript:_e(%7B%7D,'cvml','ghc-devs@haskell.org');>>: > > Friends > > > > GHC has a flag -XImpredicativeTypes that makes a half-hearted attempt to > support impredicative polymorphism. But it is vestigial…. if it works, > it’s really a fluke. We don’t really have a systematic story here at all. > > > > I propose, therefore, to remove it entirely. That is, if you use > -XImpredicativeTypes, you’ll get a warning that it does nothing (ie. > complete no-op) and you should remove it. > > > > Before I pull the trigger, does anyone think they are using it in a > mission-critical way? > > > > Now that we have Visible Type Application there is a workaround: if you > want to call a polymorphic function at a polymorphic type, you can > explicitly apply it to that type. For example: > > > > {-# LANGUAGE ImpredicativeTypes, TypeApplications, RankNTypes #-} > > module Vta where > > f x = id @(forall a. a->a) id @Int x > > > > You can also leave out the @Int part of course. > > > > Currently we have to use -XImpredicativeTypes to allow the @(forall a. > a->a). Is that sensible? Or should we allow it regardless? I rather > think the latter… if you have Visible Type Application (i.e. > -XTypeApplications) then applying to a polytype is nothing special. So I > propose to lift that restriction. > > > > I should go through the GHC Proposals Process for this, but I’m on a > plane, so I’m going to at least start with an email. > > > > Simon > > > _______________________________________________ > ghc-devs mailing list > ghc-devs@haskell.org > <javascript:_e(%7B%7D,'cvml','ghc-devs@haskell.org');> > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs > <https://na01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fmail.haskell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc-devs&data=01%7C01%7Csimonpj%40microsoft.com%7Cd4eb1fd61d0148cea9f508d3e5dca6fe%7C72f988bf86f141af91ab2d7cd011db47%7C1&sdata=ZM3djztmpA09J6x1DmmV0LEeftsA1FhjPhjwLuG5w%2FE%3D&reserved=0> > > > > > _______________________________________________ > ghc-devs mailing listghc-d...@haskell.org > <javascript:_e(%7B%7D,'cvml','ghc-devs@haskell.org');>http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs > > >
_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs