Re: Polymorphism over unboxed tuples

On Mar 24, 2017, at 9:14 AM, Simon Peyton Jones 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@haskell.org] On Behalf Of | Richard Eisenberg | Sent: 23 March 2017 16:19 | To: Ryan Scott | Cc: GHC developers | 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 | 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@haskell.org | > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs | | _______________________________________________ | ghc-devs mailing list | ghc-devs@haskell.org | http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs