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