#### Type-level insertion sort

- January 30, 2017
Kwang's Haskell Blog - Type-level insertion sort

# Type-level insertion sort

Posted on January 30, 2017 by Kwang Yul Seo

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

1. naturals, booleans and lists
2. functions

in type-level. For the basics of type-level programming, readers are referred to Type-level functions using closed type families.

# Insertion sort

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 where
Sort '[] = '[]
Sort (x ': xs) = Insert x (Sort xs)

type family Insert x xs where
Insert x '[] = x ': '[]
Insert x (y ': ys) = Insert' (CmpNat x y) x y ys

type family Insert' b x y ys where
Insert' 'LT  x y ys = x ': (y ': ys)
Insert' _    x y ys = y ': Insert x ys

type L = [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]``````

#### Type-level functions using closed type families

- January 16, 2017
Kwang's Haskell Blog - Type-level functions using closed type families

# Type-level functions using closed type families

Posted on January 16, 2017 by Kwang Yul Seo

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.TypeLits
import 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.

``````λ> :set -XDataKinds
λ> :kind 'True
'True :: Bool
λ> :kind 'False
'False :: Bool``````

We can also use numbers such as `1` and `2` as types. The kind of these numbers is `Nat`.

``````λ> :kind 1
1 :: Nat``````

# Type-level Function

`If` takes three arguments `c`, `t` and `e` and returns `t` if `c` is `True`, returns `e` otherwise. The kind of `If` is `Bool -> * -> * -> *`.

``````type family If c t e where
If 'True  t e = t
If 'False t e = e``````

We can use GHCi’s `kind!` command to evaluate type functions.

``````λ> :kind! If 'True Bool Char
If 'True Bool Char :: *
= Bool
λ> :kind! If 'False Int Double
If 'False Int Double :: *
= Double``````

# Type-level List

As we can promote types like `Bool`, we can also promote lists and treat `[]` as a kind constructor, and `[]` and `(:)` as types.

When `(:)` is seen as a type constructor, it has kind

``````λ> :kind (:)
(:) :: a -> [a] -> [a]``````

It means `(:)` is kind-polymorphic.

So we can create a type-level list of booleans as well as naturals.

``````λ> :kind [True, False]
[True, False] :: [Bool]
λ> :kind [1, 2]
[1,2] :: [Nat]``````

# Type-level List Function

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 where
Length '[]       = 0
Length (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.

``````λ> :kind! Length [Char,Bool,Int]
Length [Char,Bool,Int] :: Nat
= 3``````

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]) where
Length '[]       = 0
Length (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 :: [*]) where
Head (x ': xs) = x

type family Tail (xs :: [*]) where
Tail (x ': xs) = xs``````

We can see `Head` and `Tail` work as expected.

``````λ> :kind! Head [Char, Bool, Int]
Head [Char, Bool, Int] :: *
= Char
*Main
λ> :kind! Tail [Char, Bool, Int]
Tail [Char, Bool, Int] :: [*]
= '[Bool, Int]``````

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

``````λ> :kind! 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 :: [*]) where
Map f '[]       = '[]
Map f (x ': xs) = f x ': Map f xs``````
``````λ> :kind! Map MakePair [Char,Bool,Int]
Map MakePair [Char,Bool,Int] :: [GHC.Types.*]
= '[(Char, Char), (Bool, Bool), (Int, Int)]``````

where the definition of `MakePair` is

``````type family MakePair (x :: *) where
MakePair 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.