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