# Kinds in Haskell

## Constructors

- type constructor arguments are types
- data constructor arguments are values of the specified types

The keyword `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 `True`

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 `Int`

.

`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 `Int`

, `Maybe String`

, `(Int,String)`

, etc.).

## Kind

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 `0`

, `1`

, `2`

, and `[Int]`

can be `[0,1,2]`

. These types are inhabited types. They have values.

A type like `[]`

or `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 `[Int]`

, `[String]`

, `Just Double`

and they have values like `[0,1,2]`

, `["hello","goodbye"]`

and `[1.5,2.5,3.5]`

.

In `ghci`

we can query the kind of a type with `:k`

. `: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. `Either`

, `(,)`

and `(->)`

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

#### DataKinds

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
```

#### PolyKinds

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) :: *
```

#### TypeOperators

Allows the use and definition of of types with operator names (symbols) like `(+)`

, `(:>)`

, `:<|>`

, `.:`

, etc.

```
λ> 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 :: *
```

#### TypeInType

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.