Kinds in Haskell

2017-06-19
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.

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 * -> *.

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 '.

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.Proxy uses a * in the type constructor and ignores it in the data constructor.

TypeOperators

Allows the use and definition of of types with operator names (symbols) like (+), (:>), :<|>, .:, etc.

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.

References