> On Sep 2, 2021, at 2:56 PM, john.ericson <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`. I think you're after newtype existentials. I think these should indeed be possible, because what you propose appears to be the same as newtype Some f = MkSome (exists a. f a) We can probably support the syntax you wrote, too, but I don't want to commit to that right now. Richard > > > ---- On Thu, 02 Sep 2021 14:33:40 -0400 li...@richarde.dev wrote ---- > > > > On Sep 2, 2021, at 2:10 PM, Alex Rozenshteyn <rpglove...@gmail.com > <mailto:rpglove...@gmail.com>> wrote: > > Oh, I see. That's because this would need to introduce `pack ... as ...` and > `open ...` into the core term language, right? > > 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 <john.ericson@obsidian.systems > <mailto:john.ericson@obsidian.systems>> wrote: > > This reminds me...can we do newtype GADTs in certain situations as a stepping > stone? I would think that would be purely easier — more nominal, no nice > projections but only `case` and skolems which cannot escape. > > Newtype GADTs we're long deemed impossible IIRC, but surely the paper > demonstrates that at least some cases should work? > > I don't quite see how this relates to existentials. Note that the paper does > not address e.g. packing equalities in existentials, which would be needed > for interacting with GADTs. > > Glad folks are enjoying the paper! :) > > Richard > > > > ---- On Thu, 02 Sep 2021 14:10:34 -0400 rpglove...@gmail.com > <mailto:rpglove...@gmail.com> wrote ---- > > Oh, I see. That's because this would need to introduce `pack ... as ...` and > `open ...` into the core term language, right? > > My sense is that it shouldn't negatively affect runtime performance of > programs without existentials even if implemented naively; does that seem > accurate? Not that implementing it, even naively, is a small task. > > On Thu, Sep 2, 2021 at 1:44 PM Simon Peyton Jones <simo...@microsoft.com > <mailto:simo...@microsoft.com>> wrote: > Of course not. The same was true for QuickLook, though, wasn't it? > > No, not at all. QuickLook required zero changes to GHC’s intermediate > language – it impacted only the type inference system. Adding existentials > will entail a substantial change to the intermediate language, affecting > every optimisation pass. > > > > Simon > > > > From: Alex Rozenshteyn <rpglove...@gmail.com <mailto:rpglove...@gmail.com>> > Sent: 02 September 2021 18:13 > To: Simon Peyton Jones <simo...@microsoft.com <mailto:simo...@microsoft.com>> > Cc: GHC developers <ghc-devs@haskell.org <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 <simo...@microsoft.com > <mailto:simo...@microsoft.com>> wrote: > > If I understand correctly, the recent ICFP paper "An Existential Crisis > Resolved > <https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fdl.acm.org%2Fdoi%2Fpdf%2F10.1145%2F3473569&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 <rpglove...@gmail.com <mailto:rpglove...@gmail.com>> > Sent: 02 September 2021 17:10 > To: Simon Peyton Jones <simo...@microsoft.com <mailto:simo...@microsoft.com>> > Cc: GHC developers <ghc-devs@haskell.org <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 <simo...@microsoft.com > <mailto:simo...@microsoft.com>> wrote: > > Suppose Haskell did have existentials; > > > > Yes, I think that’s an interesting thing to work on! I’m not sure what the > implications would be. At very least we’d need to extend System FC (GHC’s > intermediate language) with existential types and the corresponding pack and > unpack syntactic forms. > > > > I don’t know of any work studying that question specifically, but others may > have pointers. > > > > simon > > > > From: Alex Rozenshteyn <rpglove...@gmail.com <mailto:rpglove...@gmail.com>> > Sent: 06 September 2019 15:21 > To: Simon Peyton Jones <simo...@microsoft.com <mailto:simo...@microsoft.com>> > Cc: Alejandro Serrano Mena <trup...@gmail.com <mailto:trup...@gmail.com>>; > GHC developers <ghc-devs@haskell.org <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 <simo...@microsoft.com > <mailto:simo...@microsoft.com>> wrote: > > I’m confused. Char does not have the type (forall a. Show a =>a), so our > example is iill-typed in System F, never mind about type inference. Perhaps > there’s a typo? I think you may have ment > > exists a. Show a => a > > which doesn’t exist in Haskell. You can write existentials with a data type > > > > data Showable where > > S :: forall a. Show a => a -> Showable > > > > Then > > map show [S 1, S ‘a’, S “b”] > > works fine today (without our new stuff), provided you say > > > > instance Show Showable where > > show (S x) = show x > > > > Our new system can only type programs that can be written in System F. (The > tricky bit is inferring the impredicative instantiations.) > > > > Simon > > > > From: ghc-devs <ghc-devs-boun...@haskell.org > <mailto:ghc-devs-boun...@haskell.org>> On Behalf Of Alex Rozenshteyn > Sent: 06 September 2019 03:31 > To: Alejandro Serrano Mena <trup...@gmail.com <mailto:trup...@gmail.com>> > Cc: GHC developers <ghc-devs@haskell.org <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 <trup...@gmail.com > <mailto:trup...@gmail.com>> wrote: > > Hi all, > > As I mentioned some time ago, we have been busy working on a new > implementation of `ImpredicativeTypes` for GHC. I am very thankful to > everybody who back then sent us examples of impredicativity which would be > nice to support, as far as we know this branch supports all of them! :) > > > > If you want to try it, > athttps://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%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 >
_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
