Polymorphism over unboxed tuples

[Simon Peyton Jones]

All true.  But perhaps the paper should articulate this thinking?

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