In an ongoing project, I’ve needed to do a bit of Haskell type-hackery with type functions implemented with type families. One thing I’ve needed is a type-heterogeneous sort — more than a type level sort, but a function that takes a value of one product type, and produces a value of a different, sorted product type. In doing so it needs to both sort the parameter type into a (potentially) different result type, as well as sort the parameter value into a result value (which of course needs to be of the result type). This works out to be a bit more complex than a pure type level sort (such as the quicksort implemented here, using funcitonal dependencies, or the merge sort implmenented here, again using functional dependencies), as Haskell type classes have to be used to select the right value-level functions to use for each step of the sort process. It was an interesting puzzle to solve — at least for me, as type level programming isn’t my strong point! (To make the problem a bit easier, I implemented a simpler, if less efficient, sorting algorithm, but quick sort or merge sort should also work at the type/value level).

Given a type for tagged values, e.g.

```
-- n is a phantom, type-level natural
newtype Tagged n t = Tagged t
```

And a product type, e.g.

```
data a :* b = a :* b
infixr 6 :*
```

I want to define tagged values such as:

```
tv0 :: Tagged N0 String
tv0 = Tagged "hello"
tv1 :: Tagged N1 Int
tv1 = Tagged 2
tv2 :: Tagged N2 Bool
tv2 = Tagged False
-- etc.
```

I want to be able to apply a function `sort`

to an arbitrary product of these types:

```
x = sort ( tv2 :* tv0 :* tv1 )
y = sort ( tv1 :* tv2 :* tv0 )
```

And the result should be the sorted product, i.e. `x == y && x == Tagged "hello" :* Tagged 2 :* Tagged False`

. Note that in the first application of sort, sort needs a type like:

```
sort :: (Tagged N2 Bool :* Tagged N0 String :* Tagged N1 Int) ->
(Tagged N0 String :* Tagged N1 Int :* Tagged N2 Bool)
```

and in the second, it needs:

```
sort :: (Tagged N1 Int :* Tagged N2 Bool :* Tagged N0 String) ->
(Tagged N0 String :* Tagged N1 Int :* Tagged N2 Bool)
```

It needs to work for arbitrarily long products of any Tagged type (with the constraint that the index `n`

must be a type-level natural). My solution to the problem follows.

```
> {-# LANGUAGE EmptyDataDecls, TypeFamilies, UndecidableInstances,
> ScopedTypeVariables, OverlappingInstances, TypeOperators,
> FlexibleInstances, NoMonomorphismRestriction #-}
> module TSort where
```

I started with the usual definition for type level naturals (with some convenient aliases for a few of them):

```
> data Zero
> data Succ n
```

```
> type N0 = Zero
> type N1 = Succ Zero
> type N2 = Succ N1
> type N3 = Succ N2
> type N4 = Succ N3
> type N5 = Succ N4
> type N6 = Succ N5
> type N7 = Succ N6
> type N8 = Succ N7
> type N9 = Succ N8
> type N10 = Succ N9
```

I also use type level booleans:

```
> data TRUE
> data FALSE
```

I need one inequality operator on naturals:

```
> type family LessThan m n
> type instance LessThan Zero Zero = FALSE
> type instance LessThan (Succ n) Zero = FALSE
> type instance LessThan Zero (Succ n) = TRUE
> type instance LessThan (Succ m) (Succ n) = LessThan m n
```

I need a type level if statement:

```
> type family Cond c t f
> type instance Cond TRUE t f = t
> type instance Cond FALSE t f = f
```

I need my tagged and product types:

```
> newtype Tagged n a = Tagged a deriving (Show,Eq)
```

```
> data a :* b = a :* b deriving (Show,Eq)
> infixr 6 :*
```

The general type of my sort is going to be something like (but not exactly):

` sort :: (Sortable a) => a -> Sorted a`

where `Sortable`

is a type class and `Sorted`

is a associated type of that type class. It didn’t work out to be quite that simple, but this is how I started thinking about the problem.

I envisioned the `Sortable`

class as:

```
class Sortable a where
type Sorted a
sort :: a -> Sorted a
```

Trying to create a simple instance of this type, for a pair of tagged values got me a bit bogged down:

```
instance Sortable (Tagged m a :* Tagged n b) where
type Sorted (Tagged m a :* Tagged n b) = ???
sort = ???
```

The type of `Sorted`

for this pair is conditional based on the value of the indices `m`

and `n`

, so I can write the type function like this:

```
type Sorted (Tagged m a :* Tagged n b) =
Cond (LessThan n m) -- if n < m
(Tagged n b :* Tagged m a) -- then swap
(Tagged m a :* Tagged n b) -- else don't
```

but how to write the `sort`

function? It can’t test the type and decide whether to swap the values. The key insight for solving this problem was that I needed some additional types to represent the operations I needed. For this simple reordering of a pair, I need two operations – *Swap*, to swap the elements of the pair if they are out of order, and *Id* (identity), to leave them alone if they are already in order:

