Typing units correctly

[Dylan Thurston]

--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--