Pretty much since they were introduced into GHC I’ve been meaning to try to port the *dimensional* library to use *Type Families* instead of *Functional Dependencies*. However, functional dependencies have served me quite well and I’ve been lacking the inspiration to dig into type families. That is, until I read the Leonidas’ *Statically Typed Vector Algebra Using Type Families*. Leonidas’ blog post resonated with me as the problem it addresses is related to one I myself have been interested in for some time (linear algebra with static guarantees). It also gave me a clear vision of how to apply type families to the fundamendal problem of dimensional – type level integers.

I’ve implemented the *numtype-tf* library which is in essence *numtype* using type families (hence the “-tf”) instead of functional dependencies. Some of my design decisions are slightly different (beside the choice of type system extension), e.g. the representation of negative integers is different and the `PosType`

and `NegType`

classes have been dropped in numtype-tf. The haddocks have also been improved a little.

A feature of the functionally dependent numtype that I was unable to reproduce with type families is ”mutual dependencies”, used in the `Sum`

and `Div`

type classes of numtype. Here is an example of type signatures (instances omitted) and ghci usage:

`> class Sum a b c | a b -> c, a c -> b, b c -> a`

> (+) :: (Sum a b c) => a -> b -> c

> (-) :: (Sum a b c) => c -> b -> a

```
\*Numeric.NumType> pos3 - pos5
NumType -2
```

To the best of my knowledge corresponding code with type families would be along the lines of:

`> type family Sum a b`

> (+) :: a -> b -> Sum a b

> (-) :: Sum a b -> b -> a

```
\*Numeric.NumType.TF> pos3 - pos5
<interactive>:1:1:
Couldn't match type `Sum a0 Pos5' with `S Pos2'
…
```

In order for the latter to compute we must assist the type checker by being explicit about the type of `a0`

, i.e. `pos3 - pos5 :: Neg2`

, which largely defeats the purpose of type level arithmetic. Instead two type families are used in numtype-tf:

`> type family Add a b -- a + b`

> (+) :: a -> b -> Add a b

> type family Sub a b -- a - b.

> (-) :: a -> b -> Sub a b

This works OK but the lack och mutual dependencies in type families restricts what I will losely refer to as “type inference back tracking”. This may or may not be a significant drawback compared to fundep numtype depending on the use case.

If you are interested in comparing code written with type families to code written with functional dependencies take a look at the respective modules on Github: Numeric.NumType.TF vs. Numeric.NumType.

The next step is to reimplement dimensional as *dimensional-tf* in order to exercise numtype-tf and better understand the impact of the differences with respect to numtype. I am also looking forward to playing with GHC.TypeNats in GHC 7.4.