Re: [Haskell] Boxing (Day) Question

[Lennart Augustsson]

On the whole it looks like you want type variables with kind #.
There are very good implementation reasons for not allowing this.
If you had type variables of kind # you could have polymorphic
functions over unboxed values.  But since the values are unboxed
they don't have a uniform representation (e.g., a Double# is probably
twice the size of a Float#).  So polymorphic functions over unboxed
values are not easy to implement.  (You can imagine implementations
of them, but none of them are pleasent.)

        -- Lennart

Ashley Yakeley wrote:

As I understand it, with unboxing switched on (->) actually has this kind:

  (->) :: ? -> ? -> *

Reading the Core specification, GHC has a particular kind of "polykindism" which introduces kind "?", and defines specialisation such that "?" may be replaced by "*" or "#" inside any kind. Accordingly, (->) may be specialised:

  (->) :: * -> * -> *
  (->) :: # -> * -> *
  (->) :: * -> # -> *
  (->) :: # -> # -> *

Examples:

  module Boxing where
  import GHC.Exts

  fooSS :: (->) Int Int
  fooSS 3 = 5
  fooSS _ = 2

  fooHS :: (->) Int# Int
  fooHS 3# = 5
  fooHS _ = 2

  fooSH :: (->) Int Int#
  fooSH 3 = 5#
  fooSH _ = 2#

  fooHH :: (->) Int# Int#
  fooHH 3# = 5#
  fooHH _ = 2#

  type Fun = (->)

  fooHH' :: Fun Int# Int#
  fooHH' 3# = 5#
  fooHH' _ = 2#

Do any other type constructors or symbols have a kind with "?" in it?

I like the "kind" approach to unboxed types. It automatically rules out "[Int#]" by kind mismatch, for instance. But I was disappointed I couldn't do this with GHC 6.4.1:

  data MyC s = MkMyC (s Int# Int)

or

  class C s where
      c :: s Int# Int

(in either case: "Kind error: Expecting kind `k_a19o', but `Int#' has kind `#' In the class declaration for `C'")

There's no kind mismatch here, merely a restriction that the kinds of arguments to classes be #-free. I can't do this, either:

  newtype MyD (u :: #) = MkMyD (u -> Bool)

GHC actually complains about parsing the kind signature.

Would Bad Things Happen if this restriction were lifted? I don't have a pressing need for it actually, though this might be useful:

  class Boxed (b :: *) (u :: #) | b -> u, u -> b where
      box :: u -> b
      unbox :: b -> u

In case you're worried, lifting the restriction would NOT allow uncompilable things such as

  newtype MyE (u :: #) = MkMyE u

...simply because there's already a straightforward restriction that values in type constructors have types of kind "*". It is merely the notion of "#-freeness" that seems unnecessary. It would, however, allow this:

  newtype Box (u :: #) = MkBox (() -> u)

...and quite possibly this:

newtype Value (x :: ?) = MkValue (() -> x)

I believe these can be compiled safely?

_______________________________________________
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell