Polymorphic kinds
Sebastien Carlier
sebc@macs.hw.ac.uk
Mon, 4 Aug 2003 16:08:52 +0100
Hello,
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).
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.
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.
The following example illustrates the problem:
> {-# OPTIONS -fglasgow-exts #-}
>
> import GHC.Prim
>
> x :: IO Int#
> x =
> return 1#
GHC (HEAD from 2003-08-01) reports:
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'
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#'
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 #).
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?)
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.
> {-# OPTIONS -fglasgow-exts #-}
>
> import GHC.Prim
>
> newtype IO# (a :: # ) = IO# (State# RealWorld -> (# State# RealWorld, a #))
>
> x :: IO# Int#
> x = IO# (\ s -> (# s, 1# #))
GHC reports:
T.lhs:8:
Illegal unlifted type argument: Int#
In the type: IO# Int#
While checking the type signature for `x'
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).
Not being able to use do-notation is slightly inconvenient; is there a
reason why newtypes cannot be applied to unlifted type arguments?
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.
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.
--
Sebastien