wiki:Commentary/Compiler/Kinds

Version 1 (modified by simonpj, 23 months ago) (diff)

--

Kinds

Kinds are represented as types:

type Kind = Type

Basic kinds are now 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

https://docs.google.com/drawings/pub

(You can edit this picture here.)

* 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 #.

(#) is the kind of unboxed tuples. Things like (# Int, Int #) have kind (#).

ArgKind is the kind of things that can appear as arguments to functions.

OpenKind is the kind of things that can appear as results of functions.