[Haskell] Boxing (Day) Question
Lennart Augustsson
lennart at augustsson.net
Mon Dec 26 05:47:20 EST 2005
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?
>
More information about the Haskell
mailing list