I update the MR Descriptionhttps://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=0https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fwww.dropbox.com%2Fs%2Fhxjp28ym3lptmxw%2Fquick-look-steps.pdf%3Fdl%3D0&data=02%7C01%7Csimonpj%40microsoft.com%7Cb531ccc74392466a22a108d731db542e%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C1%7C637032690392226873&sdata=b%2FE4R3wka1%2FEgBqcg3MhJe8LZq7tP3UTs%2FHVqMVHKKw%3D&reserved=0 El mié., 4 sept. 2019 a las 17:13, Alejandro Serrano Mena (mailto:trupill@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/a3f95a0fe0f647702fd7225fa719a8...https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgitlab.haskell.org%2Ftrupill%2Fghc%2Fcommit%2Fa3f95a0fe0f647702fd7225fa719a8062a4cc0a5%2Fpipelines%3Fref%3Dquick-look-build&data=02%7C01%7Csimonpj%40microsoft.com%7Cb531ccc74392466a22a108d731db542e%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C1%7C637032690392226873&sdata=8QvcS%2FszcjdYrGxDPFrfWbj3g2p1lsYf9TDCfekFPFA%3D&reserved=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/ghchttps://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgitlab.haskell.org%2Ftrupill%2Fghc&data=02%7C01%7Csimonpj%40microsoft.com%7Cb531ccc74392466a22a108d731db542e%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C1%7C637032690392236867&sdata=z05Ryg2y9fWVLixdQ63I%2F%2Fqzo05xS93LICRdq3HDETc%3D&reserved=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/1659https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgitlab.haskell.org%2Fghc%2Fghc%2Fmerge_requests%2F1659&data=02%7C01%7Csimonpj%40microsoft.com%7Cb531ccc74392466a22a108d731db542e%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C1%7C637032690392236867&sdata=q4zboFik4oGZaFZ4pk8c%2Be%2FleNQNIHsdtuf4grepj2k%3D&reserved=0 Kind regards, Alejandro

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&depth=9https://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&data=02%7C01%7Csimonpj%40microsoft.com%7Cf5bddbe8c13b424fad8a08d732724d04%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637033338810706935&sdata=a5c3ujC0kiPlocgHg8AX%2BwIP6ZH2hnqszCpnWOiqpGQ%3D&reserved=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:trupill@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/a3f95a0fe0f647702fd7225fa719a8...https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgitlab.haskell.org%2Ftrupill%2Fghc%2Fcommit%2Fa3f95a0fe0f647702fd7225fa719a8062a4cc0a5%2Fpipelines%3Fref%3Dquick-look-build&data=02%7C01%7Csimonpj%40microsoft.com%7Cf5bddbe8c13b424fad8a08d732724d04%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637033338810716935&sdata=PP1imEsNrkIhloEV3AS52nrZBtyjen4i1e3pJTcMi6M%3D&reserved=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/ghchttps://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgitlab.haskell.org%2Ftrupill%2Fghc&data=02%7C01%7Csimonpj%40microsoft.com%7Cf5bddbe8c13b424fad8a08d732724d04%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637033338810716935&sdata=IgtSqJP4%2BhCfy3%2FHVsqX6wpPYVMS8D1wN46aXHnFcUw%3D&reserved=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/1659https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgitlab.haskell.org%2Fghc%2Fghc%2Fmerge_requests%2F1659&data=02%7C01%7Csimonpj%40microsoft.com%7Cf5bddbe8c13b424fad8a08d732724d04%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637033338810716935&sdata=YJ5N9d7gXC2JbpqTvpqs4wjY%2F7Ev%2FikRdYIK%2Bhv4rRE%3D&reserved=0 Kind regards, Alejandro _______________________________________________ ghc-devs mailing list ghc-devs@haskell.orgmailto:ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devshttps://nam06.safelinks.protection.outlook.com/?url=http%3A%2F%2Fmail.haskell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc-devs&data=02%7C01%7Csimonpj%40microsoft.com%7Cf5bddbe8c13b424fad8a08d732724d04%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637033338810726922&sdata=jw0sroJW1D8MoBBxVKJROdGefo5gir%2BtQSto0b%2Bj3NA%3D&reserved=0

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&depth=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/a3f95a0fe0f647702fd7225fa719a8... 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

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

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&depth=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/a3f95a0fe0f647702fd7225fa719a8... 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

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

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&depth=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&data=02%7C01%7Csimonpj%40microsoft.com%7Cf5bddbe8c13b424fad8a08d732724d04%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637033338810706935&sdata=a5c3ujC0kiPlocgHg8AX%2BwIP6ZH2hnqszCpnWOiqpGQ%3D&reserved=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/a3f95a0fe0f647702fd7225fa719a8... https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgitlab.haskell.org%2Ftrupill%2Fghc%2Fcommit%2Fa3f95a0fe0f647702fd7225fa719a8062a4cc0a5%2Fpipelines%3Fref%3Dquick-look-build&data=02%7C01%7Csimonpj%40microsoft.com%7Cf5bddbe8c13b424fad8a08d732724d04%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637033338810716935&sdata=PP1imEsNrkIhloEV3AS52nrZBtyjen4i1e3pJTcMi6M%3D&reserved=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&data=02%7C01%7Csimonpj%40microsoft.com%7Cf5bddbe8c13b424fad8a08d732724d04%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637033338810716935&sdata=IgtSqJP4%2BhCfy3%2FHVsqX6wpPYVMS8D1wN46aXHnFcUw%3D&reserved=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&data=02%7C01%7Csimonpj%40microsoft.com%7Cf5bddbe8c13b424fad8a08d732724d04%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637033338810716935&sdata=YJ5N9d7gXC2JbpqTvpqs4wjY%2F7Ev%2FikRdYIK%2Bhv4rRE%3D&reserved=0

