Re: Kinds of type synonym arguments

This is not a simple change at all, though. The reason that (,) cannot accept arguments of kind # is not just that there was no levity abstraction. You simply cannot abstract over # in the same way as you can *, because the types in # are not represented uniformly. Creating a tuple with an argument of kind # would require generating code for (at the least) each different size of thing that can go in #; but there are infinitely many of those, because of unboxed tuples, so you probably have to do on-demand code generation when particular types are used. And of course, the evaluation conventions change between # and *, so you have to deal with that if tuples are supposed to accept types of both kinds. See the stuff at: https://ghc.haskell.org/trac/ghc/wiki/UnliftedDataTypes for instance. Note that that that page is only considering being able to abstract over the portion of # that is represented uniformly by a pointer, though. Things like Int#, Double# and (# Int#, Double #) are completely out of its scope. This isn't just the typing on (,) being overly restrictive. It would be a pretty fundamental change that would, I assume, be non-trivial to implement. I think it would be non-trivial to come up with a good design, too, really. -- Dan On Tue, Dec 15, 2015 at 6:25 PM, Ömer Sinan Ağacan wrote:

Oh sorry, I just mean that currently boxed tuples don't accept unboxed types:

λ> :k ( Int#, Int )

<interactive>:1:3: error: • Expecting a lifted type, but ‘Int#’ is unlifted • In the type ‘(Int#, Int)’

But unboxed variant of exactly the same thing is accepted:

λ> :k (# Int#, Int #) (# Int#, Int #) :: #

I was hoping make these two the same by adding levity arguments and making type arguments depend on levity arguments, just like how unboxed tuple types are implemented (as described in Note [Unboxed tuple levity vars]).

The changes in tuple DataCon and TyCon generation is fairly simple (in fact I just implemented that part) but the rest of the compiler started panicking. So my question is, is there a reason for not doing this, because otherwise I'd like to fix panics etc. and make this change.

2015-12-15 18:08 GMT-05:00 Simon Peyton Jones :

...

What is "this" that you propose to implement? Is there a wiki page that describes the design?

Simon

| -----Original Message----- | From: ghc-devs [mailto:ghc-devs-bounces@haskell.org] On Behalf Of Ömer Sinan | Agacan | Sent: 15 December 2015 23:06 | To: Richard Eisenberg | Cc: ghc-devs | Subject: Re: Kinds of type synonym arguments | | Hi Richard, | | Now that we have levity arguments I'm wondering if we should go ahead and | implement this. The code is already there - unboxed tuples have levity | arguments and then type arguments depend on the levity arguments, so this | works: | | λ> :k (# Int, Int# #) | (# Int, Int# #) :: # | | But this doesn't because boxed tuples are not implemented that way: | | λ> :k ( Int, Int# ) | | <interactive>:1:8: error: | • Expecting a lifted type, but ‘Int#’ is unlifted | • In the type ‘(Int, Int#)’ | | The implementation looked fairly simple so I just tried to lift this | restriction (I basically merged the code that generates TyCons and DataCons | for | unboxed and boxed tuples in WiredInTys), but some other parts of the compiler | started to panic. Should I investigate this further or are there any problems | with this that we need to solve first? | | If there's a problem with this I think we should at least add a NOTE in | TysWiredIn. Note [Unboxed tuple levity vars] explains how levity vars are | used | in unboxed tuples, but there's no comments or notes about why we don't do the | same for boxed tuples. | | Also, I was wondering if OpenKind is deprecated now. Can I assume that levity | arguments do that work now and we no longer need OpenKind? | | Thanks | | 2015-12-06 21:45 GMT-05:00 Richard Eisenberg : | > I think this is a consequence of the rule that we never abstract over types | of kind #. But I believe this should work with my branch: | > | >> type Tuple (a :: TYPE v1) (b :: TYPE v2) = (# a, b #) | > | > The user would have to request that the synonym be used over both * and #, | but the synonym should work. The need to request the special treatment might | be lifted, but we'd have to think hard about where we want the generality by | default and where we want simpler behavior by default. | > | > Richard | > | > On Dec 6, 2015, at 1:55 PM, Ömer Sinan Ağacan wrote: | > | >> In this program: | >> | >> {-# LANGUAGE MagicHash, UnboxedTuples #-} | >> | >> module Main where | >> | >> import GHC.Prim | >> import GHC.Types | >> | >> type Tuple a b = (# a, b #) | >> | >> main = do | >> let -- x :: Tuple Int# Float# | >> x :: (# Int#, Float# #) | >> x = (# 1#, 0.0# #) | >> | >> return () | >> | >> If I use the first type declaration for 'x' I'm getting this error | message: | >> | >> Expecting a lifted type, but ‘Int#’ is unlifted | >> | >> Indeed, if I look at the kinds of arguments of 'Tuple': | >> | >> λ:7> :k Tuple | >> Tuple :: * -> * -> # | >> | >> It's star. I was wondering why is this not 'OpenKind'(or whatever the | >> super-kind of star and hash). Is there a problem with this? Is this a bug? | >> Or is this simply because type synonyms are implemented before OpenKinds? | >> _______________________________________________ | >> ghc-devs mailing list | >> ghc-devs@haskell.org | >> | https://na01.safelinks.protection.outlook.com/?url=http%3a%2f%2fmail.haskell. | org%2fcgi-bin%2fmailman%2flistinfo%2fghc- | devs&data=01%7c01%7csimonpj%40064d.mgd.microsoft.com%7ce7184dc9345c4f9123c308 | d305a4631f%7c72f988bf86f141af91ab2d7cd011db47%7c1&sdata=sYBDmz3zltvhkRvFsuo1h | OiBLqO6Qsu7N0zpzUK7iPY%3d | >> | > | _______________________________________________ | ghc-devs mailing list | ghc-devs@haskell.org | https://na01.safelinks.protection.outlook.com/?url=http%3a%2f%2fmail.haskell. | org%2fcgi-bin%2fmailman%2flistinfo%2fghc- | devs%0a&data=01%7c01%7csimonpj%40064d.mgd.microsoft.com%7ce7184dc9345c4f9123c | 308d305a4631f%7c72f988bf86f141af91ab2d7cd011db47%7c1&sdata=A4khlPGkSRO%2f4S%2 | bv%2fUxEiJj9DewPXVbsuX7GAzHB0FQ%3d

---

ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs