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?