Typing units correctly

[Andrew Kennedy]

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:dpt@math.harvard.edu]
> Sent: Wednesday, February 14, 2001 7:15 PM
> To: Andrew Kennedy; haskell-cafe@haskell.org
> 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 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
>