Typing units correctly
Dylan Thurston
dpt@math.harvard.edu
Mon, 19 Feb 2001 16:05:01 -0500
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