Version 3 (modified by simonpj, 23 months ago) (diff) |
---|

# Kinds

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 "`#`".)

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

- "
`OpenKind`" is the kind of things that can appear as argument or result of functions.