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 likeInt
andMaybe Float
have kind*
. - "
#
" is the kind of unlifted values. Things likeInt#
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.)