Time and again, kinds have proven themselves to be a confusing concept for many Haskell beginners. Chances are, if you have been learning or using Haskell for some time now, you have likely ran into a kind-related error such as the following:

>> instance Monad Bool where

<interactive>: error:
  • Expected kind ‘* -> *’, but ‘Bool’ has kind ‘*’
  • In the first argument of ‘Monad’, namely ‘Bool’
    In the instance declaration for ‘Monad Bool’

Surprisingly, there have been absolutely no articles to date which tackle Haskell’s kind system comprehensively, offering mere crumbs of knowledge scattered here and there which beginners have to piece together with enough perseverance and learning aptitude. This article seeks to provide a from-scratch explanation of the kind system, its motivations, shortcomings, and semantics in the context of Haskell. The end goal of this article is that even beginners should be able to take a good look at the singletons library and have a decent grasp of the peculiar ways in which kinds are employed in its design.

Table of Contents

1. Values, Types, and Kinds
   1. Implicit Kinds
   2. Kind Signatures
   3. List of Inhabited Kinds
   4. Constraint Kinds
   5. Data Kinds
   6. Polykinds
   7. Kinds of Kinds
2. Universes
   1. Cumulative Universes vs. Universe Polymorphism, and Haskell
3. Sample Applications of Kind-level Programming
   1. Closed Type Families
   2. Refinement Types
   3. Quasi- Dependent Typing via Singletons
4. Conclusion

Values, Types, and Kinds

Most programming languages out in the wild have some notion of types and values. In Rust, for instance, we have the primitive type bool which has two values: true and false. Similarly, we have the abstract data type Bool in Haskell, containing two possible values in the form of the constructors True and False. However, Haskell takes this a step further by attaching a special sort of ‘type’ to types, which we call kinds.

Let us take a look at the kinds of several common Haskell data types:

1. Bool has the kind Type, notated Bool :: Type
2. Maybe has the kind Type -> Type, notated Maybe :: Type -> Type
3. Either has the kind Type -> Type -> Type, notated Either :: Type -> Type -> Type
4. forall a b. Either a b has the kind Type, notated Either a b :: Type

Type is one of the primitive kinds in Haskell. Type is the kind of all fully-specialized, user-definable data types. Type is also aliased as *, which you will see in compiler error messages instead; we can use these two synonyms interchangeably, albeit modern GHC now discourages using *. The reason for this is that * was more or less a design oversight; it was convenient to type and looked like a ‘type wildcard’ symbol that was intuitive to think about, however in modern times it conflicts with the type-level natural multiplication operator (*) :: Nat -> Nat -> Nat which we will briefly go over later in this article.

Let us start with Bool. Bool has kind Type because it is (quite literally) just a type.

What about Maybe :: Type -> Type? Conceptually, we can think of Maybe as a type-level function taking some type a and returning a new type Maybe a, hence the function arrow syntax. The same logic applies to our third example of Either :: Type -> Type -> Type, which takes two type inputs instead of one, hence the double function arrow syntax.

Our fourth and final example serves to contrast the third example: that Either and Either a b have completely different types. We refer to the “type constructor” Either by itself in the third example, and this “constructor” does indeed take two type inputs to produce a new type Either a b. In our fourth example, however, we have already applied the “type constructor” Either to two universally-quantified variables, thus its type reduces down to just Type. These semantics are no different from how the type of some function f :: a -> a -> a by itself differs from its fully-applied form f x y :: a.

Like a regular function, we can also partially apply these “type constructors”, which can help us reduce their arity down enough to match that of a particular type variable’s kind, as you will see later. Unlike a regular function, however, there is currently no such thing as a ‘type-level lambda’. As such, this sort of declaration would be malformed:

-- | A hypothetical way to make a Functor instance for Either in its first argument
-- instead of its second, if only it worked, that is.
instance Functor (\c -> Either c a) where

You can already see why type-level lambdas might be problematic: we would be able to make two perfectly valid Functor instances for Either, one in each argument, and fmap dispatch would be undecidable if both arguments to Either are the same type. Normally, we would create a newtype wrapper instead to achieve this sort of design, which would ‘flip’ the order of the type variables to allow for the alternate instance.

Implicit Kinds

Thinking of types as higher-level functions is key to understanding and avoiding kind errors. Remember that you can view the kind of any type in GHCi by typing :k TypeName. That said, this may not be the most efficient workflow for many Haskellers. Ideally, we should be able to deduce the kinds of type variables by just looking at how they are used in context. Let us take a look at the declaration of the class of monad transformers, MonadTrans:

class MonadTrans t where
  lift :: m a -> t m a

We have three type variables in this declaration: t, m, and a. To aid in our deduction of their kinds, the first thing we want to acknowledge is the kind of the function arrow (->):

(->) :: Type -> Type -> Type  

Surprisingly, the function arrow only takes fully-applied types as parameters. You will get a type error if either side of a function arrow contains a higher-arity kind such as (Type -> Type). As such, we can deduce from the method signature lift :: m a -> t m a that m a :: Type and t m a :: Type.

Since type variable application is left-associative like function application, we can deduce that:

• m a is similar to f x
• t m a is really just (t m) a, which is similar to f x y = (f x) y

As such, we can further deduce:

• m has kind Type -> Type
• a has kind Type
• With these assumptions, m a reduces to Type, which is correct.
• It follows that t has kind (Type -> Type) -> Type -> Type.
  • By virtue of referencing the same variables m and a that we already know the kinds of.

This is the style of critical thinking that should be applied when reasoning about implicit kinds. Remember that without further context*, the kind of a type variable always defaults to Type. If you wish to specify a different kind, you need to add explicit kind signatures.

* - “Context” in this case also includes the presence of -XPolyKinds, covered later on

Kind Signatures

Let us analyze what is going on behind kind signature expressions such as a :: *:

<type> :: <type>

The fact that the right hand side of the expression is simply <type> instead of <kind> may seem erroneous at first glance, but this is precisely how GHC Haskell encodes kinds. You see, kinds are just types. What we like to think of the kind */Type is actually just a cyclic type synonym defined in Data.Kind as follows:

type Type = Type
type * = Type

What is interesting about how Type is defined is that it relies on some compiler magic. If you try to define a similar cyclic type synonym, you will get an error like the following:

>> type Artificial = Artificial

<interactive>: error:
  Cycle in type synonym declarations:
    <interactive>: type Artificial = Artificial

An interesting property of this realization that kinds are just types is that, if the left hand side of a kind signature is a type variable, then any type can appear in the right hand side, even if those kinds are uninhabited. Strictly within the context of Haskell, we say a kind is uninhabited when there there are no types which have that particular kind. Take, for instance, the following:

