New implementation for `ImpredicativeTypes`

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

New implementation for `ImpredicativeTypes`

Alejandro Serrano Mena
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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

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 (<[hidden email]>) 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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

RE: New implementation for `ImpredicativeTypes`

GHC - devs mailing list

I update the MR Description to make the link more discoverable.

 

S

 

From: ghc-devs <[hidden email]> On Behalf Of Alejandro Serrano Mena
Sent: 05 September 2019 09:30
To: GHC developers <[hidden email]>
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

 

El mié., 4 sept. 2019 a las 17:13, Alejandro Serrano Mena (<[hidden email]>) 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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: New implementation for `ImpredicativeTypes`

Alex Rozenshteyn
In reply to this post by Alejandro Serrano Mena
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 <[hidden email]> 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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

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

RE: New implementation for `ImpredicativeTypes`

GHC - devs mailing list

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 <[hidden email]> On Behalf Of Alex Rozenshteyn
Sent: 06 September 2019 03:31
To: Alejandro Serrano Mena <[hidden email]>
Cc: GHC developers <[hidden email]>
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 <[hidden email]> 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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs


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

Re: 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 <[hidden email]> 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 <[hidden email]> On Behalf Of Alex Rozenshteyn
Sent: 06 September 2019 03:31
To: Alejandro Serrano Mena <[hidden email]>
Cc: GHC developers <[hidden email]>
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 <[hidden email]> 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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs


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

Re: 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 <[hidden email]> 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 <[hidden email]> 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 <[hidden email]> On Behalf Of Alex Rozenshteyn
>> Sent: 06 September 2019 03:31
>> To: Alejandro Serrano Mena <[hidden email]>
>> Cc: GHC developers <[hidden email]>
>> 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 <[hidden email]> 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
>> [hidden email]
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
> _______________________________________________
> ghc-devs mailing list
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: New implementation for `ImpredicativeTypes`

Alejandro Serrano Mena
In reply to this post by Alex Rozenshteyn
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 (<[hidden email]>) 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 <[hidden email]> 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 <[hidden email]> On Behalf Of Alex Rozenshteyn
Sent: 06 September 2019 03:31
To: Alejandro Serrano Mena <[hidden email]>
Cc: GHC developers <[hidden email]>
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 <[hidden email]> 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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs


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

Re: New implementation for `ImpredicativeTypes`

Vladislav Zavialov-2
In reply to this post by Iavor Diatchki
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 <[hidden email]> 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 <[hidden email]> 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 <[hidden email]> 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 <[hidden email]> On Behalf Of Alex Rozenshteyn
>>> Sent: 06 September 2019 03:31
>>> To: Alejandro Serrano Mena <[hidden email]>
>>> Cc: GHC developers <[hidden email]>
>>> 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 <[hidden email]> 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
>>> [hidden email]
>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>>
>> _______________________________________________
>> ghc-devs mailing list
>> [hidden email]
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
> _______________________________________________
> ghc-devs mailing list
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

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

Re: 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
<[hidden email]> 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 <[hidden email]> 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 <[hidden email]> 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 <[hidden email]> 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 <[hidden email]> On Behalf Of Alex Rozenshteyn
> >>> Sent: 06 September 2019 03:31
> >>> To: Alejandro Serrano Mena <[hidden email]>
> >>> Cc: GHC developers <[hidden email]>
> >>> 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 <[hidden email]> 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
> >>> [hidden email]
> >>> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
> >>
> >> _______________________________________________
> >> ghc-devs mailing list
> >> [hidden email]
> >> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
> > _______________________________________________
> > ghc-devs mailing list
> > [hidden email]
> > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: New implementation for `ImpredicativeTypes`

Vladislav Zavialov-2
No, I don’t expect the compiler to infer existential quantification, just like it doesn’t infer higher-rank universal quantification. However, I believe we could check terms against user-written types that contain existentials.

- Vlad

> On 6 Sep 2019, at 23:48, Iavor Diatchki <[hidden email]> wrote:
>
> Why would you infer this type as opposed to `[exists a. a]`?
>
> On Fri, Sep 6, 2019 at 12:08 PM Vladislav Zavialov
> <[hidden email]> 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

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

RE: New implementation for `ImpredicativeTypes`

GHC - devs mailing list
In reply to this post by Alex Rozenshteyn

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 <[hidden email]>
Sent: 06 September 2019 15:21
To: Simon Peyton Jones <[hidden email]>
Cc: Alejandro Serrano Mena <[hidden email]>; GHC developers <[hidden email]>
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 <[hidden email]> 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 <[hidden email]> On Behalf Of Alex Rozenshteyn
Sent: 06 September 2019 03:31
To: Alejandro Serrano Mena <[hidden email]>
Cc: GHC developers <[hidden email]>
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 <[hidden email]> 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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs


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