Does the most basic e.g.newtype Some f where MkSome :: forall a. f a -> Some
fHave one of those problematic equalities? ---- On Thu, 02 Sep 2021 14:33:40
-0400 li...@richarde.dev wrote ----On Sep 2, 2021, at 2:10 PM, Alex
Rozenshteyn <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> wrote:This reminds me...can we do newtype GADTs
in certain situations as a stepping stone? I would think that would be purely
easier — more nominal, no nice projections but only `case` and skolems which
cannot escape.Newtype GADTs we're long deemed impossible IIRC, but surely the
paper demonstrates that at least some cases should work?I don't quite see how
this relates to existentials. Note that the paper does not address e.g. packing
equalities in existentials, which would be needed for interacting with
GADTs.Glad folks are enjoying the paper! :)Richard---- On Thu, 02 Sep 2021
14:10:34 -0400 rpglove...@gmail.com wrote ----Oh, I see. That's because this
would need to introduce `pack ... as ...` and `open ...` into the core term
language, right?My sense is that it shouldn't negatively affect runtime
performance of programs without existentials even if implemented naively; does
that seem accurate? Not that implementing it, even naively, is a small task. On
Thu, Sep 2, 2021 at 1:44 PM Simon Peyton Jones <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> Sent: 02 September 2021 18:13To:
Simon Peyton Jones <simo...@microsoft.com>Cc: GHC developers
<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>
wrote:If I understand correctly, the recent ICFP paper "An Existential Crisis
Resolved" finally enables this; is that right?It describes one way to include
existentials in GHC’s intermediate language, which is a real contribution. But
it is not a small change. So it’s not just a question of saying “just add that
paper to GHC and voila job done”. Simon From: Alex Rozenshteyn
<rpglove...@gmail.com> Sent: 02 September 2021 17:10To: Simon Peyton Jones
<simo...@microsoft.com>Cc: GHC developers <ghc-devs@haskell.org>Subject: Re:
New implementation for `ImpredicativeTypes` If I understand correctly, the
recent ICFP paper "An Existential Crisis Resolved" finally enables this; is
that right? On Mon, Sep 9, 2019 at 12:00 PM Simon Peyton Jones
<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> Sent: 06 September 2019 15:21To: Simon Peyton Jones
<simo...@microsoft.com>Cc: Alejandro Serrano Mena <trup...@gmail.com>; 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 <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 => awhich 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> On Behalf Of Alex
RozenshteynSent: 06 September 2019 03:31To: Alejandro Serrano Mena
<trup...@gmail.com>Cc: GHC developers <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
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> 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
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
listghc-devs@haskell.orghttp://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs_______________________________________________ghc-devs
mailing
listghc-devs@haskell.orghttp://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs_______________________________________________ghc-devs
mailing
listghc-devs@haskell.orghttp://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs_______________________________________________ghc-devs
mailing
listghc-devs@haskell.orghttp://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
