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:[email protected]]
Sent: 02 October 2016 12:07
To: Simon Peyton Jones <[email protected]>; Alejandro Serrano Mena
<[email protected]>
Cc: [email protected]; [email protected]
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:[email protected]]
Sent: 26 September 2016 08:13
To: Simon Peyton Jones <[email protected]><mailto:[email protected]>
Cc: [email protected]<mailto:[email protected]>;
[email protected]<mailto:[email protected]>
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
<[email protected]<mailto:[email protected]>>:
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
[email protected]<mailto:[email protected]>
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
[email protected]<mailto:[email protected]>
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>
_______________________________________________
ghc-devs mailing list
[email protected]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
