Dimensional analysis with fundeps
anatoli
anatoli@yahoo.com
Mon, 9 Apr 2001 09:36:45 -0700 (PDT)
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/