Kinds of type synonym arguments

Dan Doel dan.doel at gmail.com
Wed Dec 16 03:04:41 UTC 2015


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


More information about the ghc-devs mailing list