kinds

TODO This page is somewhat old. It needs to be updated with recent information. The followings are the latest related information.

GHC User's Guide:

GHC Proposals:

Papers:

Kinds

Kinds classify types. So for example:

   Int :: *
   Int -> Int :: *
   Maybe :: * -> *
   Int# :: #
   (# Int, Int #) :: #

The base kinds are these:

"*" is the kind of lifted, boxed values. Things like Int and Maybe Float have kind *.
"#" is the kind of unlifted values. Things like Int# have kind #.
With the advent of data type promotion and kind polymorphism we can have a lot more kinds.
Kinds are in flux with levity polymorphism. See LevityPolymorphism. See also TypeType.

(Unboxed tuples used to have a distinct kind, but in 2012 we combined unboxed tuples with other unboxed values in a single kind "#".)

Representing kinds

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).

Kind subtyping

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.)