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

[David Feuer]

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20160524/2055d699/attachment.html>