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

> 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

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

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 sing

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

nal 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

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

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

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,

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

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:

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

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

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

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

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

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

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

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

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

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

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

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

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

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