Re: New implementation for `ImpredicativeTypes`

[John Ericson]

On 9/7/21 8:41 PM, Richard Eisenberg wrote:



On Sep 6, 2021, at 11:21 AM, John Ericson 
> wrote:


On 9/2/21 11:04 PM, Richard Eisenberg wrote:

On Sep 2, 2021, at 2:56 PM, john.ericson 
> wrote:


Does the most basic e.g.

newtype Some f where
  MkSome :: forall a. f a -> Some f

Have one of those problematic equalities?


No. That's not a GADT -- the constructor doesn't restrict anything 
about `f`.


Morally, sure, but GHC doesn't know about this.



Sure it does -- GHC doesn't include an equality constraint as one of 
the fields of MkSome. This isn't about extensions -- it's about the 
way the data constructor is interpreted.


Oops, agreed. I guess meant extensions didn't seem to check for this in 
a really syntax-driven way. But yes deciding the cases apart is not hard 
once the data definition is compiled.




I think you're after newtype existentials. I think these should 
indeed be possible, because what you propose appears to be the same as


newtype Some f = MkSome (exists a. f a)

We can probably support the syntax you wrote, too, but I don't want 
to commit to that right now.


The syntax I wrote is already basically valid?

data Some f = forall a. Some (f a)
data Some f where MkSome :: forall a f. f a -> Some f

Is accepted

newtype Some f = forall a. Some (f a)
newtype Some f where MkSome :: forall a f. f a -> Some f

Is not with "A newtype constructor cannot have existential type 
variables"


I propose we teach GHC how these "GADTs" in fact merely have 
existential variables, and not the FC constraints that require the 
extra evaluation for soundness. Than we can get the 
operational/runtime benefits of what you propose for cheap. Don't get 
me wrong -- the other aspects in the paper this doesn't address are 
still quite valuable, but I think this is a useful stepping stone / 
removal of artificial restrictions we should do first.


This sort of thing is brought up in #1965, where it is alleged this 
is in fact more difficult than it sounds. All more reason it is a 
good stepping stone, I say!




This is more difficult than it sounds. :) Newtypes are implemented via 
coercions in Core, and coercions are inherently bidirectional. The 
appearance of an existential in this way requires one-way conversions, 
which are currently not supported. So, to get what you want, we'd have 
to modify the core language as in the existentials paper, along with 
some extra work to automatically add `pack` and `open` -- rather 
similar to the type inference described in the existentials paper. The 
bottom line for me is that this seems just as hard as implementing the 
whole thing, so I see no value in having the stepping stone. If we 
always wrote out the newtype constructor, then maybe we could use its 
appearance to guide the `pack` and `open` but we don't: sometimes, we 
just use `coerce`. So I really don't think this is any easier than 
implementing the paper as written. Once that's done, we can come back 
and add this new feature relatively easily (I think).

Makes sense. That route is indeed harder than I was thinking.

There was a time before coercions when I gather newtypes were mostly 
implemented with a special-case lowering to STG. I imagine it would be 
quite easy to implement this that way, but that door is now mostly shut.


I had a few more thoughts, but I am not sure if I should trouble the 
list with them as they are still a bit rough around the edges. Suffice 
to say, I hope we could sort of "smooth out" the feature space a bit so 
that these and GADTs are not completely different, e.g. I think all 
existential variables can be projected like this (I opened #20337 for 
this), and perhaps connect GADTs to the existentials with evidence you 
mention in the "future work" section, so "true" GADTs also have 
structural counterparts in a similar way.


Happy to just continue mulling on it until a proposal or something, 
however. :)


John

___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: New implementation for `ImpredicativeTypes`

[Richard Eisenberg]

> On Sep 6, 2021, at 11:21 AM, John Ericson  
> wrote:
> 
> On 9/2/21 11:04 PM, Richard Eisenberg wrote:
> 
>> On Sep 2, 2021, at 2:56 PM, john.ericson > > wrote:
>>> 
>>> Does the most basic e.g.
>>> 
>>> newtype Some f where
>>>   MkSome :: forall a. f a -> Some f
>>> 
>>> Have one of those problematic equalities?
>> 
>> No. That's not a GADT -- the constructor doesn't restrict anything about `f`.
> Morally, sure, but GHC doesn't know about this.
> 

Sure it does -- GHC doesn't include an equality constraint as one of the fields 
of MkSome. This isn't about extensions -- it's about the way the data 
constructor is interpreted.
>> 
>> I think you're after newtype existentials. I think these should indeed be 
>> possible, because what you propose appears to be the same as
>> 
>> newtype Some f = MkSome (exists a. f a)
>> 
>> We can probably support the syntax you wrote, too, but I don't want to 
>> commit to that right now.
> The syntax I wrote is already basically valid?
> 
> data Some f = forall a. Some (f a)
> data Some f where MkSome :: forall a f. f a -> Some f
> Is accepted
> 
> newtype Some f = forall a. Some (f a)
> newtype Some f where MkSome :: forall a f. f a -> Some f
> Is not with "A newtype constructor cannot have existential type variables"
> 
> I propose we teach GHC how these "GADTs" in fact merely have existential 
> variables, and not the FC constraints that require the extra evaluation for 
> soundness. Than we can get the operational/runtime benefits of what you 
> propose for cheap. Don't get me wrong -- the other aspects in the paper this 
> doesn't address are still quite valuable, but I think this is a useful 
> stepping stone / removal of artificial restrictions we should do first.
> 
> This sort of thing is brought up in #1965, where it is alleged this is in 
> fact more difficult than it sounds. All more reason it is a good stepping 
> stone, I say!
> 

This is more difficult than it sounds. :) Newtypes are implemented via 
coercions in Core, and coercions are inherently bidirectional. The appearance 
of an existential in this way requires one-way conversions, which are currently 
not supported. So, to get what you want, we'd have to modify the core language 
as in the existentials paper, along with some extra work to automatically add 
`pack` and `open` -- rather similar to the type inference described in the 
existentials paper. The bottom line for me is that this seems just as hard as 
implementing the whole thing, so I see no value in having the stepping stone. 
If we always wrote out the newtype constructor, then maybe we could use its 
appearance to guide the `pack` and `open`, but we don't: sometimes, we just use 
`coerce`. So I really don't think this is any easier than implementing the 
paper as written. Once that's done, we can come back and add this new feature 
relatively easily (I think).

Richard

> John
> 

___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: New implementation for `ImpredicativeTypes`

[John Ericson]

On 9/2/21 11:04 PM, Richard Eisenberg wrote:

On Sep 2, 2021, at 2:56 PM, john.ericson 
mailto:john.ericson@obsidian.systems>> 
wrote:


Does the most basic e.g.

newtype Some f where
  MkSome :: forall a. f a -> Some f

Have one of those problematic equalities?


No. That's not a GADT -- the constructor doesn't restrict anything 
about `f`.


Morally, sure, but GHC doesn't know about this.

I tried, and -XGADTSyntax + -XExistenialTypes = -XGADTs it seems.



I think you're after newtype existentials. I think these should indeed 
be possible, because what you propose appears to be the same as


newtype Some f = MkSome (exists a. f a)

We can probably support the syntax you wrote, too, but I don't want to 
commit to that right now.


The syntax I wrote is already basically valid?

data Some f = forall a. Some (f a)

data Some f where MkSome :: forall a f. f a -> Some f

Is accepted

newtype Some f = forall a. Some (f a)

newtype Some f where MkSome :: forall a f. f a -> Some f

Is not with "A newtype constructor cannot have existential type variables"

I propose we teach GHC how these "GADTs" in fact merely have existential 
variables, and not the FC constraints that require the extra evaluation 
for soundness. Than we can get the operational/runtime benefits of what 
you propose for cheap. Don't get me wrong -- the other aspects in the 
paper this doesn't address are still quite valuable, but I think this is 
a useful stepping stone / removal of artificial restrictions we should 
do first.


This sort of thing is brought up in #1965, where it is alleged this is 
in fact more difficult than it sounds. All more reason it is a good 
stepping stone, I say!


John

___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: New implementation for `ImpredicativeTypes`

[Richard Eisenberg]

> On Sep 2, 2021, at 2:56 PM, john.ericson  
> wrote:
> 
> Does the most basic e.g.
> 
> newtype Some f where
>   MkSome :: forall a. f a -> Some f
> 
> Have one of those problematic equalities?

No. That's not a GADT -- the constructor doesn't restrict anything about `f`.

I think you're after newtype existentials. I think these should indeed be 
possible, because what you propose appears to be the same as

newtype Some f = MkSome (exists a. f a)

We can probably support the syntax you wrote, too, but I don't want to commit 
to that right now.

Richard

> 
> 
>  On Thu, 02 Sep 2021 14:33:40 -0400 li...@richarde.dev wrote 
> 
> 
> 
> On Sep 2, 2021, at 2:10 PM, Alex Rozenshteyn  <mailto:rpglove...@gmail.com>> wrote:
> 
> Oh, I see. That's because this would need to introduce `pack ... as ...` and 
> `open ...` into the core term language, right?
> 
> Exactly, yes.
> 
> 
> My sense is that it shouldn't negatively affect runtime performance of 
> programs without existentials even if implemented naively; does that seem 
> accurate? Not that implementing it, even naively, is a small task. 
> 
> I would agree with this, too.
> 
> On Sep 2, 2021, at 2:21 PM, john.ericson  <mailto:john.ericson@obsidian.systems>> wrote:
> 
> This reminds me...can we do newtype GADTs in certain situations as a stepping 
> stone? I would think that would be purely easier — more nominal, no nice 
> projections but only `case` and skolems which cannot escape.
> 
> Newtype GADTs we're long deemed impossible IIRC, but surely the paper 
> demonstrates that at least some cases should work?
> 
> I don't quite see how this relates to existentials. Note that the paper does 
> not address e.g. packing equalities in existentials, which would be needed 
> for interacting with GADTs.
> 
> Glad folks are enjoying the paper! :)
> 
> Richard
> 
> 
> 
>  On Thu, 02 Sep 2021 14:10:34 -0400 rpglove...@gmail.com 
> <mailto:rpglove...@gmail.com> wrote 
> 
> Oh, I see. That's because this would need to introduce `pack ... as ...` and 
> `open ...` into the core term language, right?
> 
> My sense is that it shouldn't negatively affect runtime performance of 
> programs without existentials even if implemented naively; does that seem 
> accurate? Not that implementing it, even naively, is a small task. 
> 
> On Thu, Sep 2, 2021 at 1:44 PM Simon Peyton Jones  <mailto:simo...@microsoft.com>> wrote:
> Of course not. The same was true for QuickLook, though, wasn't it?
> 
> No, not at all.   QuickLook required zero changes to GHC’s intermediate 
> language – it impacted only the type inference system.   Adding existentials 
> will entail a substantial change to the intermediate language, affecting 
> every optimisation pass.
> 
>  
> 
> Simon
> 
>  
> 
> From: Alex Rozenshteyn mailto:rpglove...@gmail.com>> 
> Sent: 02 September 2021 18:13
> To: Simon Peyton Jones mailto:simo...@microsoft.com>>
> Cc: GHC developers mailto:ghc-devs@haskell.org>>
> Subject: Re: New implementation for `ImpredicativeTypes`
> 
>  
> 
> So it’s not just a question of saying “just add that paper to GHC and voila 
> job done”. 
> 
>  
> 
> Of course not. The same was true for QuickLook, though, wasn't it?
> 
>  
> 
> On Thu, Sep 2, 2021 at 12:42 PM Simon Peyton Jones  <mailto:simo...@microsoft.com>> wrote:
> 
> If I understand correctly, the recent ICFP paper "An Existential Crisis 
> Resolved 
> <https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fdl.acm.org%2Fdoi%2Fpdf%2F10.1145%2F3473569=04%7C01%7Csimonpj%40microsoft.com%7Cc0f0a66e10f94a6f17d508d96e34f2ae%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637661997328916809%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000=kioGsomPn8BuvBLQx6KEr5glMTPvw6m93DK%2BGA0lM08%3D=0>"
>  finally enables this; is that right?
> 
> It describes one way to include existentials in GHC’s intermediate language, 
> which is a real contribution. But it is not a small change.  So it’s not just 
> a question of saying “just add that paper to GHC and voila job done”.
> 
>  
> 
> Simon
> 
>  
> 
> From: Alex Rozenshteyn mailto:rpglove...@gmail.com>> 
> Sent: 02 September 2021 17:10
> To: Simon Peyton Jones mailto:simo...@microsoft.com>>
> Cc: GHC developers mailto:ghc-devs@haskell.org>>
> Subject: Re: New implementation for `ImpredicativeTypes`
> 
>  
> 
> If I understand correctly, the recent ICFP paper "An Existential Crisis 
> Resolved 
> <https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fdl.acm.org%2Fdoi%2Fpdf%2

