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