|Version 5 (modified by simonpj, 13 months ago)|
Kinds classify types. So for example:
Int :: * Int -> Int :: * Maybe :: * -> * Int# :: # (# Int, Int #) :: #
The base kinds are these:
- "*" is the kind of boxed values. Things like Int and Maybe Float have kind *.
- "#" is the kind of unboxed values. Things like Int# have kind #.
- With the advent of data type promotion and kind polymorphism we can have a lot more kinds.
(Unboxed tuples used to have a distinct kind, but in 2012 we combined unboxed tuples with other unboxed values in a single kind "#".)
Kinds are represented by the data type Type (see Commentary/Compiler/TypeType):
type Kind = Type
Basic kinds are represented using type constructors, e.g. the kind * is represented as
liftedTypeKind :: Kind liftedTypeKind = TyConApp liftedTypeKindTyCon 
where liftedTypeKindTyCon is a built-in PrimTyCon. The arrow type constructor is used as the arrow kind constructor, e.g. the kind * -> * is represented internally as
FunTy liftedTypeKind liftedTypeKind
It's easy to extract the kind of a type, or the sort of a kind:
typeKind :: Type -> Kind
The "sort" of a kind is always one of the sorts: TY (for kinds that classify normal types) or CO (for kinds that classify coercion evidence). The coercion kind, T1 :=: T2, is represented by PredTy (EqPred T1 T2).
There is a small amount of sub-typing in kinds. Suppose you see (t1 -> t2). What kind must t1 and t2 have? It could be * or #. So we have a single kind OpenKind, which is a super-kind of both, with this simple lattice:
(You can edit this picture here.)