RE: Getting rid of -XImpredicativeTypes

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
1 message Options
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

RE: Getting rid of -XImpredicativeTypes

Haskell - Glasgow-haskell-users mailing list

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.

 

2) There was a sketch drawn up around a year ago (I think) aiming to actually fix ImpredicativeTypes. I don't recall who was working on it, but I think when I mentioned it in the context of something else, you didn't seem to be aware of it. I guess it's safe to say that nothing ever came of it, at least inasmuch as no one ever showed you their proposal for a properly functioning ImpredicativeTypes?

It’s just a swamp.  I have tried multiple times to fix ImpredicativeTypes, and failed every time.  Which is not to say that someone shouldn’t try again, with new thinking.

 

Simon

 

From: Dan Doel [mailto:[hidden email]]
Sent: 26 September 2016 00:54
To: Simon Peyton Jones <[hidden email]>
Cc: [hidden email]; [hidden email]
Subject: Re: Getting rid of -XImpredicativeTypes

 

I don't use the extension, because it's more pleasant to use newtypes with polymorphic contents. But here are some questions:

1) ImpredicativeTypes enables types like `Maybe (forall a. a)`. Do those just disappear, or are they also enabled anyway? (I would guess the former.)

2) There was a sketch drawn up around a year ago (I think) aiming to actually fix ImpredicativeTypes. I don't recall who was working on it, but I think when I mentioned it in the context of something else, you didn't seem to be aware of it. I guess it's safe to say that nothing ever came of it, at least inasmuch as no one ever showed you their proposal for a properly functioning ImpredicativeTypes?

Anyhow, if it can't be fixed, I think not having the extension is superior to its current state. And really, I think even if fixing it were on the roadmap, it'd be better to get rid of it until it were actually fixed.

-- Dan

 

On Sun, Sep 25, 2016 at 2:05 PM, Simon Peyton Jones via ghc-devs <[hidden email]> wrote:

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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

 


_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
Loading...