Re: New implementation for `ImpredicativeTypes`

[john.ericson]

Does the most basic e.g.newtype Some f where  MkSome :: forall a. f a -> Some 
fHave one of those problematic equalities?  On Thu, 02 Sep 2021 14:33:40 
-0400  li...@richarde.dev  wrote On Sep 2, 2021, at 2:10 PM, Alex 
Rozenshteyn  wrote:Oh, I see. That's because this would 
need to introduce `pack ... as ...` and `open ...` into the core term language, 
right?Exactly, yes.My sense is that it shouldn't negatively affect runtime 
performance of programs without existentials even if implemented naively; does 
that seem accurate? Not that implementing it, even naively, is a small task. I 
would agree with this, too.On Sep 2, 2021, at 2:21 PM, john.ericson 
 wrote:This reminds me...can we do newtype GADTs 
in certain situations as a stepping stone? I would think that would be purely 
easier — more nominal, no nice projections but only `case` and skolems which 
cannot escape.Newtype GADTs we're long deemed impossible IIRC, but surely the 
paper demonstrates that at least some cases should work?I don't quite see how 
this relates to existentials. Note that the paper does not address e.g. packing 
equalities in existentials, which would be needed for interacting with 
GADTs.Glad folks are enjoying the paper! :)Richard On Thu, 02 Sep 2021 
14:10:34 -0400 rpglove...@gmail.com wrote Oh, I see. That's because this 
would need to introduce `pack ... as ...` and `open ...` into the core term 
language, right?My sense is that it shouldn't negatively affect runtime 
performance of programs without existentials even if implemented naively; does 
that seem accurate? Not that implementing it, even naively, is a small task. On 
Thu, Sep 2, 2021 at 1:44 PM Simon Peyton Jones  wrote:Of 
course not. The same was true for QuickLook, though, wasn't it?No, not at all.  
 QuickLook required zero changes to GHC’s intermediate language – it impacted 
only the type inference system.   Adding existentials will entail a substantial 
change to the intermediate language, affecting every optimisation pass. Simon 
From: Alex Rozenshteyn  Sent: 02 September 2021 18:13To: 
Simon Peyton Jones Cc: GHC developers 
Subject: Re: New implementation for `ImpredicativeTypes` 
So it’s not just a question of saying “just add that paper to GHC and voila job 
done”.  Of course not. The same was true for QuickLook, though, wasn't it? On 
Thu, Sep 2, 2021 at 12:42 PM Simon Peyton Jones  
wrote:If I understand correctly, the recent ICFP paper "An Existential Crisis 
Resolved" finally enables this; is that right?It describes one way to include 
existentials in GHC’s intermediate language, which is a real contribution. But 
it is not a small change.  So it’s not just a question of saying “just add that 
paper to GHC and voila job done”. Simon From: Alex Rozenshteyn 
 Sent: 02 September 2021 17:10To: Simon Peyton Jones 
Cc: GHC developers Subject: Re: 
New implementation for `ImpredicativeTypes` If I understand correctly, the 
recent ICFP paper "An Existential Crisis Resolved" finally enables this; is 
that right? On Mon, Sep 9, 2019 at 12:00 PM Simon Peyton Jones 
 wrote:Suppose Haskell did have existentials; Yes, I 
think that’s an interesting thing to work on!  I’m not sure what the 
implications would be.  At very least we’d need to extend System FC (GHC’s 
intermediate language) with existential types and the corresponding pack and 
unpack syntactic forms. I don’t know of any work studying that question 
specifically, but others may have pointers. simon From: Alex Rozenshteyn 
 Sent: 06 September 2019 15:21To: Simon Peyton Jones 
Cc: Alejandro Serrano Mena ; GHC 
developers Subject: Re: New implementation for 
`ImpredicativeTypes` Hi Simon, You're exactly right, of course. My example is 
confusing, so let me see if I can clarify. What I want in the ideal is map show 
[1, 'a', "b"]. That is, minimal syntactic overhead to mapping a function over 
multiple values of distinct types that results in a homogeneous list. As the 
reddit thread points out, there are workarounds involving TH or wrapping each 
element in a constructor or using bespoke operators, but when it comes down to 
it, none of them actually allows me to say what I mean; the TH one is closest, 
but I reach for TH only in times of desperation. I had thought that one of the 
things preventing this was lack of impredicative instantiation, but now I'm not 
sure. Suppose Haskell did have existentials; would map show @(exists a. Show a 
=> a) [1, 'a', "b"] work in current Haskell and/or in quick-look? Tangentially, 
do you have a reference for what difficulties arise in adding existentials to 
Haskell? I have a feeling that it would make working with GADTs more ergonomic. 
On Fri, Sep 6, 2019 at 12:33 AM Simon Peyton Jones  
wrote:I’m confused.   Char does not have the type (forall a. Show a =>a), so 
our example is iill-typed in System F, never mind about type inference.  
Perhaps there’s a typo?   I think you may have ment   

Re: New implementation for `ImpredicativeTypes`

[Richard Eisenberg]

> On Sep 2, 2021, at 2:10 PM, Alex Rozenshteyn  wrote:
> 
> Oh, I see. That's because this would need to introduce `pack ... as ...` and 
> `open ...` into the core term language, right?

Exactly, yes.

> 
> My sense is that it shouldn't negatively affect runtime performance of 
> programs without existentials even if implemented naively; does that seem 
> accurate? Not that implementing it, even naively, is a small task. 

I would agree with this, too.

> On Sep 2, 2021, at 2:21 PM, john.ericson  
> wrote:
> 
> This reminds me...can we do newtype GADTs in certain situations as a stepping 
> stone? I would think that would be purely easier — more nominal, no nice 
> projections but only `case` and skolems which cannot escape.
> 
> Newtype GADTs we're long deemed impossible IIRC, but surely the paper 
> demonstrates that at least some cases should work?

I don't quite see how this relates to existentials. Note that the paper does 
not address e.g. packing equalities in existentials, which would be needed for 
interacting with GADTs.

Glad folks are enjoying the paper! :)

Richard

> 
> 
>  On Thu, 02 Sep 2021 14:10:34 -0400 rpglove...@gmail.com wrote 
> 
> Oh, I see. That's because this would need to introduce `pack ... as ...` and 
> `open ...` into the core term language, right?
> 
> My sense is that it shouldn't negatively affect runtime performance of 
> programs without existentials even if implemented naively; does that seem 
> accurate? Not that implementing it, even naively, is a small task. 
> 
> On Thu, Sep 2, 2021 at 1:44 PM Simon Peyton Jones  <mailto:simo...@microsoft.com>> wrote:
> Of course not. The same was true for QuickLook, though, wasn't it?
> 
> No, not at all.   QuickLook required zero changes to GHC’s intermediate 
> language – it impacted only the type inference system.   Adding existentials 
> will entail a substantial change to the intermediate language, affecting 
> every optimisation pass.
> 
>  
> 
> Simon
> 
>  
> 
> From: Alex Rozenshteyn mailto:rpglove...@gmail.com>> 
> Sent: 02 September 2021 18:13
> To: Simon Peyton Jones mailto:simo...@microsoft.com>>
> Cc: GHC developers mailto:ghc-devs@haskell.org>>
> Subject: Re: New implementation for `ImpredicativeTypes`
> 
>  
> 
> So it’s not just a question of saying “just add that paper to GHC and voila 
> job done”. 
> 
>  
> 
> Of course not. The same was true for QuickLook, though, wasn't it?
> 
>  
> 
> On Thu, Sep 2, 2021 at 12:42 PM Simon Peyton Jones  <mailto:simo...@microsoft.com>> wrote:
> 
> If I understand correctly, the recent ICFP paper "An Existential Crisis 
> Resolved 
> <https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fdl.acm.org%2Fdoi%2Fpdf%2F10.1145%2F3473569=04%7C01%7Csimonpj%40microsoft.com%7Cc0f0a66e10f94a6f17d508d96e34f2ae%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637661997328916809%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000=kioGsomPn8BuvBLQx6KEr5glMTPvw6m93DK%2BGA0lM08%3D=0>"
>  finally enables this; is that right?
> 
> It describes one way to include existentials in GHC’s intermediate language, 
> which is a real contribution. But it is not a small change.  So it’s not just 
> a question of saying “just add that paper to GHC and voila job done”.
> 
>  
> 
> Simon
> 
>  
> 
> From: Alex Rozenshteyn mailto:rpglove...@gmail.com>> 
> Sent: 02 September 2021 17:10
> To: Simon Peyton Jones mailto:simo...@microsoft.com>>
> Cc: GHC developers mailto:ghc-devs@haskell.org>>
> Subject: Re: New implementation for `ImpredicativeTypes`
> 
>  
> 
> If I understand correctly, the recent ICFP paper "An Existential Crisis 
> Resolved 
> <https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fdl.acm.org%2Fdoi%2Fpdf%2F10.1145%2F3473569=04%7C01%7Csimonpj%40microsoft.com%7Cc0f0a66e10f94a6f17d508d96e34f2ae%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637661997328926803%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000=DtcIgtgrp3zJygorYY32WBKhF40rYtAOhMOOmPWf6pc%3D=0>"
>  finally enables this; is that right?
> 
>  
> 
> On Mon, Sep 9, 2019 at 12:00 PM Simon Peyton Jones  <mailto:simo...@microsoft.com>> wrote:
> 
> Suppose Haskell did have existentials;
> 
>  
> 
> Yes, I think that’s an interesting thing to work on!  I’m not sure what the 
> implications would be.  At very least we’d need to extend System FC (GHC’s 
> intermediate language) with existential types and the corresponding pack and 
> unpack syntactic forms.
> 
>  
> 
> I don’t know of any work studying that qu

