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:dan.d...@gmail.com]
Sent: 26 September 2016 00:54
To: Simon Peyton Jones <simo...@microsoft.com>
Cc: ghc-us...@haskell.org; ghc-d...@haskell.org
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 
<ghc-d...@haskell.org<mailto:ghc-d...@haskell.org>> 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
ghc-d...@haskell.org<mailto:ghc-d...@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%7Cf4d41103efc4487796c708d3e59f3720%7C72f988bf86f141af91ab2d7cd011db47%7C1&sdata=Ju37RVvZoNakCzz1dgTj%2F8mO9yz4ImbII14Hw%2FHWRpk%3D&reserved=0>

_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

Reply via email to