RE: Dimensional analysis with fundeps
You shouldn't need rational exponents to take square roots as long as no *ground* type requires them. If polymorphism over units were primitive, then we'd have something like sqrt :: Real (u.u) -> Real u for a fixed numeric type Real that's parameterized over its units. (BTW, it's not possible to define such a function in the language using, say, only standard arithmetic operators and comparison; you have to build it in instead). 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? - Andrew.
-----Original Message----- From: anatoli [mailto:anatoli@yahoo.com] Sent: Monday, April 09, 2001 5:37 PM To: haskell@haskell.org Subject: Dimensional analysis with fundeps
There is a couple of things :) left to make this usable:
...
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?);
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/
participants (2)
-
anatoli -
Andrew Kennedy