Kinds and Type Level Programming

Written 2019-09-06

Recently, I have been playing around with some more advanced features of the Haskell programming language. Specifically with type level computations and kinds. Over the coming weeks, I will write a few posts from my notes on this subject.

Distinguishing Type-Level and Value-Level

For newcomers to Haskell, the idea of computing at the type level may seem strange. These abilities are still somewhat limited but this feature set is constantly being extended and improved. An important separation that you should keep in mind is between the type level and the value level.

Let's say for example you have some String input which can be validated. One way to model this would be via a phantom type similar to this:

data NonValidated
data Validated

newtype Input a = String

readNextInput :: IO (Input NonValidated)
readNextInput = undefined -- the implementation is not relevant here

validateInput :: Input a -> Input Validated
validateInput (Input xs) = Input $ filter (/= ' ') xs

In the example above, the Input a type is just a newtype wrapper around String, which completely disappears at runtime. So even though the type is different from the String type, due to Haskell's type erasure this has no bearing on any runtime representation of information.

However, no runtime impact doesn't mean that there is no impact on the logic we can express. The phantom type ensures, that we can't accidentally pass around invalid data at compile time before the program ever runs. What happens on the type level at compilation constrains value level operations taking place at runtime.

Kinds - A Level Above Types

A problem with the code above is, that it would be possible for a programmer to introduce values of type Input Int or Input Bool or use any other type in the parameter of our Input newtype. Wouldn't it be nicer if we could be sure that we only ever got Input Validated or Input NonValidated? We can do this by introducing a new kind.

Just as there is a type-level "above" the value-level, there is a kind-level above the type level. Using standard Haskell 98, however, we hardly notice it being there. Values such as True and False are inhabitants of the type Bool. In much the same way, types such as Bool or String are inhabitants of the kind *, which is the kind of types.

The kind * is inhabited by all ordinary types that don't have type parameters. * is not the only kind we have at our disposal in standard Haskell. A familiar type of a kind other than * is Maybe. Note, that we are not talking about Maybe ByteString or Maybe Handle but just Maybe.

The kind of Maybe is (* -> *). The easiest way to think of it is, that Maybe is a function that takes an ordinary type as an argument and returns an ordinary type. Another familiar type, Either, shows us yet another kind, namely (* -> * -> *). We can actually observe this in ghci:

λ :kind Int
Int :: *
λ :kind Bool
Bool :: *
λ :kind Maybe
Maybe :: * -> *
λ :kind Either
Either :: * -> * -> *

GHC comes with an extension called DataKinds that allows us to lift data constructors to the type level. This may at first sound somewhat abstract so I'll start out with an example:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}

data ValidationState = Validated | NonValidated

newtype Input (a :: ValidationState) = Input String

Just as in our first validation example above, we defined a newtype Wrapper Input a around String. The difference, however, is that before Validated and NonValidated were two different types. And, worse, nothing prevented the type parameter of Input from being any type such as Word or (IO Int).

This changes with our lifted data type ValidationState. The DataKinds extension lifts data types and constructors up a level. So the type ValidationState becomes available to us as a kind and the two constructors Validated and NonValidated become types. We again turn to ghci:

λ :kind Validated
Validated :: ValidationState
λ :kind NonValidated
NonValidated :: ValidationState
λ :kind Input
Input :: ValidationState -> *
λ :kind Input Validated
Input Validated :: *

The DataKinds extension actually is far more powerful than our rather trivial example may suggest. Using this extension every type and constructor becomes lifted so that we e.g. have a kind Bool and True and False are types of this kind:

λ :kind True
True :: Bool
λ :kind False
False :: Bool

Bearing in mind that the standard Haskell List type is basically defined as a type with two constructors, : and [], the DataKinds extension lets us define type level lists:

λ :set -XTypeOperators
λ :kind '[]
'[] :: [k]
λ  :kind (:)
(:) :: a -> [a] -> [a]
λ :kind String ': Int ': '[]
String ': Int ': '[] :: [*]
The single quote in ': and '[] is a way to syntactically indicate that we are talking about the type level list constructors (and not the value level ones).

Type-Level Numbers and Type-Level Functions

So far we haven't done any actual computing yet: we have no type-level numbers and no way to compute anything on the type level! So let's change that by first defining natural numbers on the type level. We do this by using DataKinds to define Natural numbers:

data Nat = Z | S Nat

where Z is zero and (S x) is x+1. We now have a kind Nat and all natural numbers also exist on the type level as inhabitants of the kind Nat

The last piece of the puzzle we are missing are type level functions. GHC gives us these as an extension with the somewhat strange name TypeFamilies. A type family is basically a type level function. We will now build a type family for adding our numbers we defined above. Just like an ordinary function we start with a signature:

type family Add (a :: Nat) (b :: Nat) :: Nat where

This signature tells us that our type family Add turns two Nats into a new Nat. Now we define the whole logic as follows:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies#-}
{-# LANGUAGE UndecidableInstances#-}

data Nat = Z | S Nat

type family Add (a :: Nat) (b :: Nat) :: Nat where
  Add Z a = a
  Add (S a) b = Add a (S b)

That we have to use the UndecidableInstances extension of GHC here is a bit of a wart, but it can't be avoided. The danger here is that we could build a type family that never terminates. Since type families are always evaluated at compile-time this could lead to the compiler not terminating. In general, GHC can't decide if a type family will terminate (ultimately due to the halting problem) and therefore we have to tell GHC "it's OK, believe us" using UndecidableInstances.

As usual, we want to play with this in ghci. To actually evaluate our type family we can use the :kind! command as follows:

λ :kind! Z
Z :: Nat
= 'Z
λ :kind! (S Z)
(S Z) :: Nat
= 'S 'Z
λ :kind! (S (S Z))
(S (S Z)) :: Nat
= 'S ('S 'Z)
λ :kind! Add Z Z
Add Z Z :: Nat
= 'Z
λ :kind! Add Z (S Z)
Add Z (S Z) :: Nat
= 'S 'Z
λ :kind! Add (S Z) (S Z)
Add (S Z) (S Z) :: Nat
= 'S ('S 'Z)

Conclusion

We have covered a lot of ground in this post. The discussed material, along with a bit of basic Haskell, will allow us to do some quite amazing things. I will continue this exploration of type-level computation in an upcoming post very soon. Until then I encourage anyone who reads this to play around with the code above. See you soon!