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

2016-05-28 Thread 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 f

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

2016-05-25 Thread Simon Peyton Jones
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 | > | Cc: ghc-devs | > | Subject: Re: Unpacking single

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

2016-05-25 Thread Simon Peyton Jones
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.

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

2016-05-25 Thread David Feuer
- > | From: ghc-devs [mailto:ghc-devs-boun...@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,

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

2016-05-25 Thread David Feuer
hc-devs [mailto:ghc-devs-boun...@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

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

2016-05-25 Thread Simon Peyton Jones
gress 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 | Cc: ghc-devs | Subject: Re: Unpacking single-field, single-strict-constructor GADTs and | existen

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

2016-05-24 Thread 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 w

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

2016-05-24 Thread Carter Schonwald
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 re

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

2016-05-24 Thread 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

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

2016-05-24 Thread 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

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

2016-05-24 Thread Ben Gamari
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 signature.asc Description: PGP signature

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

2016-05-24 Thread 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

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

2016-05-24 Thread 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

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

2016-05-24 Thread 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 Tues

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

2016-05-24 Thread 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

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

2016-05-24 Thread 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,

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

2016-05-24 Thread 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) -