Getting rid of -XImpredicativeTypes
Ganesh Sittampalam
ganesh at earth.li
Mon Oct 3 22:36:08 UTC 2016
Oops, I completely missed you saying that despite reading your post
multiple times and actually quoting it. Sorry about that.
But yes, that makes it very clear, thanks. Doable, even if a pain in the
neck. The motivation for my question was that I vaguely recalled
encountering code that uses impredicative instantation when upgrading
darcs to support GHC 8.0. Using VTA will at least make it feasible to
migrate even if it requires CPP, so I'm no longer worried about having
to rewrite hurriedly.
Given the type inference problems, I appreciate it's better to just give
up than try to support something half baked.
On 03/10/2016 10:14, Simon Peyton Jones wrote:
> Indeed, as I said “I mis-spoke before: In my proposal we WILL allow
> types like (Tree (forall a. a->a))”.
>
>
>
> So yes, such types will be possible in type signatures (with
> ImpredicativeTypes). But using functions with such type signatures will
> be tiresome, because you’ll have to use VTA on every occasion. E.g. if
>
> xs :: [forall a. a->a]
>
>
>
> then you can’t say (reverse xs), because that requires impredicative
> instantiation of reverse’s type argument. You must stay
>
> reverse @(forall a. a->a) xs
>
>
>
> Does that help?
>
>
>
> Simon
>
>
>
> *From:*Ganesh Sittampalam [mailto:ganesh at earth.li]
> *Sent:* 02 October 2016 12:07
> *To:* Simon Peyton Jones <simonpj at microsoft.com>; Alejandro Serrano Mena
> <trupill at gmail.com>
> *Cc:* ghc-devs at haskell.org; ghc-users at haskell.org
> *Subject:* Re: Getting rid of -XImpredicativeTypes
>
>
>
> 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:trupill at gmail.com]
> *Sent:* 26 September 2016 08:13
> *To:* Simon Peyton Jones <simonpj at microsoft.com>
> <mailto:simonpj at microsoft.com>
> *Cc:* ghc-users at haskell.org <mailto:ghc-users at haskell.org>;
> ghc-devs at haskell.org <mailto:ghc-devs at 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 at haskell.org <mailto:ghc-devs at 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 at haskell.org <mailto:ghc-devs at 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 list
>
> ghc-devs at haskell.org <mailto:ghc-devs at 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%7C2a21525b2ae3432ba31e08d3eab43e4c%7C72f988bf86f141af91ab2d7cd011db47%7C1&sdata=Y9f9UGWEd1%2FHwNFLQx2XRrlk35gZeK7Sm2w1NBnU3FY%3D&reserved=0>
>
>
>
More information about the ghc-devs
mailing list