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

[David Feuer]

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

> David Feuer <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/dcc1e329/attachment.html>