Kinds of Types

Types are to values as kinds are to type constructors. Unison attributes a kind to every type constructor, which is determined by its number of type parameters and the kinds of those type parameters.

A type must be well kinded, just like an expression must be well typed, and for the same reason. However, there is currently no syntax for kinds and they do not appear in Unison programs (this will certainly change in a future version of Unison).

Unison’s kinds have the following forms:

• A nullary type constructor or ordinary type has kind Type.
• A type constructor has kind k1 -> k2 where k1 and k2 are kinds.

For example List, a unary type constructor, has kind Type -> Type as it takes a type and yields a type. A binary type constructor like -> has kind Type -> Type -> Type, as it takes two types (it actually takes a type and yields a partially applied unary type constructor that takes the other type). A type constructor of kind (Type -> Type) -> Type is a higher-order type constructor (it takes a unary type constructor and yields a type).