---

An introduction to DataKinds and GHC.TypeLits

Posted on July 30, 2014

Kinds are kind of like types of types

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.

Unstarlike kinds

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

An introduction to DataKinds

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.

DataKinds give you free type literals, by the way

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

Proxies, like existentials, but exactly the opposite.

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

Run-time stringification

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)

Simple example: instances for the command line.

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/
 _|
   \

---

“A creative man is motivated by the desire to achieve, not by the desire to beat others.”

— Ayn Rand