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/