Multi-parameter type classes and functional dependencies made type-level programming possible. Back in 2000, Thomas Hallgren showed an implementation of insertion sort as an example of static computation using functional dependencies. The code has a strong resemblance to logic programming which looks bizarre to most functional programmers. In this post, I will show you a more “functional-style” implementation of insertion sort using closed type families.

Term-level insertion sort

Here’s an implementation of insertion sort we all know.

sort :: (Ord a) => [a] -> [a]
sort [] = []
sort (x : xs) = insert x (sort xs)
insert :: (Ord a) => a -> [a] -> [a]
insert x [] = x : []
insert x (y : ys) = insert' (compare x y) x y ys
insert' :: (Ord a) =>Ordering-> a -> a -> [a] -> [a]
insert' LT x y ys = x : (y : ys)
insert' _ x y ys = y : insert x ys
l = [1, 3, 2, 4, 7, 9, 5]

sort l sorts the given list.

λ> sort l
[1,2,3,4,5,7,9]

To implement insertion sort in type-level, we must be able to define

Here’s an implementation of type-level insertion sort. One can see the strong similarity with the term-level insertion sort.

{-# LANGUAGE DataKinds #-}{-# LANGUAGE TypeFamilies #-}{-# LANGUAGE TypeOperators #-}{-# LANGUAGE UndecidableInstances #-}type family Sort xs whereSort'[] = '[]
Sort (x ': xs) = Insert x (Sort xs)type family Insert x xs whereInsert x '[] = x ':'[]Insert x (y ': ys) = Insert' (CmpNat x y) x y ys
type family Insert' b x y ys whereInsert''LT x y ys = x ': (y ': ys)Insert' _ x y ys = y ': Insert x ystypeL= [1, 3, 2, 4, 7, 9, 5]

In this simple scenario, converting a term-level function into a type-level function is almost mechanical. Just a few rules suffice.

sort -> type family Sort

[] -> ’[]

(x : xs) -> (x ’: xs)

compare -> CmpNat

We can evaluate Sort L using GHCi’s kind! command.

λ> :kind! Sort L
Sort L :: [Nat]
= '[1, 2, 3, 4, 5, 7, 9]

In this post, we will see how to write basic type-level functions using closed type families.

Before we start, let’s declare a bunch of GHC language extensions required to use type-level functions.

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

Also import required modules. GHC.TypeLits provides type-level natural numbers and symbols.

import GHC.TypeLitsimport Data.Proxy

Literals

Datatype promotion allows us to use True and False as type constructors whose kind is Bool. The quotes are used to emphasize the promotion, but can be omitted when syntactically unambiguous.

The definition of type-level function Length is the same as the value level length function. If it an empty list returns 0. If it not empty, add 1 to the length of the tail.

type family Length xs whereLength'[] = 0Length (x ': xs) = 1 + Length xs

0 and 1 are types of Nat kind and (+) is a type-level add function defined in GHC.TypeLits. We can even use (:) as a pattern here.

It seems Length is almost identical to the value level function length, but Length function is not kind-polymorphic by default. Thus passing [1, 2, 3] to Length causes an error.

λ> :kind! Length [1,2,3]
<interactive>:1:8: error:
• Expected kind ‘[*]’, but ‘'[1, 2, 3]’ has kind ‘[Nat]’
• In the first argument of ‘Length’, namely ‘'[1, 2, 3]’
In the type ‘Length '[1, 2, 3]’

To make it poly-kinded, we need to turn on PolyKind extension. The kind is inferred automatically, but we can also specify the kind with k.

type family Length (xs :: [k]) whereLength'[] = 0Length (x ': xs) = 1 + Length xs

Head and Tail are defined in a similar manner. Note that the kind of xs is explicitly annotated with [*] because they only work on type-level lists.

type family Head (xs :: [*]) whereHead (x ': xs) = xtype family Tail (xs :: [*]) whereTail (x ': xs) = xs

One notable thing here is that both Head and Tail are partially defined. What if we pass '[] to Head or Tail?

λ> :kind! Head '[]
Head '[] :: GHC.Types.*
= Head '[]

It seems GHC treats Head '[] as a valid type instead of emitting a type error. It is a bit mysterious, but at least we can see that type-level functions in Haskell can be partial and the behavior is not intuitive. Interested readers are referred to Richard Eisenberg’s What are type families? which discusses this issue in details.

Higher-order Type-level List Function

It is even possible to define type-level map function. Map takes a type-level function f and a type-level list xs. It applies f to every element of xs and returns a new type-level list containing the results.

type family Map (f ::*->*) (xs :: [*]) whereMap f '[] = '[]
Map f (x ': xs) = f x ':Map f xs

type family MakePair (x ::*) whereMakePair x = (x, x)

Wrap-up

So far we’ve covered only the basics of type-level datatypes and functions. Recent additions to GHC make it possible to explore the whole new world of dependent type programming in Haskell. Interested readers might want to take a look at the publications of Richard A. Eisenberg whose current work is to add dependent types to Haskell.