Kind regards,

Alejandro

_______________________________________________ ghc-devs mailing list 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&data=02%7C01%7Csimonpj%40microsoft.com%7Cf5bddbe8c13b424fad8a08d732724d04%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637033338810726922&sdata=jw0sroJW1D8MoBBxVKJROdGefo5gir%2BtQSto0b%2Bj3NA%3D&reserved=0

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&depth=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&data=02%7C01%7Csimonpj%40microsoft.com%7C911c05e1dc5041e685bd08d732d57261%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637033764634397513&sdata=IeOaMmtbwIFEXOBwvLkElsqqS84q50QjFD7MFW0hpK8%3D&reserved=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/a3f95a0fe0f647702fd7225fa719a8... https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgitlab.haskell.org%2Ftrupill%2Fghc%2Fcommit%2Fa3f95a0fe0f647702fd7225fa719a8062a4cc0a5%2Fpipelines%3Fref%3Dquick-look-build&data=02%7C01%7Csimonpj%40microsoft.com%7C911c05e1dc5041e685bd08d732d57261%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637033764634397513&sdata=fWmUVHUC5hFG%2FBqNwXl1N4par46XLdHQAUxs2DstpvQ%3D&reserved=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&data=02%7C01%7Csimonpj%40microsoft.com%7C911c05e1dc5041e685bd08d732d57261%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637033764634407517&sdata=OMEyEff9CzH3iNG6DHUL%2B5TRSCgYLmEXikD9M7BBdQE%3D&reserved=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&data=02%7C01%7Csimonpj%40microsoft.com%7C911c05e1dc5041e685bd08d732d57261%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637033764634407517&sdata=lkLoNtsgThjpOO%2BEujkwYk3%2BujMrcymJJtrJ7w9FDbY%3D&reserved=0

Kind regards,

Alejandro

