Re: Typing units correctly
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
___
Haskell-Cafe mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell-cafe
RE: Typing units correctly
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:[EMAIL PROTECTED]]
> Sent: Wednesday, February 14, 2001 7:15 PM
> To: Andrew Kennedy; [EMAIL PROTECTED]
> 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
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 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
RE: Typing units correctly
To be frank, the poster that you cite doesn't know what he's talking about. He makes two elementary mistakes: (a) attempting to encode dimension/unit checking in an existing type system; (b) not appreciating the need for parametric polymorphism over dimensions/units. 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. Furthermore, parametric polymorphism is essential for code reuse - one can't even write a generic squaring function (say) without it. Best to ignore the poster and instead read the papers that contributors to this thread have cited :-) 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. - Andrew Kennedy. > -Original Message- > From: [EMAIL PROTECTED] > [mailto:[EMAIL PROTECTED]] > Sent: Wednesday, February 14, 2001 5:02 PM > To: [EMAIL PROTECTED] > Subject: Re: Typing units correctly > > > > Hi, > > I don't know if this is useful, but in response to a link to that > article that I posted on Lambda, someone posted a link arguing that > such an approach (at least in Ada) was impractical. To be honest, I > don't find it very convincing, but I haven't been following this > discussion in detail. It might raise some problems you have not > considered. > > Anyway, if you are interested, it's all at > http://lambda.weblogs.com/discuss/msgReader$818 > > Apologies if it's irrelevant or you've already seen it, > Andrew > > On Mon, Feb 12, 2001 at 01:51:54PM -0500, Dylan Thurston wrote: > [...] > > The papers I could find (e.g., > > http://citeseer.nj.nec.com/kennedy94dimension.html, > "Dimension Types") > > mention extensions to ML. I wonder if it is possible to work within > > the Haskell type system, which is richer than ML's type system. > [...] > > -- > http://www.andrewcooke.free-online.co.uk/index.html > ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: Typing units correctly
Hi, I don't know if this is useful, but in response to a link to that article that I posted on Lambda, someone posted a link arguing that such an approach (at least in Ada) was impractical. To be honest, I don't find it very convincing, but I haven't been following this discussion in detail. It might raise some problems you have not considered. Anyway, if you are interested, it's all at http://lambda.weblogs.com/discuss/msgReader$818 Apologies if it's irrelevant or you've already seen it, Andrew On Mon, Feb 12, 2001 at 01:51:54PM -0500, Dylan Thurston wrote: [...] > The papers I could find (e.g., > http://citeseer.nj.nec.com/kennedy94dimension.html, "Dimension Types") > mention extensions to ML. I wonder if it is possible to work within > the Haskell type system, which is richer than ML's type system. [...] -- http://www.andrewcooke.free-online.co.uk/index.html ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: Typing units correctly
Tom Pledger writes: In both of those cases, the apparent non-integer dimension is accompanied by a particular unit (km, V). So, could they equally well be handled by stripping away the units and exponentiating a dimensionless number? For example: (x / 1V) ^ y I think not. The "Dimension Types" paper really is excellent, and makes the distinction between the necessity of exponents on the dimensions and the exponents on the numbers very clear; I commend it to everyone in this discussion. The two things (a number of "square root volts" and a "number of volts to an exponent" are different things, unless you are simply trying to represent a ground number as an expression! Dave Barton <*> [EMAIL PROTECTED] )0( http://www.averstar.com/~dlb ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
Typing units correctly
Dylan Thurston writes: | Any such system would probably not be able to type (^), since the | output type depends on the exponent. I think that is acceptable. In other words, the first argument to (^) would have to be dimensionless? I agree. So would the arguments to trig functions, etc. Ashley Yakeley writes: | Very occasionally non-integer or 'fractal' exponents of dimensions | are useful. For instance, geographic coastlines can be measured in | km ^ n, where 1 <= n < 2. This doesn't stop the CIA world factbook | listing all coastline lengths in straight kilometres, however. David Barton writes: | Even without fractals, there are cases where weird dimensions come | up (I ran across this in my old MHDL (microwave) days). Square | root volts is the example that was constantly thrown in my face. In both of those cases, the apparent non-integer dimension is accompanied by a particular unit (km, V). So, could they equally well be handled by stripping away the units and exponentiating a dimensionless number? For example: (x / 1V) ^ y Regards, Tom ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
Typing units correctly
On Mon, Feb 12, 2001 at 10:08:02AM +0100, Bjorn Lisper wrote: > >The main complication is that the type system needs to deal with > >integer exponents of dimensions, if it's to do the job well. > Andrew Kennedy has basically solved this for higher order languages with HM > type inference. He made an extension of the ML type system with dimensional > analysis a couple of years back. Sorry I don't have the references at hand > but he had a paper in ESOP I think. The papers I could find (e.g., http://citeseer.nj.nec.com/kennedy94dimension.html, "Dimension Types") mention extensions to ML. I wonder if it is possible to work within the Haskell type system, which is richer than ML's type system. The main problem I see is that the dimensions should commute: Length * Time = Time * Length. I can't think of how to represent Length, Time, and * as types, type constructors, or whatnot so that that would be true. You could put in functions to explicitly do the conversion, but that obviously gets impractical. Any such system would probably not be able to type (^), since the output type depends on the exponent. I think that is acceptable. I think you would also need a finer-grained heirarchy in the Prelude (including than in my proposal) to get this to work. > It would be quite interesting to have a version of Haskell that would allow > the specification of differential equations, so one could make use of all > the good features of Haskell for this. This would allow the unified > specification of systems that consist both of physical and computational > components. This niche is now being filled by a mix of special-purpose > modeling languages like Modelica and Matlab/Simulink for the physical part, > and SDL and UML for control parts. The result is likely to be a mess, in > particular when these specifications are to be combined into full system > descriptions. My hope is that you wouldn't need a special version of Haskell. Best, Dylan Thurston ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
