Dimensional analysis with fundeps

[anatoli]

Hello everybody.

This is inspired by some recent threads in 
comp.lang.functional and comp.object.

It seems that fundeps are powerful enough to do
compile-time dimensional analysis in Haskell. That
is, one can devise types that represent dimensions of
quantities, such as (meter / second) or 
(kilogram * meter / second^2),
and have a complete set of type-correct operations on
such types.

Presented below is my rather crude attempt to devise
a proof-of-concept kind of "Dimension" module.

========== Dimension.lhs

> module Dimension where

Natural numbers expressed as Haskell types. Zero is 0.
If type a is Zero or positive, then (Succ a) is positive;
if type a is Zero or negative, then (Pred a) is negative.
This is very crude and should be replaced with sign-magnitude 
representation.

> data Zero
> data Succ n
> data Pred n

Natural number addition. Both operands are either positive, negative
or zero, so we consider 3*3=9 cases.

> class Add a b c | a b -> c

> instance Add Zero Zero Zero

> instance Add Zero (Succ b) (Succ b)
> instance Add Zero (Pred b) (Pred b)

> instance Add (Succ b) Zero (Succ b)
> instance Add (Pred b) Zero (Pred b)

> instance Add a b c => Add (Succ a) (Succ b) (Succ (Succ c))
> instance Add a b c => Add (Pred a) (Pred b) (Pred (Pred c))

> instance Add a b c => Add (Succ a) (Pred b) c
> instance Add a b c => Add (Pred a) (Succ b) c

Subtraction is very similar to addition.

> class Sub a b c | a b -> c

> instance Sub Zero Zero Zero

> instance Sub Zero (Succ b) (Pred b)
> instance Sub Zero (Pred b) (Succ b)

> instance Sub (Succ b) Zero (Succ b)
> instance Sub (Pred b) Zero (Pred b)

> instance Sub a b c => Sub (Succ a) (Succ b) c
> instance Sub a b c => Sub (Pred a) (Pred b) c

> instance Sub a b c => Sub (Succ a) (Pred b) (Succ (Succ c))
> instance Sub a b c => Sub (Pred a) (Succ b) (Pred (Pred c))

A Dimensioned type carries along exponents for three basic
dimensions: mass, length, and time. For simplicity we
restrict ourselves to SI units.

> newtype Dimensioned kg m s rep = Dimensioned rep

You can add only identically dimensioned quantities.

> plus, minus :: Num rep =>
>                Dimensioned kg m s rep ->
>                Dimensioned kg m s rep ->
>                Dimensioned kg m s rep
> plus  (Dimensioned x) (Dimensioned y) = Dimensioned (x+y)
> minus (Dimensioned x) (Dimensioned y) = Dimensioned (x-y)

You can multiply any two dimensioned quantities; exponents
from the operands add up in the result.

> times :: (Num rep,
>           Add kg kg' kg'',
>           Add m m' m'',
>           Add s s' s'') =>
>           Dimensioned kg m s rep ->
>           Dimensioned kg' m' s' rep ->
>           Dimensioned kg'' m'' s'' rep

> times (Dimensioned x) (Dimensioned y) = Dimensioned (x * y)

Similarly for division, except exponents are subtracted.

> divby :: (Fractional rep,
>           Sub kg kg' kg'',
>           Sub m m' m'',
>           Sub s s' s'') =>
>           Dimensioned kg m s rep ->
>           Dimensioned kg' m' s' rep ->
>           Dimensioned kg'' m'' s'' rep

> divby (Dimensioned x) (Dimensioned y) = Dimensioned (x / y)

Some handy abbreviations.

> type One = Succ Zero
> type Kg = Dimensioned One Zero Zero Double
> type Meter = Dimensioned Zero One Zero Double
> type Second = Dimensioned Zero Zero One Double
> type Unit = Dimensioned Zero Zero Zero Double

> dm x = Dimensioned x

> kg = (dm 1) :: Kg
> m  = (dm 1) :: Meter
> s  = (dm 1) :: Second
> u  = (dm 1) :: Unit

==== End of Dimension.lhs

So, now one can do this:

  (kg `times` m) `plus` (m `times` kg)

which has type

   Dimensioned (Succ Zero) (Succ Zero) Zero Double

but not this:

  kg `plus` (m `times` m)

The latter would produce a (rather cryptic, to be fair) type error:

ERROR - Constraints are not consistent with functional dependency
*** Constraint       : Add Zero Zero (Succ Zero)
*** And constraint   : Add Zero Zero Zero
*** For class        : Add a b c
*** Break dependency : b a -> c

There is a couple of things :) left to make this usable:

1) Define obvious classes and instances to make standard
   operations like (+) and (*) work intuitively. Unfortunately
   this means hiding standard Num and Fractional classes;

2) Make it work with rational (not just integer) exponents,
   so one can take square roots and the like.
   (Can one do GCD in this style, without resorting to
   undecidable and/or overlapping instances?);

3) Allow arbitrary user-defined "fundamental" dimensions
   (for things like dollars or radians) -- this may be
   very tricky;

4) Allow several unit systems (such as SI and Imperial)
   to coexist.

I've done most of these things in C++, and others did too,
so I guess there's some demand for such stuff. Even if
no one wants it, a nice example of what a powerful
type system can do is often handy in religious debates :)

-- 
anatoli t.

__________________________________________________
Do You Yahoo!?
Get email at your own domain with Yahoo! Mail. 
http://personal.mail.yahoo.com/