Types are to values askindsare 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
- A type constructor has kind
k1 -> k2where
List,a unary type constructor, has kind
Type -> Typeas it takes a type and yields a type. A binary type constructor like
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) -> Typeis ahigher-ordertype constructor (it takes a unary type constructor and yields a type).