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

Ben Gamari ben at well-typed.com
Tue May 24 16:43:02 UTC 2016


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 --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 472 bytes
Desc: not available
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20160524/1f22cc95/attachment.sig>


More information about the ghc-devs mailing list