Getting rid of -XImpredicativeTypes

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
16 messages Options
Reply | Threaded
Open this post in threaded view
|

Getting rid of -XImpredicativeTypes

GHC - devs mailing list

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
Reply | Threaded
Open this post in threaded view
|

Re: Getting rid of -XImpredicativeTypes

Carter Schonwald
Sounds good to me. Such a change actually probably be good for reducing ghc support load around flags that don't work and increase reasons why using explicit type application will be awesome / more expressive than what I would otherwise be able to do with proxy arguments 


Tldr +1
A) reduces amount of community support load around unsupported flags 
B) makes visible type application extension meaningfully stronger / more powerful than proxy value approaches 

On Sunday, September 25, 2016, 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
Reply | Threaded
Open this post in threaded view
|

Re: Getting rid of -XImpredicativeTypes

Edward Z. Yang
In reply to this post by GHC - devs mailing list
A ghc-proposals is a good way to solicit feedback and publicize more
widely.  At least a proposal is worth it (and I am in favor of removing
ImpredicativeTypes, FWIW).

Edward

Excerpts from Simon Peyton Jones via ghc-devs's message of 2016-09-25 18:05:38 +0000:

> 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
Reply | Threaded
Open this post in threaded view
|

Re: Getting rid of -XImpredicativeTypes

Dan Doel
In reply to this post by GHC - devs mailing list
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



_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: Getting rid of -XImpredicativeTypes

Ben Gamari-2
In reply to this post by GHC - devs mailing list
Simon Peyton Jones via ghc-devs <[hidden email]> writes:

> 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.
>
Out of curiosity, what ever happened to the most recent attempt at
addressing impredicativity [1]?

As far as the proposal process is concerned, it would likely be a good
idea to put together a proposal so we have somewhere to collect
comments. That being said, it needn't be terribly lengthy given that we
are merely removing a feature.

Incidentally, that reminds me that I have some documentation fixes to
the ghc-proposals repository that I should proof-read and push.

Cheers,

- Ben


[1] https://ghc.haskell.org/trac/ghc/wiki/ImpredicativePolymorphism/Impredicative-2015

_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

signature.asc (482 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|

Re: Getting rid of -XImpredicativeTypes

Alejandro Serrano Mena


2016-09-26 9:00 GMT+02:00 Ben Gamari <[hidden email]>:
Simon Peyton Jones via ghc-devs <[hidden email]> writes:

> 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.
>
Out of curiosity, what ever happened to the most recent attempt at
addressing impredicativity [1]?

It turned our that the new system being proposed was not better than the current one. In particular, it was almost impossible to know upfront whether a program using impredicative types would need an annotation to typecheck. Furthermore, I think it would imply a humongous amount of changes to GHC, for not a very large gain.
 

As far as the proposal process is concerned, it would likely be a good
idea to put together a proposal so we have somewhere to collect
comments. That being said, it needn't be terribly lengthy given that we
are merely removing a feature.

Incidentally, that reminds me that I have some documentation fixes to
the ghc-proposals repository that I should proof-read and push.

Cheers,

- Ben


[1] https://ghc.haskell.org/trac/ghc/wiki/ImpredicativePolymorphism/Impredicative-2015

_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs



_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: Getting rid of -XImpredicativeTypes

Alejandro Serrano Mena
In reply to this post by GHC - devs mailing list
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 <[hidden email]>:

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



_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

RE: Getting rid of -XImpredicativeTypes

GHC - devs mailing list
In reply to this post by Dan Doel

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

 


_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

RE: Getting rid of -XImpredicativeTypes

GHC - devs mailing list
In reply to this post by Alejandro Serrano Mena

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:[hidden email]]
Sent: 26 September 2016 08:13
To: Simon Peyton Jones <[hidden email]>
Cc: [hidden email]; [hidden email]
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 <[hidden email]>:

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

 


_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: Getting rid of -XImpredicativeTypes

Baldur Blöndal
Shot in the dark: Would extensions like QuantifiedConstraints or ImplicationConstraints, if implemented, help with ImpredicativeTypes?

