All true. But perhaps the paper should articulate this thinking?
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