```
data Swap x y = Swap x y
data Id a = Id a
```

Each of these can be seen as implementing a single step in a sorting algorithm). Each will be an instance of a `Sorter`

class:

```
> class Sorter a where
> type Sorted a
> type Unsorted a
```

`mkSort`

‘makes’ a sort function from (Unsorted a -> Sorted a) based on the type of its first argument, which is a proxy argument (its value is never examined).

```
> mkSort :: a -> Unsorted a -> Sorted a
```

The `Swap`

instance of `Sorter`

just swaps the values in a pair:

```
> instance Sorter (Swap x y) where
> type Sorted (Swap x y) = y :* x
> type Unsorted (Swap x y) = x :* y
> mkSort _ (x :* y) = y :* x
```

The `Id`

instance of `Sorter`

leaves its value alone:

```
> instance Sorter (Id a) where
> type Sorted (Id a) = a
> type Unsorted (Id a) = a
> mkSort _ v = v
```

Now my `Sortable`

class, instead of having a `sort`

function, needs instead a function to produce a sorter value:

```
> class Sortable a where
> type SorterType a
> sorter :: a -> SorterType a
```

And the sort can be written in terms of functions from the two classes:

```
> sort v = mkSort (sorter v) v
```

But still, how to implement the `sorter`

function for my pair of tagged elements?

```
> instance Sortable (Tagged m a :* Tagged n b) where
```

The type function for the `SorterType`

is now:

```
> type SorterType (Tagged m a :* Tagged n b) =
> Cond (LessThan n m)
> (Swap (Tagged m a) (Tagged n b))
> (Id (Tagged m a :* Tagged n b))
> sorter = undefined -- ???
```

As it turns out, the above implementation is sufficient. Since the `mkSort`

function doesn’t examine its first argument — it’s merely a proxy — the sorter function doesn’t need to produce a value. So `sorter`

can be left undefined — all its ‘work’ is done at compile time, in producing the right type such that the instance of ‘mkSort’ can be inferred (I have to admit, I discovered this accidentally while writing the sorting function. I left `sorter`

undefined because I couldn’t think of how to define it, then wrote `sort`

in terms of it, and accidentally ran it. It worked, my mind boggled, and then I figured out what what going on). Because no concrete *value* of either the `Id`

or `Swap`

types are ever needed, the actual definitions for these can be:

```
> data Id a
> data Swap a b
```

To sort something more than a pair, I need to be able to do more than just swap two types and values. A simple algorithm for sorting the product is to sort the ‘tail’ of the product, then insert the head of the product into the sorted tail (this is insertion sort — not the most efficient, but simpler than merge sort or quick sort). For this I need two more operations, a *sort-then-insert* operation, and an *insert* operation (the sort-then-insert operation sorts its ‘tail’ and then (if necessary) uses the insert operation to insert its head into the sorted tail). I need these operation types:

```
> data SortInsert h t
> data Insert x y
```

I need a new class similar to `Sortable`

, which has a `InserterType`

and a function to produce a `InserterType`

from the instance type:

```
> class Insertable a where
> type InserterType a
> inserter :: a -> InserterType a
```

A insertable assumes that its tail is sorted. For a product of tagged values (more than a pair), the `Insertable`

instance looks like this:

```
> instance Insertable (Tagged m a :* Tagged n b :* c) where
```

The `InserterType`

depends on whether the head element is less than the first element of the sorted tail. If it is, then the `InserterType`

is the identity, otherwise it is an `Insert x y`

:

```
> type InserterType (Tagged m a :* Tagged n b :* c) =
> Cond (LessThan n m)
> (Insert (Tagged m a) (Tagged n b :* c))
> (Id (Tagged m a :* Tagged n b :* c))
```

As in the `sorter`

function of a `Sortable`

, we don’t need the `inserter`

to do anything more than create a proxy argument:

```
> inserter = undefined
```

Inserting two elements is the same as sorting them:

```
> instance Insertable (Tagged m a :* Tagged n b) where
> type InserterType (Tagged m a :* Tagged n b) =
> Cond (LessThan n m) (Swap (Tagged m a) (Tagged n b))
> (Id (Tagged m a :* Tagged n b))
> inserter = undefined
```

A `Inserter`

is similar to a sorter: it takes an value of an `Uninserted`

type and produces a value of an `Inserted`

type:

```
> class Inserter a where
> type Inserted a
> type Uninserted a
```

`mkInsert`

‘makes’ a function `(Uninserted a -> Inserted a)`

from the instance type. The first argument again is just a proxy, it’s value never inspected:

```
> mkInsert :: a -> Uninserted a -> Inserted a
```

The identity instance is straightforward:

```
> instance Inserter (Id a) where
> type Inserted (Id a) = a
> type Uninserted (Id a) = a
> mkInsert _ v = v
```

The `Swap`

instance of `Inserter`

is essentially the same as the `Swap`

instance of `Sorter`

:

```
> instance Inserter (Swap a b) where
> type Inserted (Swap a b) = b :* a
> type Uninserted (Swap a b) = a :* b
> mkInsert _ (a :* b) = b :* a
```

The `Insert`

instance for a longer product has a rather convoluted context:

```
> instance (Insertable (a :* c)
> , Inserter (InserterType (a :* c))
> ,(a :* c) ~ Uninserted (InserterType (a :* c))
> ) => Inserter (Insert a (b :* c)) where
```

The `Inserted`

type is the first element of the tail followed by a inserted into the tail (via sort):

```
> type Inserted (Insert a (b :* c)) = b :* Inserted (InserterType (a :* c))
```

The uninserted type is simply the original (uninserted) product:

```
> type Uninserted (Insert a (b :* c)) = a :* b :* c
```

And the insert function effectively swaps the first two elements of the product and inserts the (new) tail:

```
> mkInsert _ (x :* y :* z) = y :* mkInsert (inserter $ x :* z) (x :* z)
```

The `Sorter`

instance for a `SortInsert`

that we need again has a convoluted context:

```
> instance (Sortable (b :* c)
> ,Unsorted (SorterType (b :* c)) ~ (b :* c)
> ,Uninserted (InserterType (a :* Sorted (SorterType (b :* c)))) ~
> (a :* Sorted (SorterType (b :* c)))
> ,Sorter (SorterType (b :* c))
> ,Insertable (a :* Sorted (SorterType (b :* c)))
> ,Inserter (InserterType (a :* Sorted (SorterType (b :* c))))
> ) =>
> Sorter (SortInsert a (b :* c)) where
```

The type of the output of the sort is the type of the output of the head of the product inserted with the sorted tail:

```
> type Sorted (SortInsert a (b :* c)) =
> Inserted (InserterType (a :* (Sorted (SorterType (b :* c)))))
```

The type of the input of the sort is the original (unsorted, uninserted) product:

```
> type Unsorted (SortInsert a (b :* c)) = a :* b :* c
```

And the sort function is just the insert of the head into the tail after the tail is sorted:

```
> mkSort _ (a :* b :* c) = mkInsert (inserter preinsert) preinsert
> where preinsert = a :* sort (b :* c)
```

Finally, the `Sortable`

instance for an arbitrary product is:

```
> instance (Sortable (b :* c), Sorter (SortInsert a (b :* c))) =>
> Sortable (a :* b :* c) where
> type SorterType (a :* b :* c) = SortInsert a (b :* c)
> sorter = undefined
```

Given some tagged values, I can try out the sort function:

```
> t0 :: Tagged N0 String
> t0 = Tagged "hello"
> t1 :: Tagged N1 Bool
> t1 = Tagged True
> t2 :: Tagged N2 Int
> t2 = Tagged 5
> t3 :: Tagged N3 String
> t3 = Tagged "goodbye"
```

```
*TSort1> sort (t2 :* t0 :* t1 :* t3)
Tagged "hello" :* (Tagged True :* (Tagged 5 :* Tagged "goodbye"))
*TSort1> sort (t3 :* t2 :* t1 :* t0)
Tagged "hello" :* (Tagged True :* (Tagged 5 :* Tagged "goodbye"))
*TSort1>
```

Beyond being an interesting puzzle to solve, there’s at least some use for such a function. For example, in a DSL that has operations that support named parameter association:

```
> rawConnect :: (Tagged N0 String :* Tagged N1 Int :* Tagged N2 String :*
> Tagged N3 String) -> IO ()
> rawConnect (Tagged host :* Tagged port :* Tagged user :* Tagged pass) =
> putStrLn $ "connecting to " ++ host ++ " on port " ++ show port ++
> " with username " ++ user ++ " and password " ++ pass
>
> connect = rawConnect . sort
>
> (=:) = ($)
> host :: String -> Tagged N0 String
> host = Tagged
> port :: Int -> Tagged N1 Int
> port = Tagged
> user :: String -> Tagged N2 String
> user = Tagged
> password :: String -> Tagged N3 String
> password = Tagged
```

Now you can invoke the ‘connect’ operation with parameters in no particular order:

```
> doit = do
> putStrLn "trying to connect!"
> connect ( user =: "admin" :*
> password =: "pa55w0rd" :*
> port =: 22 :*
> host =: "example.com" )
> putStrLn "connected!"
```

… which is at least mildly cool, for certain definitions of cool.

*Brought to you by BlogLiterately with generous support from pandoc, hscolour and viewers like you.*

[…] level strings. It is implemented with generous support from type families (to implement things like type/value heterogeneous list sorting), Template Haskell, Quasi Quotation, and other non-standard features too numerous to mention. […]

Pingback by Wreckage 0.0.0 « No tengo la menor idea — 2010-05-10 @ 19:58