2016-09-30 15:29 GMT+00:00 Simon Peyton Jones via ghc-devs <[hidden email]>:

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:[hidden email]]
Sent: 26 September 2016 08:13
To: Simon Peyton Jones <[hidden email]>
Cc: [hidden email]; [hidden email]
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 <[hidden email]>:

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

 


_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs



_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: Getting rid of -XImpredicativeTypes

Richard Eisenberg-4

> On Sep 30, 2016, at 6:36 PM, Baldur Blöndal <[hidden email]> wrote:
>
> Shot in the dark: Would extensions like QuantifiedConstraints or ImplicationConstraints, if implemented, help with ImpredicativeTypes?

I don't think so. The challenge with ImpredicativeTypes is retaining predictability of type inference, and I don't see how implication constraints helps with this.

Richard

_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: Getting rid of -XImpredicativeTypes

Ganesh Sittampalam
In reply to this post by GHC - devs mailing list
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 [[hidden email]]
Sent: 26 September 2016 08:13
To: Simon Peyton Jones [hidden email]
Cc: [hidden email]; [hidden email]
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 <[hidden email]>:

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

 



_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs



_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: Getting rid of -XImpredicativeTypes

Carter Schonwald
On a more inane front,  does this give a path to either making $ less magical, or better user facing errors when folks use compose (.) style code instead and hit impredicativtity issues that $ magic would have handled ?

On Sunday, October 2, 2016, Ganesh Sittampalam <[hidden email]> wrote:
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 [<a href="javascript:_e(%7B%7D,&#39;cvml&#39;,&#39;trupill@gmail.com&#39;);" target="_blank">mailto:trupill@...]
Sent: 26 September 2016 08:13
To: Simon Peyton Jones <a href="javascript:_e(%7B%7D,&#39;cvml&#39;,&#39;simonpj@microsoft.com&#39;);" target="_blank"><simonpj@...>
Cc: <a href="javascript:_e(%7B%7D,&#39;cvml&#39;,&#39;ghc-users@haskell.org&#39;);" target="_blank">ghc-users@...; <a href="javascript:_e(%7B%7D,&#39;cvml&#39;,&#39;ghc-devs@haskell.org&#39;);" target="_blank">ghc-devs@...
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 <<a href="javascript:_e(%7B%7D,&#39;cvml&#39;,&#39;ghc-devs@haskell.org&#39;);" target="_blank">ghc-devs@...>:

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
<a href="javascript:_e(%7B%7D,&#39;cvml&#39;,&#39;ghc-devs@haskell.org&#39;);" target="_blank">ghc-devs@...
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

 



_______________________________________________
ghc-devs mailing list
<a href="javascript:_e(%7B%7D,&#39;cvml&#39;,&#39;ghc-devs@haskell.org&#39;);" target="_blank">ghc-devs@...
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs



_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: Getting rid of -XImpredicativeTypes

Ben Gamari-2
Carter Schonwald <[hidden email]> writes:

> On a more inane front,  does this give a path to either making $ less
> magical, or better user facing errors when folks use compose (.) style code
> instead and hit impredicativtity issues that $ magic would have handled ?
>
I don't believe this will have any effect on the behavior of ($). That
is, unless you don't mind giving up the ability to write runST $ do ...

Cheers,

- Ben

_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

signature.asc (482 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|

RE: Getting rid of -XImpredicativeTypes

GHC - devs mailing list
In reply to this post by Ganesh Sittampalam

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:[hidden email]]
Sent: 02 October 2016 12:07
To: Simon Peyton Jones <[hidden email]>; Alejandro Serrano Mena <[hidden email]>
Cc: [hidden email]; [hidden email]
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 [[hidden email]]
Sent: 26 September 2016 08:13
To: Simon Peyton Jones [hidden email]
Cc: [hidden email]; [hidden email]
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 <[hidden email]>:

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

 




_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

 


_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: Getting rid of -XImpredicativeTypes

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