Dimensional analysis with fundeps
Wed, 11 Apr 2001 10:54:14 -0700 (PDT)
Andrew Kennedy <email@example.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
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
anatoli (at, but not speaking for) ptc (dot) com
Do You Yahoo!?
Get email at your own domain with Yahoo! Mail.