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