Kinds of type synonym arguments
Ömer Sinan Ağacan
omeragacan at gmail.com
Wed Dec 16 19:06:25 UTC 2015
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 <eir at 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.doel at 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 <omeragacan at gmail.com> 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 <simonpj at 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-bounces at haskell.org] On Behalf Of Ömer Sinan
>>>> | Agacan
>>>> | Sent: 15 December 2015 23:06
>>>> | To: Richard Eisenberg <eir at cis.upenn.edu>
>>>> | Cc: ghc-devs <ghc-devs at 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# )
>>>> |
>>>> | <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 <eir at 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 <omeragacan at 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 at 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 at 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 at haskell.org
>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>> _______________________________________________
>> ghc-devs mailing list
>> ghc-devs at haskell.org
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>>
>
More information about the ghc-devs
mailing list