GHC and Kinds

Simon Peyton-Jones simonpj at microsoft.com
Thu Oct 30 13:59:34 EST 2003


| type Kind = Type
| 
| What does this mean?

It means that Kinds are represented by Types.

Admittedly, Kinds only use a small fragment of what Types can represent,
namely Arrow, and type constructor applications.  So * is represented by
a TyConApp with a TyCon that is called typeCon.

The really annoying thing about Kinds is that there's occasionally a bit
of sub-kinding.  In particular

	error :: forall a. String -> a

We want to allow 
	error "foo" :: Int#

so the kind of 'a' can't be *, nor # (the kind of unboxed types).  It's
an "open" kind, written "?"; both * and # are sub-kinds of ?.


You should nevertheless be able to encode your kind system in the same
way as GHC does.

But I have been thinking that it's over-kill to use Types for Kinds, and
leads to no real saving.
I may well split the two types in the future.

Simon





More information about the Glasgow-haskell-users mailing list