Re: New implementation for `ImpredicativeTypes`

[john.ericson]

This reminds me...can we do newtype GADTs in certain situations as a stepping 
stone? I would think that would be purely easier — more nominal, no nice 
projections but only `case` and skolems which cannot escape.Newtype GADTs we're 
long deemed impossible IIRC, but surely the paper demonstrates that at least 
some cases should work?  On Thu, 02 Sep 2021 14:10:34 -0400  
rpglove...@gmail.com  wrote Oh, I see. That's because this would need to 
introduce `pack ... as ...` and `open ...` into the core term language, 
right?My sense is that it shouldn't negatively affect runtime performance of 
programs without existentials even if implemented naively; does that seem 
accurate? Not that implementing it, even naively, is a small task. On Thu, Sep 
2, 2021 at 1:44 PM Simon Peyton Jones  wrote:








Of course not. The same was true for QuickLook, though, wasn't it?
No, not at all.   QuickLook required zero changes to GHC’s intermediate 
language – it impacted only the type inference system.   Adding existentials 
will entail a substantial change to the intermediate
 language, affecting every optimisation pass.
 
Simon
 



From: Alex Rozenshteyn 

Sent: 02 September 2021 18:13
To: Simon Peyton Jones 
Cc: GHC developers 
Subject: Re: New implementation for `ImpredicativeTypes`


 



So it’s not just a question of saying “just add that paper to GHC and voila job 
done”. 



 



Of course not. The same was true for QuickLook, though, wasn't it?



 



On Thu, Sep 2, 2021 at 12:42 PM Simon Peyton Jones  
wrote:





If I understand correctly, the recent ICFP paper "An
 Existential Crisis Resolved" finally enables this; is that right?
It describes one way to include existentials in GHC’s intermediate language, 
which is a real contribution.
But it is not a small change.  So it’s not just a question of saying “just add 
that paper to GHC and voila job done”.
 
Simon
 



From: Alex Rozenshteyn 

Sent: 02 September 2021 17:10
To: Simon Peyton Jones 
Cc: GHC developers 
Subject: Re: New implementation for `ImpredicativeTypes`


 

If I understand correctly, the recent ICFP paper "An
 Existential Crisis Resolved" finally enables this; is that right?

 


On Mon, Sep 9, 2019 at 12:00 PM Simon Peyton Jones  
wrote:





Suppose Haskell did have existentials;
 
Yes, I think that’s an interesting thing to work on!  I’m not sure what the 
implications would be.  At very least we’d need to extend System FC (GHC’s 
intermediate language) with
 existential types and the corresponding pack and unpack syntactic forms.
 
I don’t know of any work studying that question specifically, but others may 
have pointers.
 
simon
 



From: Alex Rozenshteyn 

Sent: 06 September 2019 15:21
To: Simon Peyton Jones 
Cc: Alejandro Serrano Mena ; GHC developers 

Subject: Re: New implementation for `ImpredicativeTypes`


 


Hi Simon,


 


You're exactly right, of course. My example is confusing, so let me see if I 
can clarify.


 


What I want in the ideal is
map show [1, 'a', "b"]. That is, minimal syntactic overhead to mapping a 
function over multiple values of distinct types that results in a homogeneous 
list. As the reddit thread points out, there are workarounds
 involving TH or wrapping each element in a constructor or using bespoke 
operators, but when it comes down to it, none of them actually allows me to say 
what I
mean; the TH one is closest, but I reach for TH only in times of desperation.


 


I had thought that one of the things preventing this was lack of impredicative 
instantiation, but now I'm not sure. Suppose Haskell
did have existentials; would map show @(exists a. Show a => a) [1, 'a', "b"] 
work in current Haskell and/or in quick-look?


 


Tangentially, do you have a reference for what difficulties arise in adding 
existentials to Haskell? I have a feeling that it would make working with GADTs 
more ergonomic.


 


On Fri, Sep 6, 2019 at 12:33 AM Simon Peyton Jones  
wrote:




I’m confused.   Char does not have the type (forall a. Show a =>a), so our 
example is iill-typed in System F, never mind about type inference.  Perhaps 
there’s a typo?   I think
 you may have ment
   exists a. Show a => a
which doesn’t exist in Haskell.  You can write existentials with a data type
 
data Showable where
   S :: forall a. Show a => a -> Showable
 
Then
   map show [S 1, S ‘a’, S “b”]
works fine today (without our new stuff), provided you say
 
   instance Show Showable where
     show (S x) = show x
 
Our new system can only type programs that can be written in System F.   (The 
tricky bit is inferring the impredicative instantiations.)
 
Simon
 



From: ghc-devs 
On Behalf Of Alex Rozenshteyn
Sent: 06 September 2019 03:31
To: Alejandro Serrano Mena 
Cc: GHC developers 
Subject: Re: New implementation for `ImpredicativeTypes`


 


I didn't say anything when you were requesting use cases, so I have no 

Re: New implementation for `ImpredicativeTypes`

[Alex Rozenshteyn]

Oh, I see. That's because this would need to introduce `pack ... as ...`
and `open ...` into the core term language, right?

My sense is that it shouldn't negatively affect runtime performance of
programs without existentials even if implemented naively; does that seem
accurate? Not that implementing it, even naively, is a small task.

On Thu, Sep 2, 2021 at 1:44 PM Simon Peyton Jones 
wrote:

> Of course not. The same was true for QuickLook, though, wasn't it?
>
> No, not at all.   QuickLook required zero changes to GHC’s intermediate
> language – it impacted only the type inference system.   Adding
> existentials will entail a substantial change to the intermediate language,
> affecting every optimisation pass.
>
>
>
> Simon
>
>
>
> *From:* Alex Rozenshteyn 
> *Sent:* 02 September 2021 18:13
> *To:* Simon Peyton Jones 
> *Cc:* GHC developers 
> *Subject:* Re: New implementation for `ImpredicativeTypes`
>
>
>
> So it’s not just a question of saying “just add that paper to GHC and
> voila job done”.
>
>
>
> Of course not. The same was true for QuickLook, though, wasn't it?
>
>
>
> On Thu, Sep 2, 2021 at 12:42 PM Simon Peyton Jones 
> wrote:
>
> If I understand correctly, the recent ICFP paper "An Existential Crisis
> Resolved
> <https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fdl.acm.org%2Fdoi%2Fpdf%2F10.1145%2F3473569=04%7C01%7Csimonpj%40microsoft.com%7Cc0f0a66e10f94a6f17d508d96e34f2ae%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637661997328916809%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000=kioGsomPn8BuvBLQx6KEr5glMTPvw6m93DK%2BGA0lM08%3D=0>"
> finally enables this; is that right?
>
> It describes one way to include existentials in GHC’s intermediate
> language, which is a real contribution. *But it is not a small change*.
> So it’s not just a question of saying “just add that paper to GHC and voila
> job done”.
>
>
>
> Simon
>
>
>
> *From:* Alex Rozenshteyn 
> *Sent:* 02 September 2021 17:10
> *To:* Simon Peyton Jones 
> *Cc:* GHC developers 
> *Subject:* Re: New implementation for `ImpredicativeTypes`
>
>
>
> If I understand correctly, the recent ICFP paper "An Existential Crisis
> Resolved
> <https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fdl.acm.org%2Fdoi%2Fpdf%2F10.1145%2F3473569=04%7C01%7Csimonpj%40microsoft.com%7Cc0f0a66e10f94a6f17d508d96e34f2ae%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637661997328926803%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000=DtcIgtgrp3zJygorYY32WBKhF40rYtAOhMOOmPWf6pc%3D=0>"
> finally enables this; is that right?
>
>
>
> On Mon, Sep 9, 2019 at 12:00 PM Simon Peyton Jones 
> wrote:
>
> Suppose Haskell *did* have existentials;
>
>
>
> Yes, I think that’s an interesting thing to work on!  I’m not sure what
> the implications would be.  At very least we’d need to extend System FC
> (GHC’s intermediate language) with existential types and the corresponding
> pack and unpack syntactic forms.
>
>
>
> I don’t know of any work studying that question specifically, but others
> may have pointers.
>
>
>
> simon
>
>
>
> *From:* Alex Rozenshteyn 
> *Sent:* 06 September 2019 15:21
> *To:* Simon Peyton Jones 
> *Cc:* Alejandro Serrano Mena ; GHC developers <
> ghc-devs@haskell.org>
> *Subject:* Re: New implementation for `ImpredicativeTypes`
>
>
>
> Hi Simon,
>
>
>
> You're exactly right, of course. My example is confusing, so let me see if
> I can clarify.
>
>
>
> What I want in the ideal is map show [1, 'a', "b"]. That is, minimal
> syntactic overhead to mapping a function over multiple values of distinct
> types that results in a homogeneous list. As the reddit thread points out,
> there are workarounds involving TH or wrapping each element in a
> constructor or using bespoke operators, but when it comes down to it, none
> of them actually allows me to say what I *mean*; the TH one is closest,
> but I reach for TH only in times of desperation.
>
>
>
> I had thought that one of the things preventing this was lack of
> impredicative instantiation, but now I'm not sure. Suppose Haskell *did*
> have existentials; would map show @(exists a. Show a => a) [1, 'a', "b"]
> work in current Haskell and/or in quick-look?
>
>
>
> Tangentially, do you have a reference for what difficulties arise in
> adding existentials to Haskell? I have a feeling that it would make working
> with GADTs more ergonomic.
>
>
>
> On Fri, Sep 6, 2019 at 12:33 AM Simon Peyton Jones 
> wrote:
>
> I’m confused.   Char does not 

RE: New implementation for `ImpredicativeTypes`

[Simon Peyton Jones via ghc-devs]

Of course not. The same was true for QuickLook, though, wasn't it?
No, not at all.   QuickLook required zero changes to GHC's intermediate 
language - it impacted only the type inference system.   Adding existentials 
will entail a substantial change to the intermediate language, affecting every 
optimisation pass.

Simon

From: Alex Rozenshteyn 
Sent: 02 September 2021 18:13
To: Simon Peyton Jones 
Cc: GHC developers 
Subject: Re: New implementation for `ImpredicativeTypes`

So it's not just a question of saying "just add that paper to GHC and voila job 
done".

Of course not. The same was true for QuickLook, though, wasn't it?

On Thu, Sep 2, 2021 at 12:42 PM Simon Peyton Jones 
mailto:simo...@microsoft.com>> wrote:
If I understand correctly, the recent ICFP paper "An Existential Crisis 
Resolved<https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fdl.acm.org%2Fdoi%2Fpdf%2F10.1145%2F3473569=04%7C01%7Csimonpj%40microsoft.com%7Cc0f0a66e10f94a6f17d508d96e34f2ae%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637661997328916809%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000=kioGsomPn8BuvBLQx6KEr5glMTPvw6m93DK%2BGA0lM08%3D=0>"
 finally enables this; is that right?
It describes one way to include existentials in GHC's intermediate language, 
which is a real contribution. But it is not a small change.  So it's not just a 
question of saying "just add that paper to GHC and voila job done".

Simon