{-# LANGUAGE EmptyDataDecls #-}

-- | We create an 'artificial' kind in the style that the kind 'Type' is defined.
data Artificial

-- | We specify that the type variable @a@ has kind 'Artificial'
data Irreducible (a :: Artificial)

-- | We use () for demonstration purposes here but this could be any other type.
-- Recall that 'Artificial :: Type', so not even that will help us here. 
f :: Irreducible ()
f = undefined

-- | Oh no! There are absolutely no types in Haskell with our kind 'Artificial',
-- making it impossible for us to fully apply 'Irreducible' down to the kind 'Type'
<interactive>: error:
    • Expected kind ‘Artificial’, but ‘()’ has kind ‘*’
    • In the first argument of ‘Irreducible’, namely ‘()’
      In the type signature: f :: Irreducible ()

In other words, while you can theoretically put any type on the right hand side of a kind signature of a type variable, it says nothing bout whether there exists a type that can substituted into that type variable to begin with. If we were to use types-as-kinds naively like this, we would simply create unusable code. The compiler assigns all fully-applied top-level user-defined data types the kind Type and there is simply no way around this. To attempt otherwise would result in an error similar to the following:

{-# LANGUAGE EmptyDataDecls, DataKinds, KindSignatures #-}

data Artificial

-- | We specify that the whole type 'Unreducible (a :: Artificial)' has kind 'Artificial'.
-- This is different from just saying 'Unreducible' by itself, which has kind 
-- 'Artificial -> Artificial'.
data Unreducible (a :: Artificial) :: Artificial

<interactive>: error:
  • Kind signature on data type declaration has non-* return kind Artificial
  • In the data declaration for ‘Unspecializable’

As such, if we are to write meaningful code, care must be taken to only use inhabited kinds on the right hand side of a type variable kind signature.

List of Inhabited Kinds

Fortunately, Type is not the only inhabited kind in GHC Haskell. If this were the case, a kind system would be useless since we can assume all types have the same kind to begin with. The following is a list of all inhabited kinds in modern GHC 8.10.x -era Haskell:

• Type / *, the kind of all regular, user-definable data types
  • Int :: Type
  • forall a. [a] :: Type
  • forall a. Maybe a :: Type
• Constraint, the kind of constraint expressions
  • forall a. (Show a) :: Constraint
  • forall a. (Show a, Ord a) :: Constraint
  • forall a b. (Show a, (Ord a, Eq b)) :: Constraint
• Nat, the kind of type-level natural numbers
  • As seen in declarations such as Vec 5 a
  • 1 :: Nat
  • 2 :: Nat
  • 3 :: Nat
• Symbol, the kind of type-level string literals
  • As seen in declarations such as HasField "someField" x
  • "foo" :: Symbol
  • "bar" :: Symbol
  • "baz" :: Symbol
• Data kinds
  • [k] forall inhabited kinds k, the kind of type-level lifted list constructors
    • (:) and [] are constructors for the list data type
    • Therefore, there exists lifted representations of these: (':) and '[]
    • Thus, one can define type-level lists using familiar syntax: (Int ': '[]) :: [Type]
    • Special case: list syntax is also lifted: '[Int, Char, Bool] :: [Type]
  • All other user-defined data type constructors
    • Every constructor A :: t of some type will have a generated type-level lifted variant 'A :: t
    • In other words, the type-level variant has a kind referring to the type signature of the original
    • Ex. a GADT constructor A :: forall a. Int -> Maybe a -> X a has lifted variant 'A :: forall a. Int -> Maybe a -> X a
    • This will make more sense further below

We have previously discussed the kind Type. In the following sections, we will go over all these other kinds one by one.

Constraint Kinds

Requires {-# LANGUAGE ConstraintKinds #-}, which enables the Constraint kind for constraints.

In crude terms, a constraint refers the part to the left of the forall x y z. (if present) and right of the => in a function signature, class head, instance head, or data declaration:

f :: forall a. -> (Show a, Ord a) <- => a

class -> (forall m. Monad (t m)) <- => MonadTransProper t where

instance -> (a ~ b) <- => Show (a,b) where

data -> BadPractice a <- => DontDoThis

Constraints are all tuples, and each element of a constraint tuple must itself be a constraint. When we write a singular constraint such as f :: Show a => a, what we are really declaring is the 1-tuple f :: (Show a) => a. Similarly, constraint tuples can be nested, but their semantics will behave as though they are “flattened”. In other words, f :: (Show a, (Ord a, Eq a)) => a \(\cong\) f :: (Show a, Ord a, Eq a) => a.

All type classes have a kind which reduce down to Constraint. For instance, MonadTrans :: (Type -> Type) -> Type -> Type -> Constraint, which is just the kind of its type parameter t (which we have proven above) to Constraint. When we fully apply a type class to one or more type variables, we get a plain old Constraint, which we can then include in a constraint tuple.

Each individual 1-tuple constraint in a constraint tuple refers to a type class. Even the type equality operator ~ and kind equality operator ~~ are infix type classes defined in the base library.

The key takeaway with constraint kinds is this: all constraints have the same kind Constraint no matter how large the tuple is or how nested the tuple is. forall a. (Show a) :: Constraint just as forall a t. ((Show a, Ord a), Eq a, forall m. Monad (t m)) :: Constraint. The fact that we can attach a unique kind to constraints allows us to use constraints in type synonym and type family declarations, which allow for polymorphic-constraint programming:

-- | A type family which converts a type-level list of constraints to a `Constraint` tuple
type family ToConstraint (xs :: [Constraint]) :: Constraint where
  -- | Base case: an empty list is the empty constraint tuple (), i.e. no constraint
  ToConstraint '[] = ()
  -- | Match on the head @x@ of the list and unfold a constraint tuple recursively.
  -- It will look like (c1, (c2, (c3, (c4, (c5))))) by the end of the unfolding.
  ToConstraint (x ': xs) = (x, ToConstraint xs)

-- | Now we can write our constraints as lists instead of tuples!
-- Why would we want to do this? For no reason in particular, it just looks marginally nicer.
-- Constraint kinds are more useful as associated types in type classes or data parameters.
foo :: forall a. ToConstraint '[Show a, Ord a] => a -> a
foo = id

Data Kinds

The DataKinds extension generates type-level lifted representations of data constructors for us, whose kinds are the type of the data constructor. These lifted constructors are referenced by a front tick ' in front of the constructor name:

{-# LANGUAGE DataKinds #-}

data Example a where
  Foo :: Example ()
  Bar :: forall a x y. x y -> x a -> Example (x y)
  Baz :: a -> Example a

-- | The above GADT will conceptually generate the following lifted constructors for us:
data 'Foo :: Example ()
data 'Bar :: forall k (a :: k) (x :: k -> Type) (y :: k). x y -> x a -> Example (x y)
data 'Baz :: forall a. a -> Example a

In practice, data kinds allow us to define our own closed kinds, allowing for better type safety in certain areas. For instance, it can be used to make certain type families total, whereas otherwise one would have to write a redundant catch-all instance if it were parameterized over Type. If you will also notice, 'Bar has a similar arity-2 signature “shape” to Either. 'Bar applied to two types reduces down to z ~ (x y) => Example z, which parallels Type. It may therefore be more intuitive to think of 'Bar like the following:

data (forall k (a :: k) (x :: k -> Type) (y :: k). 
  (f ~ x y, g ~ x a) => 'Bar f g :: Example (x y)) 

This also means that one can “match” on the type parameters of 'Bar like they would with Either: (x ~ 'Bar f g); (x ~ Either f g). Likewise, the same applies to 'Baz, albeit it may be more appropriate to compare it to Maybe instead.

Type-level Naturals and String Literals

Type-level naturals and string literals are supported by GHC as the special kinds Nat and Symbol respectively. The motivation for providing special kinds for these is that the set of natural numbers and strings is infinite. In order to conveniently program with type-level natural numbers and strings, we do not want to use clunky Peano number -like constructs such as represent 5 with (S (S (S (S (S Z))))). As a result, GHC provides “magical” automatically-generated types for the natural numbers and strings with their respective kinds in order to facilitate this sort of type-level programming.

Conceptually, we can think of the types Natural and String as ADTs defined as follows:

data Natural = 1 | 2 | 3 | 4 | 5 | ...
data String = "a" | "aa" | "ab" | "abc" | ...

Following from DataKinds behavior, these would generate the types '1, '2, '3, ... and '"a", '"aa", '"aab", ..., however in reality these ADTs are not defined like this due to their infinite nature. They rely on some compiler magic, and thus their DataKinds representation is unique from the rest: we can refer to their “constructors” without ticks in front, and they do not bear the kind of their data type. That is to say, '1 :: Natural and "aab" :: [Char] is simply incorrect. Their kinds are instead specially assigned to Nat and Symbol.

Consider taking a look at the GHC.TypeLits module for a list of type synonyms, type families, and functions for working with the Nat and Symbol kinds. The following is a snippet showcasing usage of this module:

-- | We need 'NoStarIsType' if we want to use the '(*) :: Nat -> Nat -> Nat' type operator
-- otherwise GHC will interpret '*' as the synonym for 'Type'.
{-# LANGUAGE NoStarIsType, TypeOperators, TypeApplications, ConstraintKinds, RankNTypes #-}

import GHC.TypeLits

-- | The idea behind this function is simple. We pass to it a @Proxy c@ to disambiguate the
-- constraint variable @c@, and if the constraint holds, this function will typecheck and 
-- print "Typechecks" in GHCi.
prop :: forall c. c => Proxy c -> String
prop _ = "Typechecks"

>> prop $ Proxy @((5 * 3) ~ 15)
>> "Typechecks"
>> prop $ Proxy @((15 / 3) ~ 5)
>> "Typechecks"
>> prop $ Proxy @((5 - 2) ~ 3)
>> "Typechecks"
>> prop $ Proxy @((5 + 2) ~ 7)
>> "Typechecks"
>> prop $ Proxy @((0 - 1) ~ 0)
-- | The type level natural numbers, by definition, do not go below 0.
-- (0 - 1) is a valid type, we just don't have the type (-1) to use on
-- the right hand side, so the only way this will work is to say
-- ((0 - 1) ~ (0 - 1)), which is pointless.
<interactive>: error:
  • Couldn't match type ‘0 - 1’ with ‘0’ arising from a use of ‘prop’
  • In the expression: prop $ Proxy @((0 - 1) ~ 0)
-- | (5 - 2) is indeed less than 10
>> prop $ Proxy @(((5 - 2) `CmpNat` 10) ~ 'LT)
>> "Typechecks"
-- | (5 - 2) is indeed equal to 3
>> prop $ Proxy @(((5 - 2) `CmpNat` 3) ~ 'EQ)
>> "Typechecks"

>> prop $ Proxy @("foo" `AppendSymbol` "bar" ~ "foobar")
>> "Typechecks"
>> prop $ Proxy @("foo" `CmpSymbol` "foo" ~ 'True)
>> "Typechecks"

The module also contains the functions someNat/someNatVal and someSymbol/someSymbolVal to allow us to work with existentials (i.e. Nats and Symbols only known at runtime) in exchange for type ambiguity. We will talk about using existentials in kind-level programming towards the end of this article.

Polykinds

With so many kinds in Haskell, we want to be able to write code that is as kind-generic as possible. Writing naive code without explicit kind signatures would simply result in unnecessarily constraining type variables to Type, and in many cases, this is not what we want.

Enter the PolyKinds extension, which allows us to specify type variables on the right hand side of kind signatures. Since kinds are just types in Haskell, you have been able to specify types we typically think of as kinds in class instance declarations all along! Without being able to use these “kind variables” on the right hand side of a kind signature, however, this is mostly useless without PolyKinds.

The following are a few examples of PolyKinds usage:

-- | Conventionally we notate the 'kind variable' as @k@
>> class Example (a :: k) where

-- | All valid
>> instance Example 1 where
>> instance Example "foo" where
>> instance Example Bool where

-- | Whereas if we were to forget to specify a polymorphic kind variable for @a@:
>> class BadExample a where

-- | Valid
>> instance BadExample Bool where
-- | Oh no! (1 :: Nat), but the class instance implicitly expects a @Type@.
>> instance BadExample 1 where

<interactive>: error:
    • Expected a type, but ‘1’ has kind ‘Nat’
    • In the first argument of ‘BadExample’, namely ‘1’
      In the instance declaration for ‘BadExample 1’

-- | Same deal, but for @Symbol@
>> instance BadExample "foo" where

<interactive>: error:
    • Expected a type, but ‘"foo"’ has kind ‘Symbol’
    • In the first argument of ‘BadExample’, namely ‘"foo"’
      In the instance declaration for ‘BadExample "foo"’

With PolyKinds, any number of type variables can appear on the right hand side of a kind signature as part of type application; in fact, the right side can be any valid type expression potentially involving type synonyms and type families, so long as they reduce to a type with kind Type:

-- | Bad! @t@ has implicit kind @Type@; applied to the kind-level function @k@, the
-- expression @k t@ evaluates to kind @Type -> Type@, but the right hand side of the
-- kind signature for @a@ must have kind @Type@!
--
-- As we have discussed previously, the 'kind' of any kind must be @Type@, hence this
-- restriction. However if you notice, `k` when used as a "kind variable" will actually be
-- uninhabited, for there are no kinds whose 'kind' has an arity higher than 1 like what we
-- are specifying here.
>> f :: forall (k :: Type -> Type -> Type) t (a :: k t). a

<interactive>: error:
    • Expecting one more argument to ‘k t’
      Expected a type, but ‘k t’ has kind ‘* -> *’
    • In the kind ‘k t’
      In an expression type signature:
        forall (k :: * -> * -> *) t (a :: k t). a
      In the expression: f :: forall (k :: * -> * -> *) t (a :: k t). a

-- | A correct example.
--
-- The compiler will assume `k t` evaluates to `Type` so that the kind of `f` remains
-- well-formed. It will then try to deduce @k@ and @t@ for us as long as `a` is known 
-- based on the context the function is used in, however we can use TypeApplications 
-- to manually specify them if we wish to. In this case, @t@ has the implicit kind @Type@, 
-- thus @k@ by virtue of the being applied to @t@ has the kind-type @Type -> Type@.
>> f :: forall k t (a :: k t). a

Note that polymorphic kind variables in a forall must always come before any type variables referencing them. As such, the function f above would be malformed if the order of type variables was reversed:

>>   f :: forall (a :: k t) t k. a

<interactive>: error: Not in scope: type variable ‘k’
<interactive>: error: Not in scope: type variable ‘t’

In an earlier section, we noted that the presence of -XPolyKinds is a ‘context’ which can affect kind-defaulting to Type. Indeed, if we were to examine the kind signatures of declarations that do not use explicit kind signatures for type variables before and after enabling -XPolyKinds, we will get some surprising results:

>> :set -XNoPolyKinds
>> type S a b = ()
>> :k S
S :: Type -> Type -> Type

>> :set -XPolyKinds
>> type S a b = ()
>> :k S
S :: k1 -> k2 -> Type

In short, -XPolyKinds will change kind defaulting rules such that type variables are as kind-agnostic as possible. Such a change can definitely break codebases, so it is best to be mindful of it beforehand.

Last but not least, it is worth going over a common misunderstanding regarding polymorphic kinds; that polymorphic kind variables are magically “hidden” or “implicit” in cases like the following:

type family Example f (t :: k) (g :: k) where

Rest assured that there is no wizardry going on here. Recall that the above statement is really just sugar for what is conceptually the following:

type family (forall k f (t :: k) (g :: k). Example f t g) where

In other words, k is definitely quantified just like all the other variables, even if it is not used as an explicit parameter in the type family. In this context, its type is simply deduced from the kinds of t and g. Additionally, it implies the constraint (t ~~ g); or, that t has the same kind as g (rarely will we come across seeing operator (~~) like this!).

Kinds of Kinds

A common question that many new Haskellers ask when they learn about kinds is ‘are there kinds of kinds’? The answer to this is tricky. Formally speaking, in the realm of type theory, yes, there are ‘kinds of kinds’ or ‘types of kinds’, however you wish to phrase it, which we would call a level-3 universe. The problem is, Haskell has a finite-“universe” model, with a level-2 “universe” being the highest supported by the type system.

Recall that kinds are just types in Haskell. If we try to find the “kind” of a kind what we will get kind of the type declaration for the kind:

>> :k Nat
Nat :: *
>> :k *
* :: *
>> :k Type
Type :: *
-- See where this is going?
>> :k ((Nat -> Symbol) -> Constraint -> Type)
((Nat -> Symbol) -> Constraint -> Type) :: *
>> :k ((Type -> Symbol) -> Type -> Constraint)
((Type -> Symbol) -> Type -> Constraint) :: *

In other words, the naive ‘kind of a kind’ in all cases is merely Type, as you would expect. This may seem trivial at first glance but it is important to remember the semantics of how this works, for people tend to commit all sorts of design errors when venturing into any form of intermediate-advanced kind-level programming for the first time.

Let us now take a step back from types and kinds for a moment and take look at a generalization of both these concepts from type theory: universes. This will help us build an intuitive mental model of Haskell’s type and kind system in the greater context of things.

Universes

To get a true understand of kinds and what it means for Haskell to only have a finite-“universe” system, we need to retreat back to our ivory tower for a bit and gain an intuition for the original, theoretically-rooted generalization of types and kinds: universes. The term can sound a bit intimidating, however the concept itself is fairly trivial:

There are five things you need to know to reason about universes:

1. Every universe \(\textbf{U}_n\) is a set of types
   • Where \(n\) conventionally starts at 0 or 1, ascending
   • We will assume universes start at 1 for the purposes of this article
2. Every universe is itself a type
   • The representation of which we will refer to as \(T\ (\textbf{U}_n)\)
3. Each universe \(\textbf{U}_n\) is the union of all subuniverses \(\textbf{U}_{m}\) forall \(1 \leq m < n\), along with a singleton set of its immediate subuniverse as a type \(T\ (\textbf{U}_{n-1})\)
   • That is to say, \(\textbf{U}_n \equiv \left(\displaystyle\bigcup_{m=1}^{n-1} \textbf{U}_m\right)\ \cup\ { T\ (\textbf{U}_{n-1}) }\)
4. Cumulativity
   • Each universe \(\textbf{U}_n\) is an element in each universe \(\textbf{U}_m\), forall \(m > n\)
   • That is to say, a level-1 universe \(\textbf{U}_1\) is an element of \(\textbf{U}_2\), \(\textbf{U}_3\), …, \(\textbf{U}_\infty\)
   • A universe is never an element of itself
5. Every universe is an element of the end universe \(\textbf{U}_\infty\)
   • Meaning, there is no universe higher than \(\textbf{U}_\infty\)

Informally speaking, we can think of \(\textbf{U}_1\) as all types and \(\textbf{U}_2\) as all kinds in Haskell.

Cumulative Universes vs. Universe Polymorphism, and Haskell

An attentive reader may have noticed my choice of words regarding universes in Haskell, using peculiar language such as “informally speaking”, as well as quoting the term “universe” whenever the context was about Haskell. Strictly speaking, Haskell does not have universes in the conventional sense. Universes in the conventional type theory sense follow the cumulative model, in constrast to Haskell’s more limited approach. The main distinction here is that a “universe” in Haskell only contains the types of its immediate children universes. That is to say, types within “\(\textbf{U}_1\)” are not considered to be elements of “\(\textbf{U}_2\)” due to the extra level of indirection caused by “\(\textbf{U}_1\)” (Type :: U1 :: U2).

Beyond that, Haskell’s “universe” model cannot be represented as a linear hierarchy—another property of cumulative universes. As expounded on above, we have a potentially infinite number of possible kinds thanks to DataKinds—infinite level-1 “universes”. There is no “hacky” way in which we encode all of these kinds in a linear hierarchy, for it would imply a type belongs to an inappropriate universe, or that a universe contains a type other than what it actually should. In practice, however, this simplified model is acceptable since Haskell also supports universe polymorphism (in the usual limited sense, of course). In simple terms, universe polymorphism refers to how a type variable can stand for a universe. In strict Haskell terms—since it does not have proper universes—, we refer to it as kind polymorphism. As you may have guessed, this is precisely what PolyKinds allows for.

Sample Applications of Kind-level Programming

Closed Type Families

Data kinds allow for a more “proper” closed type families, allowing for totality and easier reasoning that comes with closed, user-definable kinds; ever-more-closely approximating the notion of a type-level function:

{-# LANGUAGE DataKinds #-}

data Example a where
  Foo :: Example ()
  Bar :: forall a x y. x y -> x a -> Example (x y)
  Baz :: a -> Example a

data Res = A | B | C

type family Demonstration (Example a) :: Res where
  Demonstration 'Foo       = 'A
  Demonstration ('Bar _ _) = 'B
  Demonstration ('Baz _)   = 'C

Refinement Types

You may have heard the phrase “propositions as types” or “propositions are just types” before. The concept of refinement types can be seen as a literal interpretation of these statements. A refinement type can be thought of as a wrapper for a type, additionally parameterizing it over a type-level predicate; in other words, a type-level expression that evaluates to the kind Bool. This type-level predicate is canonically used to represent static guarantees about the runtime values of its associated type (pun not intended).

Refinement types were essential to my own library surtur, which sought to ensure that Vulkan API calls were always sound given a list of static guarantees regarding device (GPU) properties. As it turns out, this also helped ensure that usage of the Vulkan API is standards-compliant, eliminating the age-old problem of determining whether the graphics driver or the program is at fault. The system of guarantees in question was implemented via nested monadic contexts parameterized over a higher-kinded list of refinement types.

Quasi- Dependent Typing via Singletons

By a long shot, the infamous singletons library contains some of the heaviest and most obscure uses of kinds one will ever see. The purposes of singletons is to essentially allow promotion of values to types and demotion of types to values. This is a roundabout way of achieving dependent types until -XDependentTypes is a thing many years from now.

Broadly speaking, dependent types allow for strong types to be used more liberally. In cases where certain type parameters may or may not be know until runtime, a compromise has to be made in their design in order to reduce how strongly-parameterized a type is (detrimental to statically-computable use cases) in order to cater to use cases where said parameters may remain unknown until runtime. Or, one could write their data structures and functions in terms of singletons, and have the best of both words in exchange for verbose and arguably-ugly syntax.

The key to understanding singletons is to read the documentation, quite literally. Normally, we think of “type synonyms”, “type families”, and “associated types” as, well, types. But recall that kinds are really just label types. Nothing is preventing a synonym or family instance from returning such types. This is the overarching concept found throughout singletons: kind synonyms, kind families, and associated kinds. This is not a deficiency with Haskell’s syntax per se, for recall that a formal universe, too, is but a type. It is merely a change in perspective. Unfortunately, we do not have much more to go by to differentiate between type or kind synonyms/families other than the documentation and any surrounding context. Thankfully, however, singletons is a fairly well-documented library, so this is in practice not as bad as it sounds.

I strongly urge you, the reader, to check out some sample Hackage documentation for singletons if you have not already. It is an excellent way to put your comprehension of kinds to the test. You will have to take my word that the signatures look scarier than they actually are.

Conclusion

Hopefully this article has left you with a solid foundation of understanding for kinds; both how they work and how they are useful. Although this is certainly a long read, I wanted to leave little to no room for doubt by the end of it all. There used to be a long section on universes in detail, however I cut it out as the article is already long enough as it is, and I thought it irrelevant for intuition. Comments and suggestions are welcome; if I left anything worth mentioning out, I will be sure to revise this article and include it.

I leave the dual meaning of title of this article an exercise to the reader, though the choice was more of a tribute to a certain band more than anything.