ANNOUNCE: dimensional-tf-0.10 – Statically checked physical dimensions with type families

As promised when I released numtype-tf in January I have now also created the dimensional-tf library – a conversion of the dimensional library to use Type Families instead of Functional Dependencies.

I skipped the experimental and to my knowledge unused CGS and Extensible modules. If you would like to see them ported let me know.

For straight-forward usage, e.g. the examples on the dimensional wiki, the only change required from library users to switch from dimensional to dimensional-tf is inserting .TF in the import statements. E.g.:

import Numeric.Units.Dimensional.TF.Prelude
import Numeric.Units.Dimensional.TF.NonSI

In such cases the choice of using dimensional backed by functional dependencies or type families is largely philosophical as neither will be visible in the client code.

If you do more advanced things with polymorphic dimensions and explicit type signatures you will have to convert the type signatures from MLTC style constraints to type families. E.g.:

myFunc :: (Num a, Mul d1 d2 d3) => Quantity d1 a -> Quantity d2 a -> Quantity d3 a

would change to:

myFunc :: Num a => Quantity d1 a -> Quantity d2 a -> Quantity (Mul d1 d2) a

Compiler errors will also be different in dimensional-tf, for better or for worse.

So, should you use dimensional or dimensional-tf? For the time being I consider dimensional-tf to be experimental. If you want stability stick with dimensional for now. If your dislike of functional dependencies trumps your need for stability, then try dimensional-tf. If dimensional-tf eventually proves itself to be a better dimensional I will merge it into the latter with a major version bump.

Dimensional-tf-0.1 compiles on GHC-7.0. The source code is on Github.

Update 2012-02-15: In case this wasn't building for you on GHC-7.4.1; I've added a FlexibleInstances pragma that should take care of it. Dimensional-tf-0.1.0.1 compiles on GHC-7.0 and 7.4.

Type level integers with Type Families (numtype-tf 0.1)

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.