From: Alex Rozenshteyn mailto:rpglove...@gmail.com>>
Sent: 02 September 2021 17:10
To: Simon Peyton Jones mailto:simo...@microsoft.com>>
Cc: GHC developers mailto:ghc-devs@haskell.org>>
Subject: Re: New implementation for `ImpredicativeTypes`

If I understand correctly, the recent ICFP paper "An Existential Crisis 
Resolved<https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fdl.acm.org%2Fdoi%2Fpdf%2F10.1145%2F3473569=04%7C01%7Csimonpj%40microsoft.com%7Cc0f0a66e10f94a6f17d508d96e34f2ae%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637661997328926803%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000=DtcIgtgrp3zJygorYY32WBKhF40rYtAOhMOOmPWf6pc%3D=0>"
 finally enables this; is that right?

On Mon, Sep 9, 2019 at 12:00 PM Simon Peyton Jones 
mailto:simo...@microsoft.com>> wrote:
Suppose Haskell did have existentials;

Yes, I think that's an interesting thing to work on!  I'm not sure what the 
implications would be.  At very least we'd need to extend System FC (GHC's 
intermediate language) with existential types and the corresponding pack and 
unpack syntactic forms.

I don't know of any work studying that question specifically, but others may 
have pointers.

simon

From: Alex Rozenshteyn mailto:rpglove...@gmail.com>>
Sent: 06 September 2019 15:21
To: Simon Peyton Jones mailto:simo...@microsoft.com>>
Cc: Alejandro Serrano Mena mailto:trup...@gmail.com>>; GHC 
developers mailto:ghc-devs@haskell.org>>
Subject: Re: New implementation for `ImpredicativeTypes`

Hi Simon,

You're exactly right, of course. My example is confusing, so let me see if I 
can clarify.

What I want in the ideal is map show [1, 'a', "b"]. That is, minimal syntactic 
overhead to mapping a function over multiple values of distinct types that 
results in a homogeneous list. As the reddit thread points out, there are 
workarounds involving TH or wrapping each element in a constructor or using 
bespoke operators, but when it comes down to it, none of them actually allows 
me to say what I mean; the TH one is closest, but I reach for TH only in times 
of desperation.

I had thought that one of the things preventing this was lack of impredicative 
instantiation, but now I'm not sure. Suppose Haskell did have existentials; 
would map show @(exists a. Show a => a) [1, 'a', "b"] work in current Haskell 
and/or in quick-look?

Tangentially, do you have a reference for what difficulties arise in adding 
existentials to Haskell? I have a feeling that it would make working with GADTs 
more ergonomic.

On Fri, Sep 6, 2019 at 12:33 AM Simon Peyton Jones 
mailto:simo...@microsoft.com>> wrote:
I'm confused.   Char does not have the type (forall a. Show a =>a), so our 
example is iill-typed in System F, never mind about type inference.  Perhaps 
there's a typo?   I think you may have ment
   exists a. Show a => a
which doesn't exist in Haskell.  You can write existentials with a data type

data Showable where
   S :: forall a. Show a => a -> Showable

Then
   map show [S 1, S 'a', S "b"]
works fine today (without our new stuff), provided you say

   instance Show Showable where
 show (S x) = show x

Our new system can only type programs that can be written in System F.   (The 
tricky bit is inferring the impredicative instantiations.)

Sim

Re: New implementation for `ImpredicativeTypes`

[Alex Rozenshteyn]

>
> So it’s not just a question of saying “just add that paper to GHC and
> voila job done”.


Of course not. The same was true for QuickLook, though, wasn't it?

On Thu, Sep 2, 2021 at 12:42 PM Simon Peyton Jones 
wrote:

> If I understand correctly, the recent ICFP paper "An Existential Crisis
> Resolved
> <https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fdl.acm.org%2Fdoi%2Fpdf%2F10.1145%2F3473569=04%7C01%7Csimonpj%40microsoft.com%7Caee2e0a922204ae3611208d96e2c2c57%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637661959634445057%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000=wsN3Z7t8jCiExzl38%2F2IwNNsPH3Pq5CHJ7dQca5R2Y4%3D=0>"
> finally enables this; is that right?
>
> It describes one way to include existentials in GHC’s intermediate
> language, which is a real contribution. *But it is not a small change*.
> So it’s not just a question of saying “just add that paper to GHC and voila
> job done”.
>
>
>
> Simon
>
>
>
> *From:* Alex Rozenshteyn 
> *Sent:* 02 September 2021 17:10
> *To:* Simon Peyton Jones 
> *Cc:* GHC developers 
> *Subject:* Re: New implementation for `ImpredicativeTypes`
>
>
>
> If I understand correctly, the recent ICFP paper "An Existential Crisis
> Resolved
> <https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fdl.acm.org%2Fdoi%2Fpdf%2F10.1145%2F3473569=04%7C01%7Csimonpj%40microsoft.com%7Caee2e0a922204ae3611208d96e2c2c57%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637661959634445057%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000=wsN3Z7t8jCiExzl38%2F2IwNNsPH3Pq5CHJ7dQca5R2Y4%3D=0>"
> finally enables this; is that right?
>
>
>
> On Mon, Sep 9, 2019 at 12:00 PM Simon Peyton Jones 
> wrote:
>
> Suppose Haskell *did* have existentials;
>
>
>
> Yes, I think that’s an interesting thing to work on!  I’m not sure what
> the implications would be.  At very least we’d need to extend System FC
> (GHC’s intermediate language) with existential types and the corresponding
> pack and unpack syntactic forms.
>
>
>
> I don’t know of any work studying that question specifically, but others
> may have pointers.
>
>
>
> simon
>
>
>
> *From:* Alex Rozenshteyn 
> *Sent:* 06 September 2019 15:21
> *To:* Simon Peyton Jones 
> *Cc:* Alejandro Serrano Mena ; GHC developers <
> ghc-devs@haskell.org>
> *Subject:* Re: New implementation for `ImpredicativeTypes`
>
>
>
> Hi Simon,
>
>
>
> You're exactly right, of course. My example is confusing, so let me see if
> I can clarify.
>
>
>
> What I want in the ideal is map show [1, 'a', "b"]. That is, minimal
> syntactic overhead to mapping a function over multiple values of distinct
> types that results in a homogeneous list. As the reddit thread points out,
> there are workarounds involving TH or wrapping each element in a
> constructor or using bespoke operators, but when it comes down to it, none
> of them actually allows me to say what I *mean*; the TH one is closest,
> but I reach for TH only in times of desperation.
>
>
>
> I had thought that one of the things preventing this was lack of
> impredicative instantiation, but now I'm not sure. Suppose Haskell *did*
> have existentials; would map show @(exists a. Show a => a) [1, 'a', "b"]
> work in current Haskell and/or in quick-look?
>
>
>
> Tangentially, do you have a reference for what difficulties arise in
> adding existentials to Haskell? I have a feeling that it would make working
> with GADTs more ergonomic.
>
>
>
> On Fri, Sep 6, 2019 at 12:33 AM Simon Peyton Jones 
> wrote:
>
> I’m confused.   Char does not have the type (forall a. Show a =>a), so our
> example is iill-typed in System F, never mind about type inference.
> Perhaps there’s a typo?   I think you may have ment
>
>exists a. Show a => a
>
> which doesn’t exist in Haskell.  You can write existentials with a data
> type
>
>
>
> data Showable where
>
>S :: forall a. Show a => a -> Showable
>
>
>
> Then
>
>map show [S 1, S ‘a’, S “b”]
>
> works fine today (without our new stuff), provided you say
>
>
>
>instance Show Showable where
>
>  show (S x) = show x
>
>
>
> Our new system can only type programs that can be written in System F.
> (The tricky bit is inferring the impredicative instantiations.)
>
>
>
> Simon
>
>
>
> *From:* ghc-devs  *On Behalf Of *Alex
> Rozenshteyn
> *Sent:* 06 September 2019 03:31
> *To:* Alejandro Serrano Mena 
> *C

RE: New implementation for `ImpredicativeTypes`

[Simon Peyton Jones via ghc-devs]

If I understand correctly, the recent ICFP paper "An Existential Crisis 
Resolved<https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fdl.acm.org%2Fdoi%2Fpdf%2F10.1145%2F3473569=04%7C01%7Csimonpj%40microsoft.com%7Caee2e0a922204ae3611208d96e2c2c57%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637661959634445057%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000=wsN3Z7t8jCiExzl38%2F2IwNNsPH3Pq5CHJ7dQca5R2Y4%3D=0>"
 finally enables this; is that right?
It describes one way to include existentials in GHC's intermediate language, 
which is a real contribution. But it is not a small change.  So it's not just a 
question of saying "just add that paper to GHC and voila job done".

Simon

From: Alex Rozenshteyn 
Sent: 02 September 2021 17:10
To: Simon Peyton Jones 
Cc: GHC developers 
Subject: Re: New implementation for `ImpredicativeTypes`

If I understand correctly, the recent ICFP paper "An Existential Crisis 
Resolved<https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fdl.acm.org%2Fdoi%2Fpdf%2F10.1145%2F3473569=04%7C01%7Csimonpj%40microsoft.com%7Caee2e0a922204ae3611208d96e2c2c57%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637661959634445057%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000=wsN3Z7t8jCiExzl38%2F2IwNNsPH3Pq5CHJ7dQca5R2Y4%3D=0>"
 finally enables this; is that right?

On Mon, Sep 9, 2019 at 12:00 PM Simon Peyton Jones 
mailto:simo...@microsoft.com>> wrote:
Suppose Haskell did have existentials;

Yes, I think that's an interesting thing to work on!  I'm not sure what the 
implications would be.  At very least we'd need to extend System FC (GHC's 
intermediate language) with existential types and the corresponding pack and 
unpack syntactic forms.

I don't know of any work studying that question specifically, but others may 
have pointers.

simon

From: Alex Rozenshteyn mailto:rpglove...@gmail.com>>
Sent: 06 September 2019 15:21
To: Simon Peyton Jones mailto:simo...@microsoft.com>>
Cc: Alejandro Serrano Mena mailto:trup...@gmail.com>>; GHC 
developers mailto:ghc-devs@haskell.org>>
Subject: Re: New implementation for `ImpredicativeTypes`

Hi Simon,

You're exactly right, of course. My example is confusing, so let me see if I 
can clarify.

What I want in the ideal is map show [1, 'a', "b"]. That is, minimal syntactic 
overhead to mapping a function over multiple values of distinct types that 
results in a homogeneous list. As the reddit thread points out, there are 
workarounds involving TH or wrapping each element in a constructor or using 
bespoke operators, but when it comes down to it, none of them actually allows 
me to say what I mean; the TH one is closest, but I reach for TH only in times 
of desperation.

I had thought that one of the things preventing this was lack of impredicative 
instantiation, but now I'm not sure. Suppose Haskell did have existentials; 
would map show @(exists a. Show a => a) [1, 'a', "b"] work in current Haskell 
and/or in quick-look?

Tangentially, do you have a reference for what difficulties arise in adding 
existentials to Haskell? I have a feeling that it would make working with GADTs 
more ergonomic.

On Fri, Sep 6, 2019 at 12:33 AM Simon Peyton Jones 
mailto:simo...@microsoft.com>> wrote:
I'm confused.   Char does not have the type (forall a. Show a =>a), so our 
example is iill-typed in System F, never mind about type inference.  Perhaps 
there's a typo?   I think you may have ment
   exists a. Show a => a
