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 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 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 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