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