which doesn't exist in Haskell.  You can write existentials with a data type

data Showable where
   S :: forall a. Show a => a -> Showable

Then
   map show [S 1, S 'a', S "b"]
works fine today (without our new stuff), provided you say

   instance Show Showable where
 show (S x) = show x

Our new system can only type programs that can be written in System F.   (The 
tricky bit is inferring the impredicative instantiations.)

Simon

From: ghc-devs 
mailto:ghc-devs-boun...@haskell.org>> On Behalf 
Of Alex Rozenshteyn
Sent: 06 September 2019 03:31
To: Alejandro Serrano Mena mailto:trup...@gmail.com>>
Cc: GHC developers mailto:ghc-devs@haskell.org>>
Subject: Re: New implementation for `ImpredicativeTypes`

I didn't say anything when you were requesting use cases, so I have no right to 
complain, but I'm still a little disappointed that this doesn't fix my 
(admittedly very minor) issue: 
https://www.reddit.com/r/haskell/comments/3am0qa/existentials_and_the_heterogenous_list_fallacy/csdwlp2/?context=8=9<https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fwww.reddit.com%2Fr%2Fhaskell%2Fcomments%2F3am0qa%2Fexistentials_and_the_heterogenous_list_fallacy%2Fcsdwlp2%2F%3Fcontext%3D8%26depth%3D

Re: New implementation for `ImpredicativeTypes`

[Alex Rozenshteyn]

If I understand correctly, the recent ICFP paper "An Existential Crisis
Resolved <https://dl.acm.org/doi/pdf/10.1145/3473569>" finally enables
this; is that right?

On Mon, Sep 9, 2019 at 12:00 PM Simon Peyton Jones 
wrote:

> Suppose Haskell *did* have existentials;
>
>
>
> Yes, I think that’s an interesting thing to work on!  I’m not sure what
> the implications would be.  At very least we’d need to extend System FC
> (GHC’s intermediate language) with existential types and the corresponding
> pack and unpack syntactic forms.
>
>
>
> I don’t know of any work studying that question specifically, but others
> may have pointers.
>
>
>
> simon
>
>
>
> *From:* Alex Rozenshteyn 
> *Sent:* 06 September 2019 15:21
> *To:* Simon Peyton Jones 
> *Cc:* Alejandro Serrano Mena ; GHC developers <
> ghc-devs@haskell.org>
> *Subject:* Re: New implementation for `ImpredicativeTypes`
>
>
>
> Hi Simon,
>
>
>
> You're exactly right, of course. My example is confusing, so let me see if
> I can clarify.
>
>
>
> What I want in the ideal is map show [1, 'a', "b"]. That is, minimal
> syntactic overhead to mapping a function over multiple values of distinct
> types that results in a homogeneous list. As the reddit thread points out,
> there are workarounds involving TH or wrapping each element in a
> constructor or using bespoke operators, but when it comes down to it, none
> of them actually allows me to say what I *mean*; the TH one is closest,
> but I reach for TH only in times of desperation.
>
>
>
> I had thought that one of the things preventing this was lack of
> impredicative instantiation, but now I'm not sure. Suppose Haskell *did*
> have existentials; would map show @(exists a. Show a => a) [1, 'a', "b"]
> work in current Haskell and/or in quick-look?
>
>
>
> Tangentially, do you have a reference for what difficulties arise in
> adding existentials to Haskell? I have a feeling that it would make working
> with GADTs more ergonomic.
>
>
>
> On Fri, Sep 6, 2019 at 12:33 AM Simon Peyton Jones 
> wrote:
>
> I’m confused.   Char does not have the type (forall a. Show a =>a), so our
> example is iill-typed in System F, never mind about type inference.
> Perhaps there’s a typo?   I think you may have ment
>
>exists a. Show a => a
>
> which doesn’t exist in Haskell.  You can write existentials with a data
> type
>
>
>
> data Showable where
>
>S :: forall a. Show a => a -> Showable
>
>
>
> Then
>
>map show [S 1, S ‘a’, S “b”]
>
> works fine today (without our new stuff), provided you say
>
>
>
>instance Show Showable where
>
>  show (S x) = show x
>
>
>
> Our new system can only type programs that can be written in System F.
> (The tricky bit is inferring the impredicative instantiations.)
>
>
>
> Simon
>
>
>
> *From:* ghc-devs  *On Behalf Of *Alex
> Rozenshteyn
> *Sent:* 06 September 2019 03:31
> *To:* Alejandro Serrano Mena 
> *Cc:* GHC developers 
> *Subject:* Re: New implementation for `ImpredicativeTypes`
>
>
>
> I didn't say anything when you were requesting use cases, so I have no
> right to complain, but I'm still a little disappointed that this doesn't
> fix my (admittedly very minor) issue:
> https://www.reddit.com/r/haskell/comments/3am0qa/existentials_and_the_heterogenous_list_fallacy/csdwlp2/?context=8=9
> <https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fwww.reddit.com%2Fr%2Fhaskell%2Fcomments%2F3am0qa%2Fexistentials_and_the_heterogenous_list_fallacy%2Fcsdwlp2%2F%3Fcontext%3D8%26depth%3D9=02%7C01%7Csimonpj%40microsoft.com%7C911c05e1dc5041e685bd08d732d57261%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637033764634397513=IeOaMmtbwIFEXOBwvLkElsqqS84q50QjFD7MFW0hpK8%3D=0>
>
>
>
> For those who don't want to click on the reddit link: I would like to be
> able to write something like map show ([1, 'a', "b"] :: [forall a. Show a
> => a]), and have it work.
>
>
>
> On Wed, Sep 4, 2019 at 8:13 AM Alejandro Serrano Mena 
> wrote:
>
> Hi all,
>
> As I mentioned some time ago, we have been busy working on a new
> implementation of `ImpredicativeTypes` for GHC. I am very thankful to
> everybody who back then sent us examples of impredicativity which would be
> nice to support, as far as we know this branch supports all of them! :)
>
>
>
> If you want to try it, at
> https://gitlab.haskell.org/trupill/ghc/commit/a3f95a0fe0f647702fd7225fa719a8062a4cc0a5/pipelines?ref=quick-look-build
> <https://nam06.safelinks.protection.outlook.com/?url=https%3A

RE: New implementation for `ImpredicativeTypes`

[Simon Peyton Jones via ghc-devs]

Suppose Haskell did have existentials;

Yes, I think that's an interesting thing to work on!  I'm not sure what the 
implications would be.  At very least we'd need to extend System FC (GHC's 
intermediate language) with existential types and the corresponding pack and 
unpack syntactic forms.

I don't know of any work studying that question specifically, but others may 
have pointers.

simon

From: Alex Rozenshteyn 
Sent: 06 September 2019 15:21
To: Simon Peyton Jones 
Cc: Alejandro Serrano Mena ; GHC developers 

Subject: Re: New implementation for `ImpredicativeTypes`

Hi Simon,

You're exactly right, of course. My example is confusing, so let me see if I 
can clarify.

What I want in the ideal is map show [1, 'a', "b"]. That is, minimal syntactic 
overhead to mapping a function over multiple values of distinct types that 
results in a homogeneous list. As the reddit thread points out, there are 
workarounds involving TH or wrapping each element in a constructor or using 
bespoke operators, but when it comes down to it, none of them actually allows 
me to say what I mean; the TH one is closest, but I reach for TH only in times 
of desperation.

I had thought that one of the things preventing this was lack of impredicative 
instantiation, but now I'm not sure. Suppose Haskell did have existentials; 
would map show @(exists a. Show a => a) [1, 'a', "b"] work in current Haskell 
and/or in quick-look?

Tangentially, do you have a reference for what difficulties arise in adding 
existentials to Haskell? I have a feeling that it would make working with GADTs 
more ergonomic.

On Fri, Sep 6, 2019 at 12:33 AM Simon Peyton Jones 
mailto:simo...@microsoft.com>> wrote:
I'm confused.   Char does not have the type (forall a. Show a =>a), so our 
example is iill-typed in System F, never mind about type inference.  Perhaps 
there's a typo?   I think you may have ment
   exists a. Show a => a
which doesn't exist in Haskell.  You can write existentials with a data type

data Showable where
   S :: forall a. Show a => a -> Showable

Then
   map show [S 1, S 'a', S "b"]
works fine today (without our new stuff), provided you say

   instance Show Showable where
 show (S x) = show x

Our new system can only type programs that can be written in System F.   (The 
tricky bit is inferring the impredicative instantiations.)

Simon

From: ghc-devs 
mailto:ghc-devs-boun...@haskell.org>> On Behalf 
Of Alex Rozenshteyn
Sent: 06 September 2019 03:31
To: Alejandro Serrano Mena mailto:trup...@gmail.com>>
Cc: GHC developers mailto:ghc-devs@haskell.org>>
Subject: Re: New implementation for `ImpredicativeTypes`

I didn't say anything when you were requesting use cases, so I have no right to 
complain, but I'm still a little disappointed that this doesn't fix my 
(admittedly very minor) issue: 
https://www.reddit.com/r/haskell/comments/3am0qa/existentials_and_the_heterogenous_list_fallacy/csdwlp2/?context=8=9<https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fwww.reddit.com%2Fr%2Fhaskell%2Fcomments%2F3am0qa%2Fexistentials_and_the_heterogenous_list_fallacy%2Fcsdwlp2%2F%3Fcontext%3D8%26depth%3D9=02%7C01%7Csimonpj%40microsoft.com%7C911c05e1dc5041e685bd08d732d57261%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637033764634397513=IeOaMmtbwIFEXOBwvLkElsqqS84q50QjFD7MFW0hpK8%3D=0>

For those who don't want to click on the reddit link: I would like to be able 
to write something like map show ([1, 'a', "b"] :: [forall a. Show a => a]), 
and have it work.

On Wed, Sep 4, 2019 at 8:13 AM Alejandro Serrano Mena 
mailto:trup...@gmail.com>> wrote:
Hi all,
As I mentioned some time ago, we have been busy working on a new implementation 
of `ImpredicativeTypes` for GHC. I am very thankful to everybody who back then 
sent us examples of impredicativity which would be nice to support, as far as 
we know this branch supports all of them! :)

If you want to try it, at 
https://gitlab.haskell.org/trupill/ghc/commit/a3f95a0fe0f647702fd7225fa719a8062a4cc0a5/pipelines?ref=quick-look-build<https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgitlab.haskell.org%2Ftrupill%2Fghc%2Fcommit%2Fa3f95a0fe0f647702fd7225fa719a8062a4cc0a5%2Fpipelines%3Fref%3Dquick-look-build=02%7C01%7Csimonpj%40microsoft.com%7C911c05e1dc5041e685bd08d732d57261%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637033764634397513=fWmUVHUC5hFG%2FBqNwXl1N4par46XLdHQAUxs2DstpvQ%3D=0>
 you can find the result of the pipeline, which includes builds for several 
platforms (click on the "Artifacts" button, the one which looks like a cloud, 
to get them). The code is being developed at 
https://gitlab.haskell.org/trupill/ghc<https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgitlab.haskell.org%2Ftrupill%2Fghc=02%7C01%7Csimonpj%40microsoft.com%7C911c05e1dc5041e685bd08d732d57261%7C72f988bf86f141af91ab2d

