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

David Feuer

19 May 2016 19 May '16

10:30 a.m.

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

Attachments:

attachment.html (text/html — 891 bytes)

Show replies by date

Ben Gamari

24 May 24 May

4:16 a.m.

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

Ben Gamari

4:22 a.m.

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

David Feuer

10:02 a.m.

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

Carter Schonwald

12:33 p.m.

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

Ben Gamari

12:43 p.m.

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

David Feuer

1:46 p.m.

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

Ben Gamari

4:18 p.m.

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

David Feuer

4:20 p.m.

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

David Feuer

5:39 p.m.

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.

Carter Schonwald

6:03 p.m.

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 javascript:_e(%7B%7D,'cvml','david.feuer@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

David Feuer

6:13 p.m.

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

Simon Peyton Jones

25 May 25 May

3:27 a.m.

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-bounces@haskell.org] On Behalf Of David Feuer | Sent: 24 May 2016 23:14 | To: Carter Schonwald | Cc: ghc-devs | 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 | 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 | https://na01.safelinks.protection.outlook.com/?url=http%3a%2f%2fmail.haskell. | org%2fcgi-bin%2fmailman%2flistinfo%2fghc- | devs&data=01%7c01%7csimonpj%40064d.mgd.microsoft.com%7ce98f7b01dbeb47cc8d3908 | d38420b38b%7c72f988bf86f141af91ab2d7cd011db47%7c1&sdata=gFnWAB1of%2fp%2b0IXkD | CgcBbyxHkS7%2b4BusMl%2fs0rUySM%3d

David Feuer

3:39 a.m.

#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 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-bounces@haskell.org] On Behalf Of David Feuer | Sent: 24 May 2016 23:14 | To: Carter Schonwald | Cc: ghc-devs | 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 | 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 | https://na01.safelinks.protection.outlook.com/?url=http%3a%2f%2fmail.haskell. | org%2fcgi-bin%2fmailman%2flistinfo%2fghc- | devs&data=01%7c01%7csimonpj%40064d.mgd.microsoft.com%7ce98f7b01dbeb47cc8d3908 | d38420b38b%7c72f988bf86f141af91ab2d7cd011db47%7c1&sdata=gFnWAB1of%2fp%2b0IXkD | CgcBbyxHkS7%2b4BusMl%2fs0rUySM%3d

Simon Peyton Jones

4:22 a.m.

OK, so nothing new in the email thread? Is it worth adding any of the examples to the ticket? | -----Original Message----- | From: David Feuer [mailto:david.feuer@gmail.com] | Sent: 25 May 2016 08:40 | To: Simon Peyton Jones | Cc: Carter Schonwald ; ghc-devs | Subject: Re: Unpacking single-field, single-strict-constructor GADTs | and existentials | | #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 | 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-bounces@haskell.org] On Behalf Of | > | David Feuer | > | Sent: 24 May 2016 23:14 | > | To: Carter Schonwald | > | Cc: ghc-devs | > | 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 | > | 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 | > | | https://na01.safelinks.protection.outlook.com/?url=http%3a%2f%2fmail.h | askell. | > | org%2fcgi-bin%2fmailman%2flistinfo%2fghc- | > | | devs&data=01%7c01%7csimonpj%40064d.mgd.microsoft.com%7ce98f7b01dbeb4 | > | 7cc8d3908 | > | | d38420b38b%7c72f988bf86f141af91ab2d7cd011db47%7c1&sdata=gFnWAB1of%2f | > | p%2b0IXkD | > | CgcBbyxHkS7%2b4BusMl%2fs0rUySM%3d

David Feuer

4 a.m.

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 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-bounces@haskell.org] On Behalf Of David Feuer | Sent: 24 May 2016 23:14 | To: Carter Schonwald | Cc: ghc-devs | 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 | 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 | https://na01.safelinks.protection.outlook.com/?url=http%3a%2f%2fmail.haskell. | org%2fcgi-bin%2fmailman%2flistinfo%2fghc- | devs&data=01%7c01%7csimonpj%40064d.mgd.microsoft.com%7ce98f7b01dbeb47cc8d3908 | d38420b38b%7c72f988bf86f141af91ab2d7cd011db47%7c1&sdata=gFnWAB1of%2fp%2b0IXkD | CgcBbyxHkS7%2b4BusMl%2fs0rUySM%3d

Simon Peyton Jones

4:47 a.m.

Oh, that's helpful thank you. I have added comments! SImon | -----Original Message----- | From: David Feuer [mailto:david.feuer@gmail.com] | Sent: 25 May 2016 09:01 | To: Simon Peyton Jones | Cc: Carter Schonwald ; ghc-devs | Subject: Re: Unpacking single-field, single-strict-constructor GADTs | and existentials | | 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 | 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-bounces@haskell.org] On Behalf Of | > | David Feuer | > | Sent: 24 May 2016 23:14 | > | To: Carter Schonwald | > | Cc: ghc-devs | > | 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 | > | 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 | > | | https://na01.safelinks.protection.outlook.com/?url=http%3a%2f%2fmail.h | askell. | > | org%2fcgi-bin%2fmailman%2flistinfo%2fghc- | > | | devs&data=01%7c01%7csimonpj%40064d.mgd.microsoft.com%7ce98f7b01dbeb4 | > | 7cc8d3908 | > | | d38420b38b%7c72f988bf86f141af91ab2d7cd011db47%7c1&sdata=gFnWAB1of%2f | > | p%2b0IXkD | > | CgcBbyxHkS7%2b4BusMl%2fs0rUySM%3d

AntC

28 May 28 May

8:19 p.m.

...

Simon Peyton Jones 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

3278

Age (days ago)

3288

Last active (days ago)

List overview

Download

17 comments

5 participants

participants (5)

AntC
Ben Gamari
Carter Schonwald
David Feuer
Simon Peyton Jones

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

tags

participants (5)