_______________________________________________ ghc-devs mailing list 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&data=02%7C01%7Csimonpj%40microsoft.com%7C911c05e1dc5041e685bd08d732d57261%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637033764634417525&sdata=2ayQ0%2Fz0YHIxyCVNGybOigFIxCmsd2lEFeQYSbSrvv4%3D&reserved=0

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&data=04%7C01%7Csimonpj%40microsoft.com%7Caee2e0a922204ae3611208d96e2c2c57%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637661959634445057%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=wsN3Z7t8jCiExzl38%2F2IwNNsPH3Pq5CHJ7dQca5R2Y4%3D&reserved=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&data=04%7C01%7Csimonpj%40microsoft.com%7Caee2e0a922204ae3611208d96e2c2c57%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637661959634445057%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=wsN3Z7t8jCiExzl38%2F2IwNNsPH3Pq5CHJ7dQca5R2Y4%3D&reserved=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 *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&depth=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&data=04%7C01%7Csimonpj%40microsoft.com%7Caee2e0a922204ae3611208d96e2c2c57%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637661959634445057%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=HEn92VgTK3lOrYywm7gml4kn%2BYRreZXxtCKvLib805g%3D&reserved=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/a3f95a0fe0f647702fd7225fa719a8... https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgitlab.haskell.org%2Ftrupill%2Fghc%2Fcommit%2Fa3f95a0fe0f647702fd7225fa719a8062a4cc0a5%2Fpipelines%3Fref%3Dquick-look-build&data=04%7C01%7Csimonpj%40microsoft.com%7Caee2e0a922204ae3611208d96e2c2c57%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637661959634455057%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=v5%2BPdW%2Fcx2OXNiIrQ8Dsa45rUgh1CRr6ERNzxbihxoA%3D&reserved=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&data=04%7C01%7Csimonpj%40microsoft.com%7Caee2e0a922204ae3611208d96e2c2c57%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637661959634465051%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=pFQzrPCiZXF0Y3KqmxjlhrDX1EVddJqII%2B%2BPTJb65h8%3D&reserved=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&data=04%7C01%7Csimonpj%40microsoft.com%7Caee2e0a922204ae3611208d96e2c2c57%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637661959634475049%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=j0JcM0Q%2Bj7JSSb6lV%2F6Aj4lAZWjAysg%2FHg5cb4x00%2FY%3D&reserved=0

Kind regards,

Alejandro

_______________________________________________ ghc-devs mailing list 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&data=04%7C01%7Csimonpj%40microsoft.com%7Caee2e0a922204ae3611208d96e2c2c57%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637661959634485038%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=9i55zUcM%2BX%2FN7ngvTARBOvfm962IJ9SYfxfa46f7wm8%3D&reserved=0

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&data=04%7C01%7Csimonpj%40microsoft.com%7Cc0f0a66e10f94a6f17d508d96e34f2ae%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637661997328916809%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=kioGsomPn8BuvBLQx6KEr5glMTPvw6m93DK%2BGA0lM08%3D&reserved=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&data=04%7C01%7Csimonpj%40microsoft.com%7Cc0f0a66e10f94a6f17d508d96e34f2ae%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637661997328926803%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=DtcIgtgrp3zJygorYY32WBKhF40rYtAOhMOOmPWf6pc%3D&reserved=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 *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&depth=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&data=04%7C01%7Csimonpj%40microsoft.com%7Cc0f0a66e10f94a6f17d508d96e34f2ae%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637661997328936796%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=IFOf9nl11qhDksPnK9jf2HxcHm7QMhVUGJZX%2F%2FOVim4%3D&reserved=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/a3f95a0fe0f647702fd7225fa719a8... https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgitlab.haskell.org%2Ftrupill%2Fghc%2Fcommit%2Fa3f95a0fe0f647702fd7225fa719a8062a4cc0a5%2Fpipelines%3Fref%3Dquick-look-build&data=04%7C01%7Csimonpj%40microsoft.com%7Cc0f0a66e10f94a6f17d508d96e34f2ae%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637661997328936796%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=eR1k8ntH2aGT5nTFOQxd86hGr5OxDSjmkxFpy09fGlg%3D&reserved=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&data=04%7C01%7Csimonpj%40microsoft.com%7Cc0f0a66e10f94a6f17d508d96e34f2ae%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637661997328946794%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=RdfPCIqvBF8VyeuGKmtOBJsnwcPl%2Bya%2B4KLi%2BWfrT3E%3D&reserved=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&data=04%7C01%7Csimonpj%40microsoft.com%7Cc0f0a66e10f94a6f17d508d96e34f2ae%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637661997328956787%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=aR6Lq4teuUmPe4o%2FOHp878Zm8OBfXVxoMrn0WqcN4fM%3D&reserved=0

Kind regards,

Alejandro

_______________________________________________ ghc-devs mailing list 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&data=04%7C01%7Csimonpj%40microsoft.com%7Cc0f0a66e10f94a6f17d508d96e34f2ae%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637661997328956787%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=IUsQu1gDuNetafA6ljvQwNBEYq%2F%2B2NFYqwT5Ytpal24%3D&reserved=0

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 rpglover64@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:simonpj@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:rpglover64@gmail.com> Sent: 02 September 2021 18:13 To: Simon Peyton Jones mailto:simonpj@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:simonpj@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&data=04%7C01%7Csimonpj%40microsoft.com%7Cc0f0a66e10f94a6f17d508d96e34f2ae%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637661997328916809%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=kioGsomPn8BuvBLQx6KEr5glMTPvw6m93DK%2BGA0lM08%3D&reserved=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:rpglover64@gmail.com> Sent: 02 September 2021 17:10 To: Simon Peyton Jones mailto:simonpj@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&data=04%7C01%7Csimonpj%40microsoft.com%7Cc0f0a66e10f94a6f17d508d96e34f2ae%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637661997328926803%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=DtcIgtgrp3zJygorYY32WBKhF40rYtAOhMOOmPWf6pc%3D&reserved=0" finally enables this; is that right?

On Mon, Sep 9, 2019 at 12:00 PM Simon Peyton Jones mailto:simonpj@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:rpglover64@gmail.com> Sent: 06 September 2019 15:21 To: Simon Peyton Jones mailto:simonpj@microsoft.com> Cc: Alejandro Serrano Mena mailto:trupill@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:simonpj@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-bounces@haskell.org> On Behalf Of Alex Rozenshteyn Sent: 06 September 2019 03:31 To: Alejandro Serrano Mena mailto:trupill@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&depth=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&data=04%7C01%7Csimonpj%40microsoft.com%7Cc0f0a66e10f94a6f17d508d96e34f2ae%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637661997328936796%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=IFOf9nl11qhDksPnK9jf2HxcHm7QMhVUGJZX%2F%2FOVim4%3D&reserved=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:trupill@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, athttps://gitlab.haskell.org/trupill/ghc/commit/a3f95a0fe0f647702fd7225fa719a8... https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgitlab.haskell.org%2Ftrupill%2Fghc%2Fcommit%2Fa3f95a0fe0f647702fd7225fa719a8062a4cc0a5%2Fpipelines%3Fref%3Dquick-look-build&data=04%7C01%7Csimonpj%40microsoft.com%7Cc0f0a66e10f94a6f17d508d96e34f2ae%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637661997328936796%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=eR1k8ntH2aGT5nTFOQxd86hGr5OxDSjmkxFpy09fGlg%3D&reserved=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&data=04%7C01%7Csimonpj%40microsoft.com%7Cc0f0a66e10f94a6f17d508d96e34f2ae%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637661997328946794%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=RdfPCIqvBF8VyeuGKmtOBJsnwcPl%2Bya%2B4KLi%2BWfrT3E%3D&reserved=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&data=04%7C01%7Csimonpj%40microsoft.com%7Cc0f0a66e10f94a6f17d508d96e34f2ae%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637661997328956787%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=aR6Lq4teuUmPe4o%2FOHp878Zm8OBfXVxoMrn0WqcN4fM%3D&reserved=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&data=04%7C01%7Csimonpj%40microsoft.com%7Cc0f0a66e10f94a6f17d508d96e34f2ae%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637661997328956787%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=IUsQu1gDuNetafA6ljvQwNBEYq%2F%2B2NFYqwT5Ytpal24%3D&reserved=0_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org mailto:ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs 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

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 lists@richarde.dev wrote ----

