[Haskell] Boxing (Day) Question

[Simon Peyton-Jones]

Ashley

I think Lennart answered your question rather well.  As he says, the
restriction is that an unboxed type must not instantiate a polymorphic
type variable (and that polymorphic type variables may not have an
unboxed kind).   You may like to read the paper "Unboxed types as
first-class citizens", which explains some of it, I think.
http://research.microsoft.com/%7Esimonpj/Papers/unboxed-values.ps.Z

The .NET CLR lifts the restriction by specialising code, so that it can
adapt to whether it is moving Int# or Double# values around.  In
Haskell, though, it's not possible to statically generate all the
instances you need, so you'd need run-time code generation to do this.  

It's a real restriction, and sometimes very tiresome, but I'm not
planning to fix it soon, unless I have a brilliant idea for how to do it
easily.

Simon 

| -----Original Message-----
| From: haskell-bounces at haskell.org [mailto:haskell-bounces at haskell.org]
On Behalf Of Ashley Yakeley
| Sent: 26 December 2005 08:49
| To: haskell at haskell.org
| Subject: [Haskell] Boxing (Day) Question
| 
| 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?
| 
| --
| Ashley Yakeley, Seattle WA
| 
| _______________________________________________
| Haskell mailing list
| Haskell at haskell.org
| http://www.haskell.org/mailman/listinfo/haskell