New implementation for `ImpredicativeTypes`

Alex Rozenshteyn rpglover64 at gmail.com
Thu Sep 2 17:13:00 UTC 2021


>
> 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 <simonpj at 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%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 <rpglover64 at gmail.com>
> *Sent:* 02 September 2021 17:10
> *To:* Simon Peyton Jones <simonpj at microsoft.com>
> *Cc:* GHC developers <ghc-devs at 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%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 <simonpj at 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 <rpglover64 at gmail.com>
> *Sent:* 06 September 2019 15:21
> *To:* Simon Peyton Jones <simonpj at microsoft.com>
> *Cc:* Alejandro Serrano Mena <trupill at gmail.com>; GHC developers <
> ghc-devs at 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 <simonpj at 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 <ghc-devs-bounces at haskell.org> *On Behalf Of *Alex
> Rozenshteyn
> *Sent:* 06 September 2019 03:31
> *To:* Alejandro Serrano Mena <trupill at gmail.com>
> *Cc:* GHC developers <ghc-devs at 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%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 <trupill at gmail.com>
> wrote:
>
> Hi all,
>
> As I mentioned some time ago, we have been busy working on a new
> implementation of `ImpredicativeTypes` for GHC. I am very thankful to
> everybody who back then sent us examples of impredicativity which would be
> nice to support, as far as we know this branch supports all of them! :)
>
>
>
> If you want to try it, at
> https://gitlab.haskell.org/trupill/ghc/commit/a3f95a0fe0f647702fd7225fa719a8062a4cc0a5/pipelines?ref=quick-look-build
> <https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgitlab.haskell.org%2Ftrupill%2Fghc%2Fcommit%2Fa3f95a0fe0f647702fd7225fa719a8062a4cc0a5%2Fpipelines%3Fref%3Dquick-look-build&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 at 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>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20210902/18bff05b/attachment-0001.html>


More information about the ghc-devs mailing list