Unpacking single-field, single-strict-constructor GADTs and existentials
Simon Peyton Jones
simonpj at microsoft.com
Wed May 25 07:27:51 UTC 2016
I'm not following the details of this discussion. Would it be possible to write a compact summary, with the key examples, in the appropriate ticket?
I think that https://ghc.haskell.org/trac/ghc/ticket/10016 is one such ticket, but I think there may be more than one issue at stake here. For example, #10016 can be done in a strongly typed way in Core; but #1965 cannot (so far as I know).
It could also help to have a wiki page to summarise the cluster of issues, pointing to the appropriate tickets for individual cases.
An articulate summary will make it much more likely that progress is made! Thanks.
| -----Original Message-----
| From: ghc-devs [mailto:ghc-devs-bounces at haskell.org] On Behalf Of David Feuer
| Sent: 24 May 2016 23:14
| To: Carter Schonwald <carter.schonwald at gmail.com>
| Cc: ghc-devs <ghc-devs at haskell.org>
| Subject: Re: Unpacking single-field, single-strict-constructor GADTs and
| Unboxing, per se, is not required; only newtype optimization. I
| believe Ed would probably have mentioned something when I discussed
| the issue with him if he'd already had an idea for hacking around it.
| Instead, he said he wanted the feature too.
| On Tue, May 24, 2016 at 6:03 PM, Carter Schonwald
| <carter.schonwald at gmail.com> wrote:
| > Phrased differently: there's a subclass of existential data types which
| > a well behaved unboxed memory layout?
| > @ David : have you tried simulating this in userland using eds structs /
| > structures lib?
| > On Tuesday, May 24, 2016, David Feuer <david.feuer at gmail.com> wrote:
| >> I should mention that while this does not require UNPACKing sum types (or
| >> any of the difficult trade-offs that involves), it lets programmers
| >> accomplish such unpacking by hand under sufficiently general conditions to
| >> be quite useful in practice. As long as the set of types involved is
| >> it'll do.
| >> David Feuer <david.feuer at gmail.com> writes:
| >> > Given
| >> >
| >> > data Big a = B1 !(Small1 a) | B2 !(Small2 a) | B3 !(Small3 a), where the
| >> > Small types are (possibly recursive) sums, it's generally possible to
| >> > express that as something like
| >> >
| >> > data Selector = One | Two | Three
| >> > data Big a = forall (x :: Selector) .
| >> > Big !(BigG x a)
| >> > data BigG x a where
| >> > GB1a :: some -> fields -> BigG 'One a
| >> > GB1b :: fields -> BigG 'One a
| >> > GB2a :: whatever -> BigG 'Two a
| >> > GB3a :: yeah -> BigG 'Three a
| >> >
| >> > Making one big GADT from all the constructors of the "small" types, and
| >> > then wrapping it up in an existential. That's what I meant about
| >> > "unpacking". But for efficiency purposes, that wrapper needs the newtype
| >> > optimization.
| >> Yes, but you'd need to unbox a sum in this case, no? I think this is the
| >> first issue that you need to solve before you can talk about dealing
| >> with the polymorphism issue (although hopefully Ömer will make progress
| >> on this for 8.2).
| >> Cheers,
| >> - Ben
| ghc-devs mailing list
| ghc-devs at haskell.org
More information about the ghc-devs