Typing units correctly
Dylan Thurston
dpt@math.harvard.edu
Wed, 14 Feb 2001 14:14:36 -0500
--opJtzjQTFsWo+cga
Content-Type: text/plain; charset=us-ascii
Content-Disposition: inline
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
--opJtzjQTFsWo+cga
Content-Type: text/plain; charset=us-ascii
Content-Disposition: attachment; filename="dim3.hs"
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
--opJtzjQTFsWo+cga--