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 [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs |
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 <[hidden email]> 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 > [hidden email] > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs _______________________________________________ ghc-devs mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs |
All true. But perhaps the paper should articulate this thinking?
Simon | -----Original Message----- | From: ghc-devs [mailto:[hidden email]] On Behalf Of | Richard Eisenberg | Sent: 23 March 2017 16:19 | To: Ryan Scott <[hidden email]> | Cc: GHC developers <[hidden email]> | 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 <[hidden email]> | 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 | > [hidden email] | > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs | | _______________________________________________ | ghc-devs mailing list | [hidden email] | http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs _______________________________________________ ghc-devs mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs |
> On Mar 24, 2017, at 9:14 AM, Simon Peyton Jones <[hidden email]> 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:[hidden email]] On Behalf Of > | Richard Eisenberg > | Sent: 23 March 2017 16:19 > | To: Ryan Scott <[hidden email]> > | Cc: GHC developers <[hidden email]> > | 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 <[hidden email]> > | 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 > | > [hidden email] > | > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs > | > | _______________________________________________ > | ghc-devs mailing list > | [hidden email] > | http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs _______________________________________________ ghc-devs mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs |
Free forum by Nabble | Edit this page |