Re: New implementation for `ImpredicativeTypes`

[Iavor Diatchki]

Why would you infer this type as opposed to `[exists a. a]`?

On Fri, Sep 6, 2019 at 12:08 PM Vladislav Zavialov
 wrote:
>
> Iavor,
>
> Alex’s example can be well-typed if we allow first-class existentials:
>
>   [1, ‘a’, “b”] :: [exists a. Show a => a]
>
> This has nothing to do with the definition of lists. I believe the confusion 
> was between existential types and impredicative types, as Simon has pointed 
> out.
>
> - Vlad
>
> > On 6 Sep 2019, at 20:56, Iavor Diatchki  wrote:
> >
> > Hello Alex,
> >
> > the issue with your example is not the mapping of `show` but the list
> > `[1, 'a', "b"]`.  It is not well typed simply because of how lists are
> > defined.   Remember that `[1, 'a', "b"]` is not really special---it is
> > just syntactic sugar for `1 : 'a' : "b" : []` and the type of `(:)`
> > requires the elements to have the same type.
> >
> > Of course, in principle, one could define a different list type that
> > allowed values of arbitrary types to be stored in it (e.g., the
> > example list would be just of type `List`).
> > The issue is that you can't really use the elements of such a list as
> > you wouldn't know what type they have.
> >
> > Yet another option is to define a list type where the "cons" operation
> > remembers the types of the elements in the type of the constructed
> > list---at this point the lists become more like tuples (e.g., the
> > example would be of type `List [Int,Char,String]`).   This is
> > possible, but then them `map` function would have an interesting
> > type...
> >
> > I'd be happy to answer more questions but I don't want to side-track
> > the thread as all this is quite orthogonal to impredicative types.
> >
> > -Iavor
> >
> >
> >
> >
> >
> >
> >
> >
> >
> > On Fri, Sep 6, 2019 at 7:21 AM Alex Rozenshteyn  
> > wrote:
> >>
> >> Hi Simon,
> >>
> >> You're exactly right, of course. My example is confusing, so let me see if 
> >> I can clarify.
> >>
> >> What I want in the ideal is map show [1, 'a', "b"]. That is, minimal 
> >> syntactic overhead to mapping a function over multiple values of distinct 
> >> types that results in a homogeneous list. As the reddit thread points out, 
> >> there are workarounds involving TH or wrapping each element in a 
> >> constructor or using bespoke operators, but when it comes down to it, none 
> >> of them actually allows me to say what I mean; the TH one is closest, but 
> >> I reach for TH only in times of desperation.
> >>
> >> I had thought that one of the things preventing this was lack of 
> >> impredicative instantiation, but now I'm not sure. Suppose Haskell did 
> >> have existentials; would map show @(exists a. Show a => a) [1, 'a', "b"] 
> >> work in current Haskell and/or in quick-look?
> >>
> >> Tangentially, do you have a reference for what difficulties arise in 
> >> adding existentials to Haskell? I have a feeling that it would make 
> >> working with GADTs more ergonomic.
> >>
> >> On Fri, Sep 6, 2019 at 12:33 AM Simon Peyton Jones  
> >> wrote:
> >>>
> >>> I’m confused.   Char does not have the type (forall a. Show a =>a), so 
> >>> our example is iill-typed in System F, never mind about type inference.  
> >>> Perhaps there’s a typo?   I think you may have ment
> >>>
> >>>   exists a. Show a => a
> >>>
> >>> which doesn’t exist in Haskell.  You can write existentials with a data 
> >>> type
> >>>
> >>>
> >>>
> >>> data Showable where
> >>>
> >>>   S :: forall a. Show a => a -> Showable
> >>>
> >>>
> >>>
> >>> Then
> >>>
> >>>   map show [S 1, S ‘a’, S “b”]
> >>>
> >>> works fine today (without our new stuff), provided you say
> >>>
> >>>
> >>>
> >>>   instance Show Showable where
> >>>
> >>> show (S x) = show x
> >>>
> >>>
> >>>
> >>> Our new system can only type programs that can be written in System F.   
> >>> (The tricky bit is inferring the impredicative instantiations.)
> >>>
> >>>
> >>>
> >>> Simon
> >>>
> >&

Re: New implementation for `ImpredicativeTypes`

[Vladislav Zavialov]

Iavor,

Alex’s example can be well-typed if we allow first-class existentials:

  [1, ‘a’, “b”] :: [exists a. Show a => a]

This has nothing to do with the definition of lists. I believe the confusion 
was between existential types and impredicative types, as Simon has pointed out.

- Vlad

> On 6 Sep 2019, at 20:56, Iavor Diatchki  wrote:
> 
> Hello Alex,
> 
> the issue with your example is not the mapping of `show` but the list
> `[1, 'a', "b"]`.  It is not well typed simply because of how lists are
> defined.   Remember that `[1, 'a', "b"]` is not really special---it is
> just syntactic sugar for `1 : 'a' : "b" : []` and the type of `(:)`
> requires the elements to have the same type.
> 
> Of course, in principle, one could define a different list type that
> allowed values of arbitrary types to be stored in it (e.g., the
> example list would be just of type `List`).
> The issue is that you can't really use the elements of such a list as
> you wouldn't know what type they have.
> 
> Yet another option is to define a list type where the "cons" operation
> remembers the types of the elements in the type of the constructed
> list---at this point the lists become more like tuples (e.g., the
> example would be of type `List [Int,Char,String]`).   This is
> possible, but then them `map` function would have an interesting
> type...
> 
> I'd be happy to answer more questions but I don't want to side-track
> the thread as all this is quite orthogonal to impredicative types.
> 
> -Iavor
> 
> 
> 
> 
> 
> 
> 
> 
> 
> On Fri, Sep 6, 2019 at 7:21 AM Alex Rozenshteyn  wrote:
>> 
>> Hi Simon,
>> 
>> You're exactly right, of course. My example is confusing, so let me see if I 
>> can clarify.
>> 
>> What I want in the ideal is map show [1, 'a', "b"]. That is, minimal 
>> syntactic overhead to mapping a function over multiple values of distinct 
>> types that results in a homogeneous list. As the reddit thread points out, 
>> there are workarounds involving TH or wrapping each element in a constructor 
>> or using bespoke operators, but when it comes down to it, none of them 
>> actually allows me to say what I mean; the TH one is closest, but I reach 
>> for TH only in times of desperation.
>> 
>> I had thought that one of the things preventing this was lack of 
>> impredicative instantiation, but now I'm not sure. Suppose Haskell did have 
>> existentials; would map show @(exists a. Show a => a) [1, 'a', "b"] work in 
>> current Haskell and/or in quick-look?
>> 
>> Tangentially, do you have a reference for what difficulties arise in adding 
>> existentials to Haskell? I have a feeling that it would make working with 
>> GADTs more ergonomic.
>> 
>> On Fri, Sep 6, 2019 at 12:33 AM Simon Peyton Jones  
>> wrote:
>>> 
>>> I’m confused.   Char does not have the type (forall a. Show a =>a), so our 
>>> example is iill-typed in System F, never mind about type inference.  
>>> Perhaps there’s a typo?   I think you may have ment
>>> 
>>>   exists a. Show a => a
>>> 
>>> which doesn’t exist in Haskell.  You can write existentials with a data type
>>> 
>>> 
>>> 
>>> data Showable where
>>> 
>>>   S :: forall a. Show a => a -> Showable
>>> 
>>> 
>>> 
>>> Then
>>> 
>>>   map show [S 1, S ‘a’, S “b”]
>>> 
>>> works fine today (without our new stuff), provided you say
>>> 
>>> 
>>> 
>>>   instance Show Showable where
>>> 
>>> show (S x) = show x
>>> 
>>> 
>>> 
>>> Our new system can only type programs that can be written in System F.   
>>> (The tricky bit is inferring the impredicative instantiations.)
>>> 
>>> 
>>> 
>>> Simon
>>> 
>>> 
>>> 
>>> From: ghc-devs  On Behalf Of Alex Rozenshteyn
>>> Sent: 06 September 2019 03:31
>>> To: Alejandro Serrano Mena 
>>> Cc: GHC developers 
>>> Subject: Re: New implementation for `ImpredicativeTypes`
>>> 
>>> 
>>> 
>>> I didn't say anything when you were requesting use cases, so I have no 
>>> right to complain, but I'm still a little disappointed that this doesn't 
>>> fix my (admittedly very minor) issue: 
>>> https://www.reddit.com/r/haskell/comments/3am0qa/existentials_and_the_heterogenous_list_fallacy/csdwlp2/?context=8=9
>>> 
>>&

Re: New implementation for `ImpredicativeTypes`

[Alejandro Serrano Mena]

Hi Alex,
Also de-railing the conversation, the Utrecht Haskell Compiler supports
existential types in addition to universally-quantified ones. The work on
Atze Dijkstra (among others) describes some of the problems and possible
solutions to inference:
- His PhD thesis [https://dspace.library.uu.nl/handle/1874/7352] describes
existentials in Section 8.
- Their paper "A Lazy Language Needs a Lazy Type System" [
https://dspace.library.uu.nl/handle/1874/346316] proposes treating
existential types as "polymorphic contexts".

Going back to impredicativity, adding existential types would only
complicate inference more, since there are more types to choose from while
instantiating. But the delta would not be that large, since once a type
constructor guards a type, everything inside of it should be equal, and
checking equality of existential types is as hard as checking for universal
types.

Alejandro

El vie., 6 sept. 2019 a las 16:21, Alex Rozenshteyn ()
escribió:

> Hi Simon,
>
> You're exactly right, of course. My example is confusing, so let me see if
> I can clarify.
>
> What I want in the ideal is map show [1, 'a', "b"]. That is, minimal
> syntactic overhead to mapping a function over multiple values of distinct
> types that results in a homogeneous list. As the reddit thread points out,
> there are workarounds involving TH or wrapping each element in a
> constructor or using bespoke operators, but when it comes down to it, none
> of them actually allows me to say what I *mean*; the TH one is closest,
> but I reach for TH only in times of desperation.
>
> I had thought that one of the things preventing this was lack of
> impredicative instantiation, but now I'm not sure. Suppose Haskell *did*
> have existentials; would map show @(exists a. Show a => a) [1, 'a', "b"]
> work in current Haskell and/or in quick-look?
>
> Tangentially, do you have a reference for what difficulties arise in
> adding existentials to Haskell? I have a feeling that it would make working
> with GADTs more ergonomic.
>
> On Fri, Sep 6, 2019 at 12:33 AM Simon Peyton Jones 
> wrote:
>
>> I’m confused.   Char does not have the type (forall a. Show a =>a), so
>> our example is iill-typed in System F, never mind about type inference.
>> Perhaps there’s a typo?   I think you may have ment
>>
>>exists a. Show a => a
>>
>> which doesn’t exist in Haskell.  You can write existentials with a data
>> type
>>
>>
>>
>> data Showable where
>>
>>S :: forall a. Show a => a -> Showable
>>
>>
>>
>> Then
>>
>>map show [S 1, S ‘a’, S “b”]
>>
>> works fine today (without our new stuff), provided you say
>>
>>
>>
>>instance Show Showable where
>>
>>  show (S x) = show x
>>
>>
>>
>> Our new system can only type programs that can be written in System F.
>> (The tricky bit is inferring the impredicative instantiations.)
>>
>>
>>
>> Simon
>>
>>
>>
>> *From:* ghc-devs  *On Behalf Of *Alex
>> Rozenshteyn
>> *Sent:* 06 September 2019 03:31
>> *To:* Alejandro Serrano Mena 
>> *Cc:* GHC developers 
>> *Subject:* Re: New implementation for `ImpredicativeTypes`
>>
>>
>>
>> I didn't say anything when you were requesting use cases, so I have no
>> right to complain, but I'm still a little disappointed that this doesn't
>> fix my (admittedly very minor) issue:
>> https://www.reddit.com/r/haskell/comments/3am0qa/existentials_and_the_heterogenous_list_fallacy/csdwlp2/?context=8=9
>> <https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fwww.reddit.com%2Fr%2Fhaskell%2Fcomments%2F3am0qa%2Fexistentials_and_the_heterogenous_list_fallacy%2Fcsdwlp2%2F%3Fcontext%3D8%26depth%3D9=02%7C01%7Csimonpj%40microsoft.com%7Cf5bddbe8c13b424fad8a08d732724d04%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C63708810706935=a5c3ujC0kiPlocgHg8AX%2BwIP6ZH2hnqszCpnWOiqpGQ%3D=0>
>>
>>
>>
>> For those who don't want to click on the reddit link: I would like to be
>> able to write something like map show ([1, 'a', "b"] :: [forall a. Show
>> a => a]), and have it work.
>>
>>
>>
>> On Wed, Sep 4, 2019 at 8:13 AM Alejandro Serrano Mena 
>> wrote:
>>
>> Hi all,
>>
>> As I mentioned some time ago, we have been busy working on a new
>> implementation of `ImpredicativeTypes` for GHC. I am very thankful to
>> everybody who back then sent us examples of impredicativity which would be
>> nice to support, as far as we know this branch supports all of them! :)
>

Re: New implementation for `ImpredicativeTypes`

[Iavor Diatchki]

Hello Alex,

the issue with your example is not the mapping of `show` but the list
`[1, 'a', "b"]`.  It is not well typed simply because of how lists are
defined.   Remember that `[1, 'a', "b"]` is not really special---it is
just syntactic sugar for `1 : 'a' : "b" : []` and the type of `(:)`
requires the elements to have the same type.

Of course, in principle, one could define a different list type that
allowed values of arbitrary types to be stored in it (e.g., the
example list would be just of type `List`).
The issue is that you can't really use the elements of such a list as
you wouldn't know what type they have.

Yet another option is to define a list type where the "cons" operation
remembers the types of the elements in the type of the constructed
list---at this point the lists become more like tuples (e.g., the
example would be of type `List [Int,Char,String]`).   This is
possible, but then them `map` function would have an interesting
type...

I'd be happy to answer more questions but I don't want to side-track
the thread as all this is quite orthogonal to impredicative types.

-Iavor









On Fri, Sep 6, 2019 at 7:21 AM Alex Rozenshteyn  wrote:
>
> Hi Simon,
>
> You're exactly right, of course. My example is confusing, so let me see if I 
> can clarify.
>
> What I want in the ideal is map show [1, 'a', "b"]. That is, minimal 
> syntactic overhead to mapping a function over multiple values of distinct 
> types that results in a homogeneous list. As the reddit thread points out, 
> there are workarounds involving TH or wrapping each element in a constructor 
> or using bespoke operators, but when it comes down to it, none of them 
> actually allows me to say what I mean; the TH one is closest, but I reach for 
> TH only in times of desperation.
>
> I had thought that one of the things preventing this was lack of 
> impredicative instantiation, but now I'm not sure. Suppose Haskell did have 
> existentials; would map show @(exists a. Show a => a) [1, 'a', "b"] work in 
> current Haskell and/or in quick-look?
>
> Tangentially, do you have a reference for what difficulties arise in adding 
> existentials to Haskell? I have a feeling that it would make working with 
> GADTs more ergonomic.
>
> On Fri, Sep 6, 2019 at 12:33 AM Simon Peyton Jones  
> wrote:
>>
>> I’m confused.   Char does not have the type (forall a. Show a =>a), so our 
>> example is iill-typed in System F, never mind about type inference.  Perhaps 
>> there’s a typo?   I think you may have ment
>>
>>exists a. Show a => a
>>
>> which doesn’t exist in Haskell.  You can write existentials with a data type
>>
>>
>>
>> data Showable where
>>
>>S :: forall a. Show a => a -> Showable
>>
>>
>>
>> Then
>>
>>map show [S 1, S ‘a’, S “b”]
>>
>> works fine today (without our new stuff), provided you say
>>
>>
>>
>>instance Show Showable where
>>
>>  show (S x) = show x
>>
>>
>>
>> Our new system can only type programs that can be written in System F.   
>> (The tricky bit is inferring the impredicative instantiations.)
>>
>>
>>
>> Simon
>>
>>
>>
>> From: ghc-devs  On Behalf Of Alex Rozenshteyn
>> Sent: 06 September 2019 03:31
>> To: Alejandro Serrano Mena 
>> Cc: GHC developers 
>> Subject: Re: New implementation for `ImpredicativeTypes`
>>
>>
>>
>> I didn't say anything when you were requesting use cases, so I have no right 
>> to complain, but I'm still a little disappointed that this doesn't fix my 
>> (admittedly very minor) issue: 
>> https://www.reddit.com/r/haskell/comments/3am0qa/existentials_and_the_heterogenous_list_fallacy/csdwlp2/?context=8=9
>>
>>
>>
>> For those who don't want to click on the reddit link: I would like to be 
>> able to write something like map show ([1, 'a', "b"] :: [forall a. Show a => 
>> a]), and have it work.
>>
>>
>>
>> On Wed, Sep 4, 2019 at 8:13 AM Alejandro Serrano Mena  
>> wrote:
>>
>> Hi all,
>>
>> As I mentioned some time ago, we have been busy working on a new 
>> implementation of `ImpredicativeTypes` for GHC. I am very thankful to 
>> everybody who back then sent us examples of impredicativity which would be 
>> nice to support, as far as we know this branch supports all of them! :)
>>
>>
>>
>> If you want to try it, at 
>> https://gitlab.haskell.org/trupill/ghc/commit/a3f95a0fe0f647702fd7225fa719a8062a4cc0a5/pipelines?ref=quick-lo

Re: New implementation for `ImpredicativeTypes`

[Alex Rozenshteyn]

Hi Simon,

You're exactly right, of course. My example is confusing, so let me see if
I can clarify.

What I want in the ideal is map show [1, 'a', "b"]. That is, minimal
syntactic overhead to mapping a function over multiple values of distinct
types that results in a homogeneous list. As the reddit thread points out,
there are workarounds involving TH or wrapping each element in a
constructor or using bespoke operators, but when it comes down to it, none
of them actually allows me to say what I *mean*; the TH one is closest, but
I reach for TH only in times of desperation.

I had thought that one of the things preventing this was lack of
impredicative instantiation, but now I'm not sure. Suppose Haskell *did*
have existentials; would map show @(exists a. Show a => a) [1, 'a', "b"]
work in current Haskell and/or in quick-look?

Tangentially, do you have a reference for what difficulties arise in adding
existentials to Haskell? I have a feeling that it would make working with
GADTs more ergonomic.

On Fri, Sep 6, 2019 at 12:33 AM Simon Peyton Jones 
wrote:

> I’m confused.   Char does not have the type (forall a. Show a =>a), so our
> example is iill-typed in System F, never mind about type inference.
> Perhaps there’s a typo?   I think you may have ment
>
>exists a. Show a => a
>
> which doesn’t exist in Haskell.  You can write existentials with a data
> type
>
>
>
> data Showable where
>
>S :: forall a. Show a => a -> Showable
>
>
>
> Then
>
>map show [S 1, S ‘a’, S “b”]
>
> works fine today (without our new stuff), provided you say
>
>
>
>instance Show Showable where
>
>  show (S x) = show x
>
>
>
> Our new system can only type programs that can be written in System F.
> (The tricky bit is inferring the impredicative instantiations.)
>
>
>
> Simon
>
>
>
> *From:* ghc-devs  *On Behalf Of *Alex
> Rozenshteyn
> *Sent:* 06 September 2019 03:31
> *To:* Alejandro Serrano Mena 
> *Cc:* GHC developers 
> *Subject:* Re: New implementation for `ImpredicativeTypes`
>
>
>
> I didn't say anything when you were requesting use cases, so I have no
> right to complain, but I'm still a little disappointed that this doesn't
> fix my (admittedly very minor) issue:
> https://www.reddit.com/r/haskell/comments/3am0qa/existentials_and_the_heterogenous_list_fallacy/csdwlp2/?context=8=9
> <https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fwww.reddit.com%2Fr%2Fhaskell%2Fcomments%2F3am0qa%2Fexistentials_and_the_heterogenous_list_fallacy%2Fcsdwlp2%2F%3Fcontext%3D8%26depth%3D9=02%7C01%7Csimonpj%40microsoft.com%7Cf5bddbe8c13b424fad8a08d732724d04%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C63708810706935=a5c3ujC0kiPlocgHg8AX%2BwIP6ZH2hnqszCpnWOiqpGQ%3D=0>
>
>
>
> For those who don't want to click on the reddit link: I would like to be
> able to write something like map show ([1, 'a', "b"] :: [forall a. Show a
> => a]), and have it work.
>
>
>
> On Wed, Sep 4, 2019 at 8:13 AM Alejandro Serrano Mena 
> wrote:
>
> Hi all,
>
> As I mentioned some time ago, we have been busy working on a new
> implementation of `ImpredicativeTypes` for GHC. I am very thankful to
> everybody who back then sent us examples of impredicativity which would be
> nice to support, as far as we know this branch supports all of them! :)
>
>
>
> If you want to try it, at
> https://gitlab.haskell.org/trupill/ghc/commit/a3f95a0fe0f647702fd7225fa719a8062a4cc0a5/pipelines?ref=quick-look-build
> <https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgitlab.haskell.org%2Ftrupill%2Fghc%2Fcommit%2Fa3f95a0fe0f647702fd7225fa719a8062a4cc0a5%2Fpipelines%3Fref%3Dquick-look-build=02%7C01%7Csimonpj%40microsoft.com%7Cf5bddbe8c13b424fad8a08d732724d04%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C63708810716935=PP1imEsNrkIhloEV3AS52nrZBtyjen4i1e3pJTcMi6M%3D=0>
> you can find the result of the pipeline, which includes builds for several
> platforms (click on the "Artifacts" button, the one which looks like a
> cloud, to get them). The code is being developed at
> https://gitlab.haskell.org/trupill/ghc
> <https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgitlab.haskell.org%2Ftrupill%2Fghc=02%7C01%7Csimonpj%40microsoft.com%7Cf5bddbe8c13b424fad8a08d732724d04%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C63708810716935=IgtSqJP4%2BhCfy3%2FHVsqX6wpPYVMS8D1wN46aXHnFcUw%3D=0>
> .
>
>
>
> Any code should run *unchanged* except for some eta-expansion required for
> some specific usage patterns of higher-rank types. Please don't hesitate to
> ask any questions or clarifications about it. A merge request for tracking
> this can b

RE: New implementation for `ImpredicativeTypes`

[Simon Peyton Jones via ghc-devs]

I’m confused.   Char does not have the type (forall a. Show a =>a), so our 
example is iill-typed in System F, never mind about type inference.  Perhaps 
there’s a typo?   I think you may have ment
   exists a. Show a => a
which doesn’t exist in Haskell.  You can write existentials with a data type

data Showable where
   S :: forall a. Show a => a -> Showable

Then
   map show [S 1, S ‘a’, S “b”]
works fine today (without our new stuff), provided you say

   instance Show Showable where
 show (S x) = show x

Our new system can only type programs that can be written in System F.   (The 
tricky bit is inferring the impredicative instantiations.)

Simon

From: ghc-devs  On Behalf Of Alex Rozenshteyn
Sent: 06 September 2019 03:31
To: Alejandro Serrano Mena 
Cc: GHC developers 
Subject: Re: New implementation for `ImpredicativeTypes`

I didn't say anything when you were requesting use cases, so I have no right to 
complain, but I'm still a little disappointed that this doesn't fix my 
(admittedly very minor) issue: 
https://www.reddit.com/r/haskell/comments/3am0qa/existentials_and_the_heterogenous_list_fallacy/csdwlp2/?context=8=9<https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fwww.reddit.com%2Fr%2Fhaskell%2Fcomments%2F3am0qa%2Fexistentials_and_the_heterogenous_list_fallacy%2Fcsdwlp2%2F%3Fcontext%3D8%26depth%3D9=02%7C01%7Csimonpj%40microsoft.com%7Cf5bddbe8c13b424fad8a08d732724d04%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C63708810706935=a5c3ujC0kiPlocgHg8AX%2BwIP6ZH2hnqszCpnWOiqpGQ%3D=0>

For those who don't want to click on the reddit link: I would like to be able 
to write something like map show ([1, 'a', "b"] :: [forall a. Show a => a]), 
and have it work.

On Wed, Sep 4, 2019 at 8:13 AM Alejandro Serrano Mena 
mailto:trup...@gmail.com>> wrote:
Hi all,
As I mentioned some time ago, we have been busy working on a new implementation 
of `ImpredicativeTypes` for GHC. I am very thankful to everybody who back then 
sent us examples of impredicativity which would be nice to support, as far as 
we know this branch supports all of them! :)

If you want to try it, at 
https://gitlab.haskell.org/trupill/ghc/commit/a3f95a0fe0f647702fd7225fa719a8062a4cc0a5/pipelines?ref=quick-look-build<https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgitlab.haskell.org%2Ftrupill%2Fghc%2Fcommit%2Fa3f95a0fe0f647702fd7225fa719a8062a4cc0a5%2Fpipelines%3Fref%3Dquick-look-build=02%7C01%7Csimonpj%40microsoft.com%7Cf5bddbe8c13b424fad8a08d732724d04%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C63708810716935=PP1imEsNrkIhloEV3AS52nrZBtyjen4i1e3pJTcMi6M%3D=0>
 you can find the result of the pipeline, which includes builds for several 
platforms (click on the "Artifacts" button, the one which looks like a cloud, 
to get them). The code is being developed at 
https://gitlab.haskell.org/trupill/ghc<https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgitlab.haskell.org%2Ftrupill%2Fghc=02%7C01%7Csimonpj%40microsoft.com%7Cf5bddbe8c13b424fad8a08d732724d04%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C63708810716935=IgtSqJP4%2BhCfy3%2FHVsqX6wpPYVMS8D1wN46aXHnFcUw%3D=0>.

Any code should run *unchanged* except for some eta-expansion required for some 
specific usage patterns of higher-rank types. Please don't hesitate to ask any 
questions or clarifications about it. A merge request for tracking this can be 
found at 
https://gitlab.haskell.org/ghc/ghc/merge_requests/1659<https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgitlab.haskell.org%2Fghc%2Fghc%2Fmerge_requests%2F1659=02%7C01%7Csimonpj%40microsoft.com%7Cf5bddbe8c13b424fad8a08d732724d04%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C63708810716935=YJ5N9d7gXC2JbpqTvpqs4wjY%2F7Ev%2FikRdYIK%2Bhv4rRE%3D=0>

Kind regards,
Alejandro
___
ghc-devs mailing list
ghc-devs@haskell.org<mailto:ghc-devs@haskell.org>
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs<https://nam06.safelinks.protection.outlook.com/?url=http%3A%2F%2Fmail.haskell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc-devs=02%7C01%7Csimonpj%40microsoft.com%7Cf5bddbe8c13b424fad8a08d732724d04%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C63708810726922=jw0sroJW1D8MoBBxVKJROdGefo5gir%2BtQSto0b%2Bj3NA%3D=0>
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: New implementation for `ImpredicativeTypes`

[Alex Rozenshteyn]

I didn't say anything when you were requesting use cases, so I have no
right to complain, but I'm still a little disappointed that this doesn't
fix my (admittedly very minor) issue:
https://www.reddit.com/r/haskell/comments/3am0qa/existentials_and_the_heterogenous_list_fallacy/csdwlp2/?context=8=9

For those who don't want to click on the reddit link: I would like to be
able to write something like map show ([1, 'a', "b"] :: [forall a. Show a
=> a]), and have it work.

On Wed, Sep 4, 2019 at 8:13 AM Alejandro Serrano Mena 
wrote:

> Hi all,
> As I mentioned some time ago, we have been busy working on a new
> implementation of `ImpredicativeTypes` for GHC. I am very thankful to
> everybody who back then sent us examples of impredicativity which would be
> nice to support, as far as we know this branch supports all of them! :)
>
> If you want to try it, at
> https://gitlab.haskell.org/trupill/ghc/commit/a3f95a0fe0f647702fd7225fa719a8062a4cc0a5/pipelines?ref=quick-look-build
> you can find the result of the pipeline, which includes builds for several
> platforms (click on the "Artifacts" button, the one which looks like a
> cloud, to get them). The code is being developed at
> https://gitlab.haskell.org/trupill/ghc.
>
> Any code should run *unchanged* except for some eta-expansion required for
> some specific usage patterns of higher-rank types. Please don't hesitate to
> ask any questions or clarifications about it. A merge request for tracking
> this can be found at
> https://gitlab.haskell.org/ghc/ghc/merge_requests/1659
>
> Kind regards,
> Alejandro
> ___
> ghc-devs mailing list
> ghc-devs@haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

RE: New implementation for `ImpredicativeTypes`

[Simon Peyton Jones via ghc-devs]

I update the MR 
Description<https://gitlab.haskell.org/ghc/ghc/merge_requests/1659> to make the 
link more discoverable.

S

From: ghc-devs  On Behalf Of Alejandro Serrano 
Mena
Sent: 05 September 2019 09:30
To: GHC developers 
Subject: Re: New implementation for `ImpredicativeTypes`

To follow up on this, the current spec. is available in the following PDF: 
https://www.dropbox.com/s/hxjp28ym3lptmxw/quick-look-steps.pdf?dl=0<https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fwww.dropbox.com%2Fs%2Fhxjp28ym3lptmxw%2Fquick-look-steps.pdf%3Fdl%3D0=02%7C01%7Csimonpj%40microsoft.com%7Cb531ccc74392466a22a108d731db542e%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C1%7C637032690392226873=b%2FE4R3wka1%2FEgBqcg3MhJe8LZq7tP3UTs%2FHVqMVHKKw%3D=0>

El mié., 4 sept. 2019 a las 17:13, Alejandro Serrano Mena 
(mailto:trup...@gmail.com>>) escribió:
Hi all,
As I mentioned some time ago, we have been busy working on a new implementation 
of `ImpredicativeTypes` for GHC. I am very thankful to everybody who back then 
sent us examples of impredicativity which would be nice to support, as far as 
we know this branch supports all of them! :)

If you want to try it, at 
https://gitlab.haskell.org/trupill/ghc/commit/a3f95a0fe0f647702fd7225fa719a8062a4cc0a5/pipelines?ref=quick-look-build<https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgitlab.haskell.org%2Ftrupill%2Fghc%2Fcommit%2Fa3f95a0fe0f647702fd7225fa719a8062a4cc0a5%2Fpipelines%3Fref%3Dquick-look-build=02%7C01%7Csimonpj%40microsoft.com%7Cb531ccc74392466a22a108d731db542e%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C1%7C637032690392226873=8QvcS%2FszcjdYrGxDPFrfWbj3g2p1lsYf9TDCfekFPFA%3D=0>
 you can find the result of the pipeline, which includes builds for several 
platforms (click on the "Artifacts" button, the one which looks like a cloud, 
to get them). The code is being developed at 
https://gitlab.haskell.org/trupill/ghc<https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgitlab.haskell.org%2Ftrupill%2Fghc=02%7C01%7Csimonpj%40microsoft.com%7Cb531ccc74392466a22a108d731db542e%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C1%7C637032690392236867=z05Ryg2y9fWVLixdQ63I%2F%2Fqzo05xS93LICRdq3HDETc%3D=0>.

Any code should run *unchanged* except for some eta-expansion required for some 
specific usage patterns of higher-rank types. Please don't hesitate to ask any 
questions or clarifications about it. A merge request for tracking this can be 
found at 
https://gitlab.haskell.org/ghc/ghc/merge_requests/1659<https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgitlab.haskell.org%2Fghc%2Fghc%2Fmerge_requests%2F1659=02%7C01%7Csimonpj%40microsoft.com%7Cb531ccc74392466a22a108d731db542e%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C1%7C637032690392236867=q4zboFik4oGZaFZ4pk8c%2Be%2FleNQNIHsdtuf4grepj2k%3D=0>

Kind regards,
Alejandro
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: New implementation for `ImpredicativeTypes`

[Alejandro Serrano Mena]

To follow up on this, the current spec. is available in the following PDF:
https://www.dropbox.com/s/hxjp28ym3lptmxw/quick-look-steps.pdf?dl=0

El mié., 4 sept. 2019 a las 17:13, Alejandro Serrano Mena (<
trup...@gmail.com>) escribió:

> Hi all,
> As I mentioned some time ago, we have been busy working on a new
> implementation of `ImpredicativeTypes` for GHC. I am very thankful to
> everybody who back then sent us examples of impredicativity which would be
> nice to support, as far as we know this branch supports all of them! :)
>
> If you want to try it, at
> https://gitlab.haskell.org/trupill/ghc/commit/a3f95a0fe0f647702fd7225fa719a8062a4cc0a5/pipelines?ref=quick-look-build
> you can find the result of the pipeline, which includes builds for several
> platforms (click on the "Artifacts" button, the one which looks like a
> cloud, to get them). The code is being developed at
> https://gitlab.haskell.org/trupill/ghc.
>
> Any code should run *unchanged* except for some eta-expansion required for
> some specific usage patterns of higher-rank types. Please don't hesitate to
> ask any questions or clarifications about it. A merge request for tracking
> this can be found at
> https://gitlab.haskell.org/ghc/ghc/merge_requests/1659
>
> Kind regards,
> Alejandro
>
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs