Polymorphic kinds

[Simon Peyton-Jones]

The real question is:
	why does GHC distinguish kind * from kind #?

For example,  Int   has kind *
		Int# has kind #

The main reason is this: a polymorphic function assumes that values of
type 'a' are represented by a pointer.  For example:
	const :: a -> b -> a
const assumes that its arguments are represented by pointers.  The
machine instructions simply would not work if it was passed (say) two
double-precision floats, of type Double#.

To avoid this bad thing happening, GHC imposes the following rule
(described in detail in "Unboxed values as first class citizens"
http://research.microsoft.com/~simonpj/Papers/unboxed-values.ps.Z)

	A polymorphic type variable (such as 'a' and 'b' in the type of
const) can
	only be instantiated by a boxed type (of kind *)

Value whose type is of kind * are always represented by a pointer.
Value whose type is of kind # are represented in a type-dependent way.


In your particular case, consider '>>=3D'.  It is required to transport
the value returned by its left argument to the function that is its
right argument.  The machine instructions reqd to do that differ if the
value so transported is an Int#.

[One of the big advantages of .NET is that its generic type system
*does* allow polymorphic type variables to be instantiated with unboxed
types, using run-time code generation to "fluff up" copies of the
function code instantiated with the representation type.]


[An Int# is the same size as a pointer, yes, but its GC behaviour is
different.]


Now, do-notation expands to the overloaded '>>=3D' stuff, so you are
stuck.

It would be possible, I guess, to change the way in which do-notation
expanded, so that in the special case of the IO monad unboxed LHSs were
allowed.  That might allow you to use do-notation, but it seems a bit ad
hoc.

Simon
	  =20
| -----Original Message-----
| From: glasgow-haskell-users-admin@haskell.org
[mailto:glasgow-haskell-users-admin@haskell.org]
| On Behalf Of Sebastien Carlier
| Sent: 04 August 2003 16:09
| To: glasgow-haskell-users@haskell.org
| Subject: Polymorphic kinds
|=20
|=20
| Hello,
|=20
| I am experimenting with GHC to write low level code (e.g., device
| drivers, interrupt handlers).  The ultimate goal is to write a
| prototype operating system in Haskell, using the GHC RTS as a kind of
| microkernel (this appears to be relatively easy by removing all the
| dependencies on an operating system, and providing a block allocator
| and interval timers).
|=20
| I have added the necessary primitive operations to generate privileged
| instructions for IA32 to GHC, and it seems to work fine, good quality
| assembly code is generated.
|=20
| Now, I would like to make use of do-notation to write cleaner code
| (threading a State# RealWorld through computations is quite ugly).
| I want to avoid allocating memory in parts of the code, so I would
| like to be able to have monadic computations which return unboxed
| values.  Sadly, GHC currently does not appear to allow that.
|=20
| The following example illustrates the problem:
|=20
| > {-# OPTIONS -fglasgow-exts #-}
| >
| > import GHC.Prim
| >
| > x :: IO Int#
| > x =3D
| >     return 1#
|=20
| GHC (HEAD from 2003-08-01) reports:
|=20
| T.lhs:5:
|     Kind error: Expecting a lifted type, but `Int#' is unlifted
|     When checking kinds in `IO Int#'
|     In the type: IO Int#
|     While checking the type signature for `x'
|=20
| T.lhs:7:
|     Couldn't match `*' against `#'
|     When matching types `a' and `Int#'
|         Expected type: a
|         Inferred type: Int#
|     In the first argument of `return', namely `1#'
|=20
| After looking into the problem for a while, I realized that GHC does
| not have polymorphic kinds - after checking a bunch of definitions, it
| "zonks" all kind variables to (Type *) and all boxity variables to *.
| So IO has kind (Type * -> Type *), and cannot be applied to an unboxed
| value of kind (Type #).
|=20
| GHC has had explicit kind annotations for a while:
| <http://www.haskell.org/pipermail/haskell/2002-February/008906.html>
| So I ought to be able define an IO# type for computations that return
| unboxed values.
| (By the way, is there already an unboxed unit value and type?)
|=20
| Strangely, GHC did not recognizes # as the kind of unlifted types, so
| I added that to the compiler, and hoped that things would work out.
| Well, almost.
|=20
| > {-# OPTIONS -fglasgow-exts #-}
| >
| > import GHC.Prim
| >
| > newtype IO# (a :: # ) =3D IO# (State# RealWorld -> (# State#
RealWorld, a #))
| >
| > x :: IO# Int#
| > x =3D IO# (\ s -> (# s, 1# #))
|=20
| GHC reports:
|=20
| T.lhs:8:
|     Illegal unlifted type argument: Int#
|     In the type: IO# Int#
|     While checking the type signature for `x'
|=20
| The example is accepted if "newtype" is replaced by "type" (and by
| removing uses of the IO# value constructor), so I can proceed with my
| experiment by not using do-notation (defining return#, then#, etc
| appears to work fine).
|=20
| Not being able to use do-notation is slightly inconvenient; is there a
| reason why newtypes cannot be applied to unlifted type arguments?
|=20
| I expect that I would eventually have been beaten anyway when trying
| to make an instance of the Monad type class for the above IO# newtype,
| since Monad is probably regarded as a predicate of kind (* -> *) -> P
| (where P would be the hypothetical kind of propositions); application
| to an operator of kind (# -> *) would fail.
|=20
| What would need to be done to extend the compiler so that it allows IO
| computations to be able to return unboxed values?  For some reason I
| am worried that "just" having polymorphic kind may not be enough.
| I also fail to understand all the implications of having polymorphic
| kinds, so I would greatly appreciate if one of the GHC experts could
| say something about that too.
|=20
| --
| Sebastien
| _______________________________________________
| Glasgow-haskell-users mailing list
| Glasgow-haskell-users@haskell.org
| http://www.haskell.org/mailman/listinfo/glasgow-haskell-users