On Sep 2, 2021, at 2:10 PM, Alex Rozenshteyn mailto:rpglover64@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 rpglover64@gmail.com mailto:rpglover64@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:simonpj@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:rpglover64@gmail.com> Sent: 02 September 2021 18:13 To: Simon Peyton Jones mailto:simonpj@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:simonpj@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&data=04%7C01%7Csimonpj%40microsoft.com%7Cc0f0a66e10f94a6f17d508d96e34f2ae%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637661997328916809%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=kioGsomPn8BuvBLQx6KEr5glMTPvw6m93DK%2BGA0lM08%3D&reserved=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:rpglover64@gmail.com> Sent: 02 September 2021 17:10 To: Simon Peyton Jones mailto:simonpj@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&data=04%7C01%7Csimonpj%40microsoft.com%7Cc0f0a66e10f94a6f17d508d96e34f2ae%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637661997328926803%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=DtcIgtgrp3zJygorYY32WBKhF40rYtAOhMOOmPWf6pc%3D&reserved=0" finally enables this; is that right?

On Mon, Sep 9, 2019 at 12:00 PM Simon Peyton Jones mailto:simonpj@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:rpglover64@gmail.com> Sent: 06 September 2019 15:21 To: Simon Peyton Jones mailto:simonpj@microsoft.com> Cc: Alejandro Serrano Mena mailto:trupill@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:simonpj@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-bounces@haskell.org> On Behalf Of Alex Rozenshteyn Sent: 06 September 2019 03:31 To: Alejandro Serrano Mena mailto:trupill@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&depth=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&data=04%7C01%7Csimonpj%40microsoft.com%7Cc0f0a66e10f94a6f17d508d96e34f2ae%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637661997328936796%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=IFOf9nl11qhDksPnK9jf2HxcHm7QMhVUGJZX%2F%2FOVim4%3D&reserved=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:trupill@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, athttps://gitlab.haskell.org/trupill/ghc/commit/a3f95a0fe0f647702fd7225fa719a8... https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgitlab.haskell.org%2Ftrupill%2Fghc%2Fcommit%2Fa3f95a0fe0f647702fd7225fa719a8062a4cc0a5%2Fpipelines%3Fref%3Dquick-look-build&data=04%7C01%7Csimonpj%40microsoft.com%7Cc0f0a66e10f94a6f17d508d96e34f2ae%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637661997328936796%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=eR1k8ntH2aGT5nTFOQxd86hGr5OxDSjmkxFpy09fGlg%3D&reserved=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&data=04%7C01%7Csimonpj%40microsoft.com%7Cc0f0a66e10f94a6f17d508d96e34f2ae%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637661997328946794%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=RdfPCIqvBF8VyeuGKmtOBJsnwcPl%2Bya%2B4KLi%2BWfrT3E%3D&reserved=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&data=04%7C01%7Csimonpj%40microsoft.com%7Cc0f0a66e10f94a6f17d508d96e34f2ae%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637661997328956787%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=aR6Lq4teuUmPe4o%2FOHp878Zm8OBfXVxoMrn0WqcN4fM%3D&reserved=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&data=04%7C01%7Csimonpj%40microsoft.com%7Cc0f0a66e10f94a6f17d508d96e34f2ae%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637661997328956787%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=IUsQu1gDuNetafA6ljvQwNBEYq%2F%2B2NFYqwT5Ytpal24%3D&reserved=0_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org mailto:ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org mailto:ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs 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

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 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.

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