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
Type
. - A type constructor has kind
k1 -> k2
wherek1
andk2
are kinds.
For exampleList
,a unary type constructor, has kindType -> Type
as it takes a type and yields a type. A binary type constructor like->
has kindType -> 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 ahigher-ordertype constructor (it takes a unary type constructor and yields a type).