## An introduction to DataKinds and GHC.TypeLits

Posted on July 30, 2014

You intuitively understand that the type of the value *1* is *Int* within the expression:

`λ 1 :: Int`

Kinds extend this intuition for type constructors. The kind of the type constructor *Int* is * within the expression:

```
λ :kind Int
Int :: *
```

The * means that the type constructor is a fully applied lifted type. Lifted means that the value may contain bottom, or is boxed (can be jammed into a closure). You can think of types of kind * as types ready to have *boxed* values associated with them. Haskell calls these types *inhabited*.

When you see an arrow from kind to kind, you are reading the signature of a type with free type variables. Once these type level functions have had types applied to them, they become fully applied and inhabitable.

So a function at the value level:

```
λ :type (+1)
(+1) :: Num a => a -> a
λ :type (+1) 1
(+1) 1 :: Num a => a
```

Looks much like an equivalent function at the type level:

```
λ :kind Maybe
Maybe :: * -> *
λ :kind Maybe Int
Maybe Int :: *
```

Monad transformers are another interesting example:

```
λ :kind ReaderT
ReaderT :: * -> (* -> *) -> * -> *
λ :kind IO
IO :: * -> *
λ :kind ReaderT Int IO ()
ReaderT Int IO () :: *
```

If any of that confused you, I’d suggest skimming through the Wikipedia article for kinds and the informal semantics section of the GHC users guide.

Despite all these stars flying about, not all kinds are star. Class constraints are, funnily enough, Constraints.

```
λ :kind (forall a. Num a)
(forall a. Num a) :: Constraint
```

Unboxed primitives are magical hashes.

```
λ :set -XMagicHash
λ import GHC.Prim
λ :type 'x'#
'x'# :: Char#
λ :kind Char#
Char# :: #
```

You’ll note these hashes are *not* lifted types, you can’t do some things that you might think you could.

```
λ :kind Maybe Char#
<interactive>:1:7:
Expecting a lifted type, but ‘Char#’ is unlifted
In a type in a GHCi command: Maybe Char#
λ undefined :: Char#
<interactive>:59:1:
Kind incompatibility when matching types:
a0 :: *
Char# :: #
In the first argument of ‘print’, namely ‘it’
In a stmt of an interactive GHCi command: print it
```

DataKinds are relatively simple. You turn on the extension and all of a sudden some of your data types have unique kinds!

```
λ :set -XDataKinds
λ data Animal = Pegasus | Octopus
λ :kind Pegasus
Pegasus :: Animal
```

There’s a few restrictions on what gets promoted to the kind level. You can read more about this in the datatype promotion section of the GHC users guide, which has a few nice examples too. None of that will be important for what we’re trying to do today, though.

Somewhat confusingly, type level literals are provided by the DataKinds extension. This interacts with the GHC.TypeLits package to provide two magical kinds, *Nat* and *Symbol*. We will ignore Nat, we’re not playing with natural numbers today.

The compiler will give you all possible type literals and an instance for the type class *KnownSymbol* for free:

```
data ("a" :: Symbol) -- type "a" of kind Symbol
data ("b" :: Symbol)
...
data ("ab" :: Symbol)
...
```

```
instance KnownSymbol "a"
instance KnownSymbol "b"
...
instance KnownSymbol "ab"
...
```

Because the type literal “a” has a kind of *Symbol*, we can never inhabit a Haskell value with it. Nevertheless, there is a trick to pass these things around as regular haskell values: Data.Proxy. There is not much documentation of *Proxy*, but let’s go through what we have.

```
-- | A concrete, poly-kinded proxy type
data Proxy t = Proxy
```

You can see that it’s essentially an existential in reverse. An existential will take a value and hide type information associated with it, keeping only a constraint. A *Proxy* will take no value and attach type information to it.

What do they mean by poly-kinded, you ask? Well, note that t is never used, t could really be anything! Well, the PolyKinds module provides the machinery to allow t to be of any kind.

```
λ :kind Proxy
Proxy :: k -> *
```

The k here stands for any kind. This means we can put our symbol in it and pass it around as a concrete value.

```
λ let p = Proxy :: Proxy "hai"
λ print p
Proxy
```

Within GHC.TypeLits lives a magical function:

`symbolVal :: forall n proxy. KnownSymbol n => proxy n -> String`

So we can get from a Symbol to a String at runtime via a Proxy, but what about the other way?

```
data SomeSymbol = forall n. KnownSymbol n => SomeSymbol (Proxy n)
someSymbolVal :: String -> SomeSymbol
```

There’s even a function for comparing these KnownSymbols:

```
sameSymbol :: (KnownSymbol a, KnownSymbol b)
=> Proxy a -> Proxy b -> Maybe (a :~: b)
```

This means that we can check for symbol equality at runtime, against a runtime input!

```
same :: (KnownSymbol a, KnownSymbol b) => Proxy a -> Proxy b -> Bool
same a b = isJust (sameSymbol a b)
```

Putting this all together now, we can define an API for users to implement non-overlapping command-line actions.

```
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE FlexibleInstances #-}
import GHC.TypeLits
import Data.Proxy
import System.Environment
import Data.Maybe
import Control.Monad
-- | An existential box to place anything that is a Handler and KnownSymbol.
data SomeHandler
= forall h. (KnownSymbol h, Handler h) => SomeHandler (Proxy h)
class Handler h where
-- We need to pass the proxy in here because a class has to work on a
-- value that mentions at least one type variable.
handleIt :: Proxy h -> IO ()
-- | The type just goes inline as a literal.
instance Handler "dance" where
handleIt _ = putStrLn "* *\n \\o/\n _|\n \\"
-- | The user will need to place the commands in here to be iterated over to
-- check for a match.
handlers :: [SomeHandler]
handlers = [SomeHandler (Proxy :: Proxy "dance")]
same :: (KnownSymbol a, KnownSymbol b) => Proxy a -> Proxy b -> Bool
same a b = isJust (sameSymbol a b)
handleCommand :: [String] -> IO ()
handleCommand [] = error "please to command"
handleCommand (str:_) =
-- A case statement is needed to extract the existential here, or GHC's
-- brain explodes.
case someSymbolVal str of
SomeSymbol user_proxy ->
forM_ handlers $ \(SomeHandler proxy) ->
when (same user_proxy proxy) (handleIt proxy)
main :: IO ()
main = getArgs >>= handleCommand
```

And for the fruits of our labour:

```
$ runhaskell Commands.hs dance
* *
\o/
_|
\
```