Kinds of Types

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 kindType.
  • A type constructor has kindk1 -> k2wherek1andk2are kinds.

For exampleList,a unary type constructor, has kindType -> Typeas 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) -> Typeis ahigher-ordertype constructor (it takes a unary type constructor and yields a type).