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

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

I understand the problem, but I was actually talking about something else. We already have some other restrictions for polymorphism over boxed and unboxed types. For example: data T a b = T a b This has kind * -> * -> *. Similarly, kinds of 'a' and 'b' in this function are *: f :: (a, b) -> a f (x, _) = x I'm not trying to make this function polymorphic over both hash and start types. I'm just trying to make something like this possible: f :: (Int#, b) -> b f (_, b) = b Here the polymorphic part is boxed, * type. This should not be that hard, I think. Unless on-demand code generation part as mentioned by Dan is too much work. In any case, this is not that big deal. When I read the code I thought this should be a trivial change but apparently it's not. 2015-12-15 23:44 GMT-05:00 Richard Eisenberg :

Yes. I completely agree with Dan.

I wasn't suggesting that boxed tuples would be able to work with unboxed arguments. I was just suggesting that it should be possible to declare a levity-polymorphic type synonym for unboxed tuples, if that's what you need.

Richard

On Dec 15, 2015, at 10:04 PM, Dan Doel wrote:

...

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

---

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

I have another related question: What about allowing primitive types in newtypes? λ:4> newtype Blah1 = Blah1 Int λ:5> newtype Blah2 = Blah2 Int# <interactive>:5:23: error: • Expecting a lifted type, but ‘Int#’ is unlifted • In the type ‘Int#’ In the definition of data constructor ‘Blah2’ In the newtype declaration for ‘Blah2’ Ideally second definition should be OK, and kind of Blah2 should be #. Is this too hard to do? 2015-12-16 17:22 GMT-05:00 Richard Eisenberg :

On Dec 16, 2015, at 2:06 PM, Ömer Sinan Ağacan wrote:

...

In any case, this is not that big deal. When I read the code I thought this should be a trivial change but apparently it's not.

No, it's not. Your example (`f :: (Int#, b) -> b`) still has an unboxed thing in a boxed tuple. Boxed tuples simply can't (currently) hold unboxed things. And changing that is far from trivial. It's not the polymorphism that's the problem -- it's the unboxed thing in a boxed tuple.

Richard

newtype T = MkT Int# Provided T :: # (i.e. unlifted), I don’t think this would be too hard. That is, you can give a new name (via newtype) to an unlifted type like Int#, Float#, Double# etc. Worth a wiki page and a ticket. Simon From: ghc-devs [mailto:ghc-devs-bounces@haskell.org] On Behalf Of Edward Kmett Sent: 21 December 2015 09:10 To: Ömer Sinan Ağacan Cc: ghc-devs Subject: Re: Kinds of type synonym arguments I brought up the subject of allowing newtypes in kind # (or even in any kind that ends in * or # after a chain of ->'s to get more powerful Coercible instances) at ICFP this year and Simon seemed to think it'd be a pretty straightforward modification to the typechecker. I confess, he's likely waiting for me to actually sit down and give the idea a nice writeup. ;) This would be good for many things, especially when it comes to improving the type safety of various custom c-- tricks. -Edward On Sun, Dec 20, 2015 at 2:14 PM, Ömer Sinan Ağacan mailto:omeragacan@gmail.com> wrote: I have another related question: What about allowing primitive types in newtypes? λ:4> newtype Blah1 = Blah1 Int λ:5> newtype Blah2 = Blah2 Int# <interactive>:5:23: error: • Expecting a lifted type, but ‘Int#’ is unlifted • In the type ‘Int#’ In the definition of data constructor ‘Blah2’ In the newtype declaration for ‘Blah2’ Ideally second definition should be OK, and kind of Blah2 should be #. Is this too hard to do? 2015-12-16 17:22 GMT-05:00 Richard Eisenberg mailto:eir@cis.upenn.edu>:

On Dec 16, 2015, at 2:06 PM, Ömer Sinan Ağacan mailto:omeragacan@gmail.com> wrote:

...

In any case, this is not that big deal. When I read the code I thought this should be a trivial change but apparently it's not.

No, it's not. Your example (`f :: (Int#, b) -> b`) still has an unboxed thing in a boxed tuple. Boxed tuples simply can't (currently) hold unboxed things. And changing that is far from trivial. It's not the polymorphism that's the problem -- it's the unboxed thing in a boxed tuple.

Richard

_______________________________________________ ghc-devs mailing list ghc-devs@haskell.orgmailto:ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devshttps://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%7c4ba7cbf98af84227d01808d309e6931f%7c72f988bf86f141af91ab2d7cd011db47%7c1&sdata=nmxCKI9q3o%2b1pw%2f8phLXRWHv3QZ1xUpyAbN5CmyUwxQ%3d