Unpacking single-field, single-strict-constructor GADTs and existentials

[Simon Peyton Jones]

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.

Simon

| -----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
| existentials
| 
| 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
| have
| > 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
| closed,
| >> 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
| https://na01.safelinks.protection.outlook.com/?url=http%3a%2f%2fmail.haskell.
| org%2fcgi-bin%2fmailman%2flistinfo%2fghc-
| devs&data=01%7c01%7csimonpj%40064d.mgd.microsoft.com%7ce98f7b01dbeb47cc8d3908
| d38420b38b%7c72f988bf86f141af91ab2d7cd011db47%7c1&sdata=gFnWAB1of%2fp%2b0IXkD
| CgcBbyxHkS7%2b4BusMl%2fs0rUySM%3d