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

This sounds to me like what we're trying to describe here smells like an unboxed existential , which is a hairs breadth out of reach of ghcs type system @david have you tried out eds structures package? It may provide the right tooling to simulate this or something close to what you want. On Tuesday, May 24, 2016, David Feuer wrote:

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. On May 24, 2016 4:16 AM, "Ben Gamari" javascript:_e(%7B%7D,'cvml','ben@well-typed.com');> wrote:

...

David Feuer javascript:_e(%7B%7D,'cvml','david.feuer@gmail.com');> writes:

...

Data.IntMap could be cleaned up some if single-field, single strict constructor GADTs/existentials could be unpacked even when wrapping a sum type. We could then have

data Status = E | NE data IntMap' (s :: Status) a where Bin :: ... -> ... -> !(IntMap' NE a) -> !(IntMap' NE a) -> IntMap' NE a Tip :: ... -> a -> IntMap' NE a Nil :: IntMap' E a data IntMap a = forall s . IM {-# UNPACK #-} !(IntMap' s a)

I'm not sure I understand how the existential helps you unpack this sum. Surely I'm missing something.

...

The representation would be the same as that of a newtype, but the pattern matching semantics would be strict. In the GADT case, this would essentially allow any fixed concrete datatype to serve directly as a witness for an arbitrary set of type equalities demanded on construction.

Is there any hope something like this could happen?

Ignoring the sum issue for a moment:

My understanding is that it ought to be possible to unpack at least single-constructor types in an existentially quantified datacon, although someone needs to step up to do it. A closely related issue (existentials in newtypes) was discussed by dons in a Stack Overflow question [1] quite some time ago.

As far as I understand as long as the existentially-quantified argument is unconstrained (therefore there is no need to carry a dictionary) and of kind * (therefore has a uniform representation) there is no reason why unpacking shouldn't be possible.

The case that you cite looks to be even easier since the existential is a phantom so there is no need to represent it at all. It seems to me like it might not be so difficult to treat this case in particular. It's possible all that is necessary would be to adjust the unpackability criteria in MkId.

It actually looks like there's a rather closely related ticket already open, #10016.

Cheers,

- Ben

[1] http://stackoverflow.com/questions/5890094/is-there-a-way-to-define-an-exist...