Polymorphism over unboxed tuples

[Richard Eisenberg]

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/levity-1.pdf
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs