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:



Kinds classify types. So for example:

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

The base kinds are these:

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

Last modified 14 months ago Last modified on Sep 1, 2018 9:20:35 AM