Dimensional analysis with fundeps

[anatoli]

Andrew Kennedy <akenn@microsoft.com> wrote:
> You shouldn't need rational exponents to take square roots as long as no
> *ground* type requires them.

Rational exponents for ground types are not strictly required 
but sometimes very convenient. I'm not a physicist, but a web
search for "sqrt(hz)" turns up a lot of pages. This is apparently
a component of some unit of sensitivity and/or noise level. For 
instance, sensitivity of an amplifier would be measured in Volt/sqrt(Hz)
which is the same as Volt*sqrt(second).

> In your encoding, is the following a valid type?
> 
>   sqrt :: (Num rep, Add kg kg kg', Add m m m', Add s s s') => 
>     Dimensioned kg' m' s' rep -> Dimensioned kg m s rep
> 
> Or have I misunderstood multi-parameter classes with functional
> dependencies?

It is valid but not very useful: if the type of (sqrt x) is known
then the type of x can be deduced, but not the other way around, because
of the direction of dependencies.

Typically we want it the other way around, and preferrably both ways:

  class Half a b | a->b, b->a
  instance Half Zero Zero
  instance Half x y => Half (Succ (Succ x)) (Succ y)

  sqrt :: (Half kg kg', Half m m', Half s s') => 
    Dimensioned kg m s rep -> Dimensioned kg' m' s' rep

Sigh. I guess that with dependent types some things are a lot
easier.

-- 
anatoli (at, but not speaking for) ptc (dot) com

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