Kinds of type synonym arguments

Richard Eisenberg eir at cis.upenn.edu
Wed Dec 16 04:44:35 UTC 2015 

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