Getting rid of -XImpredicativeTypes
Simon Peyton Jones
simonpj at microsoft.com
Fri Sep 30 15:29:47 UTC 2016
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>
Cc: ghc-users at haskell.org; 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>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20160930/2f10afbe/attachment-0001.html>
More information about the ghc-devs
mailing list