Typing units correctly

[Dylan Thurston]

On Thu, Feb 15, 2001 at 07:18:14AM -0800, Andrew Kennedy wrote:
> First, I think there's been a misunderstanding. I was referring to 
> the poster ("Christoph Grein") ... but from 
> what I've seen your (Dylan's) posts are well-informed. Sorry if 
> there was any confusion.

It was easy to get confused, since I was quite clueless in the post in
question.  No big deal.

> As you suspect, negative exponents are necessary.

On a recent plane ride, I convinced myself that negative exponents are
possible to provide along the same lines, although it's not very
elegant: addition seems to require 13 separate cases, depending on the
sign of each term, with the representation I picked.

There are other representations.  There is a binary representation,
similar to Chris Okasaki's in the square matrices paper.

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

Great.  I'll look it up.  I had run across similar problems in an
unrelated context recently.

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

One point of view is that anything you can do inconveniently by hand,
as with the Peano integers example I posted, you ought to be able to
do conveniently with good language support.  I think you can do a lot
of these constraint-based systems using PeanoAdd; I may try
programming some.  Language support does have advantages here: type
signatures can often be simplified considerably, and can often be
shown to be inconsistent.

For instance,
   a <= b, a <= b+1
can be simplified to
  a <= b
while
  (PeanoLessEqual a b, PeanoLessEqual a (Succ b))
which means more or less the same thing, cannot be simplified to
  (PeanoLessEqual a b)
though probably a function could be written that converts between the
two; but I don't see how to make it polymorphic enough.

Your dimension types and Boolean algebra do add something really new
that cannot be simulated like this: type inference and principal
types.  I wonder how they can be incorporated into Haskell in some
reasonable and general way.  Is a single kind of "dimensions" the
right thing?  What if, e.g., I care about the distinction between
rational and integral exponents, or I want Z/2 torsion?  How do I
create a new dimension?  Is there some function that creates a
dimension from a string or some such?  What is its type?  Can I
prevent dimensions from unrelated parts of the program from
interfering?

Best,
	Dylan Thurston