Kinds in Haskell
- type constructor arguments are types
- data constructor arguments are values of the specified types
data declares a type constructor on the left hand side and a data constructor on the right hand side.
Bool is a simple example. None of the constructors take arguments.
Bool is the type constructor and
False are the data constructors.
There is a type constructor
User that takes no arguments and a data constructor
User that takes a
String and an
Maybe is a type constructor that takes a single argument,
Nothing is a data constructor that takes no arguments and
Just is a data constructor that takes one argument of type
a. The type constructor of
Just 1 would be
Maybe Int. The type for a data constructor maybe polymorphic (determined by the the type constructor) or fixed (using a type like
A kind is the type of a type constructor. Ordinary types have the kind
*. This means they do not need another type as an argument and can be directly related to a value. For example,
Int can have values such as
[Int] can be
[0,1,2]. These types are inhabited types. They have values.
A type like
Maybe has the kind
* -> *. It needs to be given a type before it can be related to any values. These types are unihabited types. They do not have values. When we provide a type to these types, we can make inhabited types like
Just Double and they have values like
ghci we can query the kind of a type with
:k Int returns
Int :: *,
:k Maybe returns
Maybe :: * -> *. Here are the kinds of some common types.
There are more complicated kinds. We can even have partially applied kinds.
(->) all require two kinds
* -> * -> *. If we give any of these only one type
Either String or
(,) Int then the kind is
* -> *.
-- Binary type constructors Either :: * -> * -> * (,) :: * -> * -> * (->) :: * -> * -> * -- Binary type constructors applied to one type Either Int :: * -> * (,) Int :: * -> * (->) Int :: * -> * -- Binary type constructors applied to two types Either Int String :: * (,) Int String :: * (Int,String) :: * (->) Int String :: * Int -> String :: *
What to Remember about Kinds
- Kinds are the type of a type constructor.
- Kinds represent the arity (number of parameters) of a type constructor.
- Kinds are a higher-order type operator.
*is the kind of an inhabited type. Inhabited types have values.
- All other kinds (
* -> *,
* -> * -> *,
(* -> *) -> *, etc.) are uninhabited types. Uninhabited types do not have values.
Names of Kinds
*nullary type constructor.
* -> *unary type constructor.
* -> * -> *binary type constructor.
(* -> *) -> *higher-order type constructor.
GHC Language Extensions
Allows promotion of data types to kind level. Promote datatype to be a kind and its data constructor to be a type constructor. Promoted constructors are prefixed with
Allows kind polymorphic types. This introduces kind variables. We can name a variable that has a particular kind signature in the type constructor and then apply it to a type in the data constructor.
Assume we want to have a constructor for an
Int that is contained in something but we do not care what the container is.
Data.Proxy uses a
* in the type constructor and ignores it in the data constructor.
Allows the use and definition of of types with operator names (symbols) like
Allows kind declaration and operations to be as descriptive as types: explicit quantification over kind variables, higher-rank kinds, type synonyms and families in kinds, etc.