Version 5 (modified by 5 years 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.)