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

[Carter Schonwald]

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 <david.feuer at gmail.com> 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" <ben at well-typed.com
> <javascript:_e(%7B%7D,'cvml','ben at well-typed.com');>> wrote:
>
>> David Feuer <david.feuer at gmail.com
>> <javascript:_e(%7B%7D,'cvml','david.feuer at 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-existentially-quantified-newtype-in-ghc-haskell
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20160524/74440294/attachment.html>