Polymorphism over unboxed tuples

[Richard Eisenberg]

> On Mar 24, 2017, at 9:14 AM, Simon Peyton Jones <simonpj at microsoft.com> wrote:
> 
> All true.  But perhaps the paper should articulate this thinking?

I'm OK with adding an appendix with this reasoning. I think it would clutter the paper itself to put this all there.

Richard

> 
> Simon
> 
> |  -----Original Message-----
> |  From: ghc-devs [mailto:ghc-devs-bounces at haskell.org] On Behalf Of
> |  Richard Eisenberg
> |  Sent: 23 March 2017 16:19
> |  To: Ryan Scott <ryan.gl.scott at gmail.com>
> |  Cc: GHC developers <ghc-devs at haskell.org>
> |  Subject: Re: Polymorphism over unboxed tuples
> |  
> |  This was a design choice in implementing, and one that is open for
> |  revision (but not for 8.2).
> |  
> |  The key property is this:
> |   (*) Two types with different representations must have different
> |  kinds.
> |  
> |  Note that (*) does not stipulate what happens with two types with the
> |  same representation, such as (# Int, (# Bool #) #) and (# Double, Char
> |  #). We decided it was simpler to have unboxed tuples with the same
> |  representation but different nestings to have different kinds. Part of
> |  the complication with what’s proposed in the paper is that the kind of
> |  unboxed tuple type constructors become more complicated. For example,
> |  we would have
> |  
> |  (#,#) :: forall (r1 :: [UnaryRep]) (r2 :: [UnaryRep]). TYPE r1 -> TYPE
> |  r2 -> TYPE (TupleRep (Concat ‘[r1, r2]))
> |  
> |  where Concat is a type family that does type-level list concatenation.
> |  This would work. But would it have type inference consequences? (You
> |  would be unable to infer the constituent kinds from the result kind.)
> |  I doubt anyone would notice.
> |  
> |  The next problem comes when thinking about unboxed sums, though. To
> |  implement unboxed sums (unmentioned in the paper) along similar lines,
> |  you would need to include the quite-complicated algorithm for figuring
> |  out the concrete representation of a sum from its types. For example,
> |  (# (# Int, Int# #) | (# Word#, Int# #) #) takes up only 4 words in
> |  memory: 1 each for the tag, the pointer to the Int, the Word#, and the
> |  Int#. Note that the slot for the Int# is shared between the disjuncts!
> |  We can’t share other slots because the GC properties for an Int are
> |  different than for a Word#. But we also don’t take up 5 slots,
> |  repeating the Int#. The algorithm to figure this out is thus somewhat
> |  involved.
> |  
> |  If we wanted two unboxed sums with the same representations to have
> |  the same kind, we would need to implement this algorithm in type
> |  families. It’s doable, surely, but nothing I want to contemplate. And,
> |  worse, it would expose this algorithm to users, who might start to
> |  depend on it in their polymorphism. What if we decide to change it?
> |  Then the type families change and users’ code breaks. Ich.
> |  
> |  Of course, we could use precise kinds for tuples (Concat isn’t hard
> |  and isn’t likely to change) and imprecise kinds for sums. There’s
> |  nothing wrong with such a system. But until a user appears (maybe
> |  you!) asking for the precise kinds, it seems premature to commit
> |  ourselves to that mode.
> |  
> |  Richard
> |  
> |  > On Mar 23, 2017, at 11:15 AM, Ryan Scott <ryan.gl.scott at gmail.com>
> |  wrote:
> |  >
> |  > Section 4.2 of the paper Levity Polymorphism [1] makes a bold claim
> |  > about polymorphism for unboxed tuples:
> |  >
> |  >  Note that this format respects the computational irrelevance of
> |  > nesting of unboxed tuples. For example, these three types all have
> |  the
> |  > same kind, here written PFP for short:
> |  >
> |  >  type PFP = TYPE '[PtrRep, FloatRep, PtrRep]
> |  >  (# Int, (# Float#, Bool #) #)        :: PFP
> |  >  (# Int, Float#, Bool #)              :: PFP
> |  >  (# (# Int, (# #) #), Float#, Bool #) :: PFP
> |  >
> |  > But in GHC, that isn't the case! Here's proof of it from a recent
> |  GHCi session:
> |  >
> |  >  GHCi, version 8.3.20170322: http://www.haskell.org/ghc/  :? for
> |  help
> |  > λ> :set -XUnboxedTuples -XMagicHash  λ> import GHC.Exts  λ> :kind (#
> |  > Int, (# Float#, Bool #) #)  (# Int, (# Float#, Bool #) #) :: TYPE
> |  >                                     ('TupleRep '['LiftedRep,
> |  'TupleRep
> |  > '['FloatRep, 'LiftedRep]])  λ> :kind (# Int, Float#, Bool #)  (#
> |  Int,
> |  > Float#, Bool #) :: TYPE
> |  >                               ('TupleRep '['LiftedRep, 'FloatRep,
> |  > 'LiftedRep])
> |  >  λ> :kind (# (# Int, (# #) #), Float#, Bool #)  (# (# Int, (# #) #),
> |  > Float#, Bool #) :: TYPE
> |  >                                            ('TupleRep
> |  >                                               '['TupleRep
> |  > '['LiftedRep, 'TupleRep '[]], 'FloatRep,
> |  >                                                 'LiftedRep])
> |  >
> |  > As you can see, each of these different nestings of unboxed tuples
> |  > yields different kinds, so they most certainly do *not* uphold the
> |  > property claimed in the paper.
> |  >
> |  > Is this a bug? Or is there some reason that GHC implemented it
> |  differently?
> |  >
> |  > Ryan S.
> |  > -----
> |  > [1]
> |  > https://www.microsoft.com/en-us/research/wp-
> |  content/uploads/2016/11/le
> |  > vity-1.pdf _______________________________________________
> |  > ghc-devs mailing list
> |  > ghc-devs at haskell.org
> |  > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
> |  
> |  _______________________________________________
> |  ghc-devs mailing list
> |  ghc-devs at haskell.org
> |  http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs