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

[AntC]

> Simon Peyton Jones  microsoft.com> writes:
> 
> Oh, that's helpful thank you.  I have added comments!
> 

I've added a further use case (Example 3 -- from my one-eyed focus on Records).

And apologies if these are two dumb questions, but is there a bigger prize here?

If we can figure out rules for when a GADT can be 'newtype'd; 
then can we also figure it out for ordinary 'data'?

Then 'newtype' becomes more of an optimisation pragma
than a distinct declaration.

And we can smooth over that nervous cluelessness for newbies
agonising about what/whether they can newtype.
(Ref the examples in Haskell 12010 report 4.2.3.)

Also: are the conditions under which we can newtype a GADT
also the conditions under which we can implement deriving ...
That is, deriving as part of the decl, rather than standalone.
(A Summer-of-code project?)

AntC

___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

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

[David Feuer]

I've started a wiki page at
https://ghc.haskell.org/trac/ghc/wiki/NewtypeOptimizationForGADTS

On Wed, May 25, 2016 at 3:27 AM, Simon Peyton Jones
<simo...@microsoft.com> wrote:
> I'm not following the details of this discussion.  Would it be possible to 
> write a compact summary, with the key examples, in the appropriate ticket?
>
> I think that https://ghc.haskell.org/trac/ghc/ticket/10016 is one such 
> ticket, but I think there may be more than one issue at stake here.  For 
> example, #10016 can be done in a strongly typed way in Core; but #1965 cannot 
> (so far as I know).
>
> It could also help to have a wiki page to summarise the cluster of issues, 
> pointing to the appropriate tickets for individual cases.
>
> An articulate summary will make it much more likely that progress is made! 
> Thanks.
>
> Simon
>
> | -Original Message-
> | From: ghc-devs [mailto:ghc-devs-boun...@haskell.org] On Behalf Of David 
> Feuer
> | Sent: 24 May 2016 23:14
> | To: Carter Schonwald <carter.schonw...@gmail.com>
> | Cc: ghc-devs <ghc-devs@haskell.org>
> | Subject: 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
> | <carter.schonw...@gmail.com> 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 <david.fe...@gmail.com> 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 <david.fe...@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
> | ___
> | ghc-devs mailing list
> | ghc-devs@haskell.org
> | 
> https://na01.safelinks.protection.outlook.com/?url=http%3a%2f%2fmail.haskell.
> | org%2fcgi-bin%2fmailman%2flistinfo%2fghc-
> | 
> devs=01%7c01%7csimonpj%40064d.mgd.microsoft.com%7ce98f7b01dbeb47cc8d3908
> | 
> d38420b38b%7c72f988bf86f141af91ab2d7cd011db47%7c1=gFnWAB1of%2fp%2b0IXkD
> | CgcBbyxHkS7%2b4BusMl%2fs0rUySM%3d
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

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

[David Feuer]

#1965 *as modified by comments #7 and #9* is pretty much what I'm hoping for.

On Wed, May 25, 2016 at 3:27 AM, Simon Peyton Jones
<simo...@microsoft.com> wrote:
> I'm not following the details of this discussion.  Would it be possible to 
> write a compact summary, with the key examples, in the appropriate ticket?
>
> I think that https://ghc.haskell.org/trac/ghc/ticket/10016 is one such 
> ticket, but I think there may be more than one issue at stake here.  For 
> example, #10016 can be done in a strongly typed way in Core; but #1965 cannot 
> (so far as I know).
>
> It could also help to have a wiki page to summarise the cluster of issues, 
> pointing to the appropriate tickets for individual cases.
>
> An articulate summary will make it much more likely that progress is made! 
> Thanks.
>
> Simon
>
> | -Original Message-
> | From: ghc-devs [mailto:ghc-devs-boun...@haskell.org] On Behalf Of David 
> Feuer
> | Sent: 24 May 2016 23:14
> | To: Carter Schonwald <carter.schonw...@gmail.com>
> | Cc: ghc-devs <ghc-devs@haskell.org>
> | Subject: 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
> | <carter.schonw...@gmail.com> 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 <david.fe...@gmail.com> 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 <david.fe...@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
> | ___
> | ghc-devs mailing list
> | ghc-devs@haskell.org
> | 
> https://na01.safelinks.protection.outlook.com/?url=http%3a%2f%2fmail.haskell.
> | org%2fcgi-bin%2fmailman%2flistinfo%2fghc-
> | 
> devs=01%7c01%7csimonpj%40064d.mgd.microsoft.com%7ce98f7b01dbeb47cc8d3908
> | 
> d38420b38b%7c72f988bf86f141af91ab2d7cd011db47%7c1=gFnWAB1of%2fp%2b0IXkD
> | CgcBbyxHkS7%2b4BusMl%2fs0rUySM%3d
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

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

[David Feuer]

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
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

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

[David Feuer]

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
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

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

[David Feuer]

No, because the pattern matching semantics are different. Matching on
the constructor *must* force the contents to maintain type safety.
It's really strict data with the newtype optimization, rather than a
bona fide newtype.

On Tue, May 24, 2016 at 4:18 PM, Ben Gamari  wrote:
> David Feuer  writes:
>
>> Not really. It's really just the newtype optimization, although it's not a
>> newtype.
>
> Ahh, I see. Yes, you are right. I was being silly.
>
> However, in this case wouldn't it make more sense to just call it a newtype?
>
> Cheers,
>
> - Ben
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

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

[David Feuer]

Not really. It's really just the newtype optimization, although it's not a
newtype.
On May 24, 2016 12:43 PM, "Ben Gamari"  wrote:

> 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
>
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

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

[Ben Gamari]

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


signature.asc
Description: PGP signature
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: 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  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"  > wrote:
>
>> David Feuer > > 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
>>
>
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

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

> David Feuer  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
>
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

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

[Ben Gamari]

Ben Gamari  writes:

snip

> 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.
>
To clarify, as pointed out in #10016 it should also be possible to
unpack in the constrained case. You merely need to retain a spot in the
datacon's representation to place the dictionary.

I hope this helps.

Cheers,

- Ben


signature.asc
Description: PGP signature
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

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

[Ben Gamari]

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


signature.asc
Description: PGP signature
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs