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.
-- Nullary type constructors Int :: * String :: * -- Unary type constructors  :: * -> * Maybe :: * -> * Vector :: * -> * -- Unary type constructors applied to one type [Int] :: * Maybe String :: * Vector Int :: *
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
λ> data Nat = Zero | Succ Nat λ> :k 'Zero 'Zero :: Nat λ> :k 'Succ 'Succ :: Nat -> Nat λ> data List a = Nil | Cons a (List a) λ> :k Nil 'Nil :: List a λ> :k Cons 'Cons :: a -> List a -> List a
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 A (x :: * -> *) = B (x Int) λ> :k A Maybe A Maybe :: * λ> :k A  A  :: * λ> let x = B $ Just 1 λ> let y = B [1,2,3] λ> :t x y :: A Maybe λ> :t y y :: A 
Data.Proxy uses a
* in the type constructor and ignores it in the data constructor.
λ> data KProxy (x :: *) = KProxy λ> :k KProxy Int KProxy Int :: * λ> :k KProxy (Int,String) KProxy (Int,String) :: *
Allows the use and definition of of types with operator names (symbols) like
λ> data a + b = Plus a b λ> :t Plus 1 2 Plus 1 2 :: (Num b, Num a) => a + b λ> :t Plus 1 "123" Plus 1 "123" :: (Data.String.IsString b, Num a) => a + b λ> type Foo = Int + Bool λ> :k Foo Foo :: *
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.