Re: Kinds of type synonym arguments

[Edward Kmett]

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 
wrote:

> I have another related question: What about allowing primitive types
> in newtypes?
>
> λ:4> newtype Blah1 = Blah1 Int
> λ:5> newtype Blah2 = Blah2 Int#
>
> :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
> ___
> 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

Re: Kinds of type synonym arguments

[Reid Barton]

On Mon, Dec 21, 2015 at 5:13 AM, Simon Peyton Jones 
wrote:

> 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.
>

There is already a ticket at least,
https://ghc.haskell.org/trac/ghc/ticket/1311.

Regards,
Reid Barton
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: Kinds of type synonym arguments

[Ömer Sinan Ağacan]

I have another related question: What about allowing primitive types
in newtypes?

λ:4> newtype Blah1 = Blah1 Int
λ:5> newtype Blah2 = Blah2 Int#

: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
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: Kinds of type synonym arguments

[Ömer Sinan Ağacan]

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 <e...@cis.upenn.edu>:
> 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 <dan.d...@gmail.com> 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 <omeraga...@gmail.com> 
>> wrote:
>>> Oh sorry, I just mean that currently boxed tuples don't accept unboxed 
>>> types:
>>>
>>>λ> :k ( Int#, Int )
>>>
>>>: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 <simo...@microsoft.com>:
>>>> 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-boun...@haskell.org] On Behalf Of Ömer 
>>>> Sinan
>>>> | Agacan
>>>> | Sent: 15 December 2015 23:06
>>>> | To: Richard Eisenberg <e...@cis.upenn.edu>
>>>> | Cc: ghc-devs <ghc-devs@haskell.org>
>>>> | 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 ther

Re: Kinds of type synonym arguments

[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
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: Kinds of type synonym arguments

[Ömer Sinan Ağacan]

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# )

: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
>> 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

RE: Kinds of type synonym arguments

[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-boun...@haskell.org] On Behalf Of Ömer Sinan
| Agacan
| Sent: 15 December 2015 23:06
| To: Richard Eisenberg <e...@cis.upenn.edu>
| Cc: ghc-devs <ghc-devs@haskell.org>
| 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# )
| 
| :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 <e...@cis.upenn.edu>:
| > 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 <omeraga...@gmail.com> 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=01%7c01%7csimonpj%40064d.mgd.microsoft.com%7ce7184dc9345c4f9123c308
| d305a4631f%7c72f988bf86f141af91ab2d7cd011db47%7c1=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=01%7c01%7csimonpj%40064d.mgd.microsoft.com%7ce7184dc9345c4f9123c
| 308d305a4631f%7c72f988bf86f141af91ab2d7cd011db47%7c1=A4khlPGkSRO%2f4S%2
| bv%2fUxEiJj9DewPXVbsuX7GAzHB0FQ%3d
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: Kinds of type synonym arguments

[Ömer Sinan Ağacan]

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

λ> :k ( Int#, Int )

: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 <simo...@microsoft.com>:
> 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-boun...@haskell.org] On Behalf Of Ömer Sinan
> | Agacan
> | Sent: 15 December 2015 23:06
> | To: Richard Eisenberg <e...@cis.upenn.edu>
> | Cc: ghc-devs <ghc-devs@haskell.org>
> | 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# )
> |
> | :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 <e...@cis.upenn.edu>:
> | > 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 <omeraga...@gmail.com> 
> 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?
> | >> ___
> | &g

Re: Kinds of type synonym arguments

[Dan Doel]

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 <omeraga...@gmail.com> wrote:
> Oh sorry, I just mean that currently boxed tuples don't accept unboxed types:
>
> λ> :k ( Int#, Int )
>
> :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 <simo...@microsoft.com>:
>> 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-boun...@haskell.org] On Behalf Of Ömer 
>> Sinan
>> | Agacan
>> | Sent: 15 December 2015 23:06
>> | To: Richard Eisenberg <e...@cis.upenn.edu>
>> | Cc: ghc-devs <ghc-devs@haskell.org>
>> | 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# )
>> |
>> | :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 <e...@cis.upenn.edu>:
>> | > 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 

Re: Kinds of type synonym arguments

[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 <dan.d...@gmail.com> 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 <omeraga...@gmail.com> 
> wrote:
>> Oh sorry, I just mean that currently boxed tuples don't accept unboxed types:
>> 
>>λ> :k ( Int#, Int )
>> 
>>: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 <simo...@microsoft.com>:
>>> 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-boun...@haskell.org] On Behalf Of Ömer 
>>> Sinan
>>> | Agacan
>>> | Sent: 15 December 2015 23:06
>>> | To: Richard Eisenberg <e...@cis.upenn.edu>
>>> | Cc: ghc-devs <ghc-devs@haskell.org>
>>> | 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# )
>>> |
>>> | :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 

Re: Kinds of type synonym arguments

[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
> 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