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? ---- 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:13
To: 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:10
To: 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:21
To: 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 => 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>
On Behalf Of Alex Rozenshteyn
Sent: 06 September 2019 03:31
To: 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, 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
ghc-devs@haskell.org
http://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
