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

[Simon Peyton Jones]

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 at gmail.com]
|  Sent: 25 May 2016 08:40
|  To: Simon Peyton Jones <simonpj at microsoft.com>
|  Cc: Carter Schonwald <carter.schonwald at gmail.com>; ghc-devs <ghc-
|  devs at haskell.org>
|  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
|  <simonpj at 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-bounces at haskell.org] On Behalf Of
|  > | David Feuer
|  > | Sent: 24 May 2016 23:14
|  > | To: Carter Schonwald <carter.schonwald at gmail.com>
|  > | Cc: ghc-devs <ghc-devs at 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.schonwald at 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.feuer at 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.feuer at 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 at 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