RE: Typing units correctly
First, I think there's been a misunderstanding. I was referring to
the poster ("Christoph Grein") of
http://www.adapower.com/lang/dimension.html
when I said that "he doesn't know what he's talking about". I've
not been following the haskell cafe thread very closely, but from
what I've seen your (Dylan's) posts are well-informed. Sorry if
there was any confusion.
As you suspect, negative exponents are necessary. How else would you
give a polymorphic type to
\ x - 1.0/x
?
However, because of the equivalence on type schemes that's not just
alpha-conversion, many types can be rewritten to avoid negative
exponents, though I don't think that this is particularly desirable.
For example the type of division can be written
/ :: Real (u.v) - Real u - Real v
or
/ :: Real u - Real v - Real (u.v^-1)
where u and v are "unit" variables.
In fact, I have since solved the simplification problem mentioned
in my ESOP paper, and it would assign the second of these two
(equivalent) types, as it works from left to right in the type. I
guess it does boil down to choosing a nice basis; more precisely
it corresponds to the Hermite Normal Form from the theory of
integer matrices (more generally: modules over commutative rings).
For more detail see my thesis, available from
http://research.microsoft.com/users/akenn/papers/index.html
By the way, type system pathologists might be interested to know
that the algorithm described in ESOP'94 doesn't actually work
without an additional step in the rule for let (he says shamefacedly).
Again all this is described in my thesis - but for a clearer explanation
of this issue you might want to take a look at my technical report
"Type Inference and Equational Theories".
Which brings me to your last point: some more general system that
subsumes the rather specific dimension/unit types system. There's been
some nice work by Martin Sulzmann et al on constraint based systems
which can express dimensions. See
http://www.cs.mu.oz.au/~sulzmann/
for more details. To my taste, though, unless you want to express all
sorts of other stuff in the type system, the equational-unification-based
approach that I described in ESOP is simpler, even with the fix for let.
I've been promising for years that I'd write up a journal-quality (and
correct!) version of my ESOP paper including all the relevant material
from my thesis. As I have now gone so far as to promise my boss that I'll
do such a thing, perhaps it will happen :-)
- Andrew.
-Original Message-
From: Dylan Thurston [mailto:[EMAIL PROTECTED]]
Sent: Wednesday, February 14, 2001 7:15 PM
To: Andrew Kennedy; [EMAIL PROTECTED]
Subject: Re: Typing units correctly
On Wed, Feb 14, 2001 at 08:10:39AM -0800, Andrew Kennedy wrote:
To be frank, the poster that you cite doesn't know what he's talking
about. He makes two elementary mistakes:
Quite right, I didn't know what I was talking about. I still don't.
But I do hope to learn.
(a) attempting to encode dimension/unit checking in an existing type
system;
We're probably thinking about different contexts, but please see the
attached file (below) for a partial solution. I used Hugs' dependent
types to get type inference. This makes me uneasy, because I know that
Hugs' instance checking is, in general, not decidable; I don't know if
the fragment I use is decidable. You can remove the dependent types,
but then you need to type all the results, etc., explicitly. This
version doesn't handle negative exponents; perhaps what you say here:
As others have pointed out, (a) doesn't work because the algebra of
units of measure is not free - units form an Abelian group (if
integer exponents are used) or a vector space over the rationals (if
rational exponents are used) and so it's not possible to do
unit-checking by equality-on-syntax or unit-inference by ordinary
syntactic unification. ...
is that I won't be able to do it?
Note that I didn't write it out, but this version can accomodate
multiple units of measure.
(b) not appreciating the need for parametric polymorphism over
dimensions/units.
... Furthermore, parametric polymorphism is
essential for code reuse - one can't even write a generic squaring
function (say) without it.
I'm not sure what you're getting at here; I can easily write a
squaring function in the version I wrote. It uses ad-hoc polymorphism
rather than parametric polymorphism. It also gives much uglier
types; e.g., the example from your paper
f (x,y,z) = x*x + y*y*y + z*z*z*z*z
gets some horribly ugly context:
f :: (Additive a, Mul b c d, Mul c c e, Mul e c b, Mul d c a,
Mul f f a, Mul g h a, Mul h h g) = (f,h,c) - a
Not that I recommend this solution, mind you. I think language
support would be much better. But specific language support for units
rubs me the wrong way: I'd much rather see a general notion of types
with
Re: Typing units correctly
On Wed, Feb 14, 2001 at 08:10:39AM -0800, Andrew Kennedy wrote: To be frank, the poster that you cite doesn't know what he's talking about. He makes two elementary mistakes: Quite right, I didn't know what I was talking about. I still don't. But I do hope to learn. (a) attempting to encode dimension/unit checking in an existing type system; We're probably thinking about different contexts, but please see the attached file (below) for a partial solution. I used Hugs' dependent types to get type inference. This makes me uneasy, because I know that Hugs' instance checking is, in general, not decidable; I don't know if the fragment I use is decidable. You can remove the dependent types, but then you need to type all the results, etc., explicitly. This version doesn't handle negative exponents; perhaps what you say here: As others have pointed out, (a) doesn't work because the algebra of units of measure is not free - units form an Abelian group (if integer exponents are used) or a vector space over the rationals (if rational exponents are used) and so it's not possible to do unit-checking by equality-on-syntax or unit-inference by ordinary syntactic unification. ... is that I won't be able to do it? Note that I didn't write it out, but this version can accomodate multiple units of measure. (b) not appreciating the need for parametric polymorphism over dimensions/units. ... Furthermore, parametric polymorphism is essential for code reuse - one can't even write a generic squaring function (say) without it. I'm not sure what you're getting at here; I can easily write a squaring function in the version I wrote. It uses ad-hoc polymorphism rather than parametric polymorphism. It also gives much uglier types; e.g., the example from your paper f (x,y,z) = x*x + y*y*y + z*z*z*z*z gets some horribly ugly context: f :: (Additive a, Mul b c d, Mul c c e, Mul e c b, Mul d c a, Mul f f a, Mul g h a, Mul h h g) = (f,h,c) - a Not that I recommend this solution, mind you. I think language support would be much better. But specific language support for units rubs me the wrong way: I'd much rather see a general notion of types with integer parameters, which you're allowed to add. This would be useful in any number of places. Is this what you're suggesting below? To turn to the original question, I did once give a moment's thought to the combination of type classes and types for units-of-measure. I don't think there's any particular problem: units (or dimensions) are a new "sort" or "kind", just as "row" is in various proposals for record polymorphism in Haskell. As long as this is tracked through the type system, everything should work out fine. Of course, I may have missed something, in which case I'd be very interested to know about it. Incidentally, I went and read your paper just now. Very interesting. You mentioned one problem came up that sounds interesting: to give a nice member of the equivalence class of the principal type. This boils down to picking a nice basis for a free Abelian group with a few distinguished elements. Has any progress been made on that? Best, Dylan Thurston module Dim3 where default (Double) infixl 7 *** infixl 6 +++ data Zero = Zero data Succ x = Succ x class Peano a where value :: a - Int element :: a instance Peano Zero where value Zero = 0 ; element = Zero instance (Peano a) = Peano (Succ a) where value (Succ x) = value x + 1 ; element = Succ element class (Peano a, Peano b, Peano c) = PeanoAdd a b c | a b - c instance (Peano a) = PeanoAdd Zero a a instance (PeanoAdd a b c) = PeanoAdd (Succ a) b (Succ c) data (Peano a) = Dim a b = Dim a b deriving (Eq) class Mul a b c | a b - c where (***) :: a - b - c instance Mul Double Double Double where (***) = (*) instance (Mul a b c, PeanoAdd d e f) = Mul (Dim d a) (Dim e b) (Dim f c) where (Dim _ a) *** (Dim _ b) = Dim element (a *** b) instance (Show a, Peano b) = Show (Dim b a) where show (Dim b a) = show a ++ " d^" ++ show (value b) class Additive a where (+++) :: a - a - a zero :: a instance Additive Double where (+++) = (+) ; zero = 0 instance (Peano a, Additive b) = Additive (Dim a b) where Dim a b +++ Dim c d = Dim a (b+++d) zero = Dim element zero scalar :: Double - Dim Zero Double scalar x = Dim Zero x unit = scalar 1.0 d = Dim (Succ Zero) 1.0 f (x,y,z) = x***x +++ y***y***y +++ z***z***z***z***z
Re: Typing units correctly
Tom Pledger writes: In both of those cases, the apparent non-integer dimension is accompanied by a particular unit (km, V). So, could they equally well be handled by stripping away the units and exponentiating a dimensionless number? For example: (x / 1V) ^ y I think not. The "Dimension Types" paper really is excellent, and makes the distinction between the necessity of exponents on the dimensions and the exponents on the numbers very clear; I commend it to everyone in this discussion. The two things (a number of "square root volts" and a "number of volts to an exponent" are different things, unless you are simply trying to represent a ground number as an expression! Dave Barton * [EMAIL PROTECTED] )0( http://www.averstar.com/~dlb ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
