Kinds and Type Level Programming 2

Written 2019-10-14

This is the continuation of my first post on advanced type-level programming features of the Haskell programming language. In this post I am going to implement some features of the haskell Prelude on the type level.

Since the features we are going to use in the following are not standard Haskell as defined by the Haskell2010 Report, we will start with activating a number of language extensions to get all the code in this post to work:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE RankNTypes #-}

import GHC.TypeLits (TypeError (..), ErrorMessage(..))

Booleans and control structures

The best type-level equivalent to a function on the value-level is a (closed) type family. We will start out by defining a few basic type families to model basic boolean logic and conditions.

type family Negate (x :: Bool) :: Bool where
  Negate True = False
  Negate False = True

type family Equals (a :: k) (b :: k) :: Bool where
  Equals a a = True
  Equals _ _ = False

type family And (a :: Bool) (b :: Bool) :: Bool where
  And True True = True
  And _    _    = False

type family Or (a :: Bool) (b :: Bool) :: Bool where
  Or False False = False
  Or _     _ = True

An essential control structure is if/then/else branching. Haskell does not provide this for us on the type level, but we can still roll our own. What we do is to write type family with one boolean parameter (the condition) and two parameters representing the result of the then/else branches.

type family IfThenElse (c :: Bool) (a :: k) (b :: k) where
  IfThenElse True a _ = a
  IfThenElse False _ b = b

Basic list processing

By using the DataKinds extension, Lists Haskell automatically lifts lists to the type level for us. Instead of defining our own list-type we will simply reuse Haskell's List type.

Head & tail with custom type errors

Recall the value level definition of head:

head :: [a] -> a
head (x:_) = x
head [] = error "Head of empty list"

Pattern matching on a list's head in a type family is very straight forward, in fact we did so in the previous post. What's new to us is the error call in the case of an empty list. It turns out just as we can call error on the value level, Haskell also lets us do an error call on the type level which will lead to a compile-time error message. For this we need the GHC.TypeLits import from above. Our head function will then look like this:

type family Head (xs :: [a]) :: a where
  Head '[] = TypeError (Text "Head of empty (type level) list!")
  Head (x ': _) = x

Remember that the single quote (') before an identifier is for emphasizing that we are talking about the "lifted" type level version. Text is a constructor of the TypeError type. With this technique, we can easily define a type level version of tail.

type family Tail (xs :: [a]) :: [a] where
  Tail '[] = TypeError (Text "Tail of empty (type level) list!")
  Tail (_ ': xs) = xs

Catenating lists

List concatenation will come in very handy for some of the next steps:

type family Catenate (x :: [k]) (y :: [k]) :: [k] where
  Catenate '[] ys = ys
  Catenate (x ': xs) ys = x ': (Catenate xs ys)

Higher order functions

One of the more significant features of the Haskell programming language is its ubiquitous use of higher order functions. What would our little type-level Prelude be without some higher order functions of our own?
One of the simples and most frequently used higher order functions in standard Haskell is the dot operator for function composition, so we will define the type-level equivalent of that first:

type family Compose (f :: a -> b) (g :: b -> c) (x :: a) :: c where
  Compose f g x = g (f x)

An other common higher order Haskell function is the filter function. In order to implement this, we will have to reuse some of the functionality we implemented previously:

type family Filter (predicate :: k -> Bool) (list :: [k]) :: [k] where
  Filter predicate '[] = '[]
  Filter predicate (x ': xs) =
    Catenate (IfThenElse (predicate x) '[x] '[]) (Filter predicate xs)
Similarly we can define type level analogues of the standard functions fold and map.
type family Map (f :: a -> b) (xs :: [a]) :: [b] where
  Map f '[] = '[]
  Map f (x ': xs) = (f x) ': (Map f xs)

type family Fold (f :: b -> a -> b) (x :: b) (as :: [a]) :: b where
  Fold f x '[] = x
  Fold f x (a ': as) = Fold f (f x a) as