Re: Units of measure
On Aug 26, 18:34, Christian Sievers wrote: > Is there any sense physically in rational exponents? It depends on unit system. SI wants electric charge to be fundamental (and Coulomb's constant is derived from it), while CGS assumes Coulomb's constant = 1 and charge is derived: Charge ^ 2Mass * Length (Mass * Length ^ 3) ^ 1/2 -- = - => Charge = - Length ^ 2Time ^2 Time -- Anatoli Tubman <[EMAIL PROTECTED]> - opinions aren't
Re: Units of measure
Thanks for all the replies.
I'm nervous about fixing the arity of Unit, in any language used for
commercial applications.
Herbert Graeber writes:
> [...]
>
> Using C++, one can define templates for proper handling of units without
> additional language extensions:
>
> template
> class Unit {
> ...
> };
>
> [...]
Christian Sievers writes:
> [...]
>
> > sqrt :: (m::Int) |-> (l::Int) |-> (t::Int) |->
> >Unit (2*m) (2*l) (2*t) -> Unit m l t
>
> [...]
The S.I. units are stable. However, currency units benefit from the
same treatment, with each currency as a separate dimension (assuming
that compilers should not be exchange rate aware), and a commercial
application may need to deal with any number of currencies.
Then, there's the issue of letting the end users define additional
currencies at run time. I see a couple of ways to deal with this:
1. Don't attempt to type-check currency at compile time. Fix the
arity of Unit after all, if that helps with anything.
2. Deem the currency-defining task to be programming, not a true end
user activity. Deem your application's configuration parameters
to be a programming language.
Regards,
Tom
Re: Units of measure
> > (Cayenne doesn't happen to have c*n-patterns?) [ ;-) forgotten.] > `c*n' and `n+k' are equally abominable. Cayenne has neither. I thought they might be nice to express the type of sqrt. When we have the type as > Unit (mass::Int) (length::Int) (time::Int) = Double it should be s.th. like Unit (2*m) (2*l) (2*t) -> Unit m l t. Now I realized that the type does indeed nearly look like that, but without using any doubtful pattern matching features: > sqrt :: (m::Int) |-> (l::Int) |-> (t::Int) |-> >Unit (2*m) (2*l) (2*t) -> Unit m l t (Will hidden arguments work in this case?) I really like Cayenne. All the best, Christian Sievers
Re: Units of measure
Christian Sievers wrote: > Anatoli Tubman wrote: > > > I once wrote a C++ template library that did exactly that. Arbitrary units, > > rational exponents -- you can have (m^(3/2)/kg^(5/16)) dimensioned value. > > All at compile time, without runtime checking whatsoever. > > Is there any sense physically in rational exponents? > If not, we could use this extra information for less permissive type > checking, for example only allowing a square root from an argument > that has only even exponents. > (Cayenne doesn't happen to have c*n-patterns?) `c*n' and `n+k' are equally abominable. Cayenne has neither. -- -- Lennart
Units of measure
Hi. Here's a short question which has been bothering me, and a longer
discussion of why. Apologies if it's a rote.
Where do units of measure fit into a type system?
Expressions along these lines should ideally be legal:
(x :: Metres) / (y :: Seconds)
(x :: Pounds_sterling_per_kilowatt_hour) * (y :: kilowatt_hours)
...and there's something to be said for supporting the addition of a
number of feet to a number of metres,
...but this should ideally be rejected by the compiler:
(x :: Metres) + (y :: Seconds)
It's tempting to use the type system, but then it runs into these two
problems (at least):
- There are infinitely many derivable units of measure. At what
point do you stop defining them singly and statically?
- There's a slew of (*) and (/) overloadings, none of which are fit
to be written by hand.
If a set of units is declared elsewhere than in your program, what
happens when another currency becomes of concern?
Could every numeric expression be accompanied by a set - inferred
where possible - of (unit, nonzero exponent) pairs? For example,
could a force expression have {(kg, 1), (m, 1), (s, -2)} as part of
its type?
Regards,
Tom
Re: Units of measure
Anatoli Tubman wrote: > I once wrote a C++ template library that did exactly that. Arbitrary units, > rational exponents -- you can have (m^(3/2)/kg^(5/16)) dimensioned value. > All at compile time, without runtime checking whatsoever. Is there any sense physically in rational exponents? If not, we could use this extra information for less permissive type checking, for example only allowing a square root from an argument that has only even exponents. (Cayenne doesn't happen to have c*n-patterns?) Christian Sievers
Re: Units of measure
> Good idea. Andrew Kennedy wrote a whole thesis about this, and a
> paper or two besides.
>
> http://research.microsoft.com/~akenn/
Unfortunalty this work concentrates on extending a programming language
with units. It would be better to extend Haskell with more universal
features that makes the implementation of a library for units of measure
possible.
Using C++, one can define templates for proper handling of units without
additional language extensions:
template
class Unit {
...
};
template
Unit operator * (Unit value1, Unit
value2) {
...
}
.. and so on ...
typedef Unit<1,0> Distance;
typedef Unit<0,1> Time;
typedef Unit<1,-1> Speed;
.. and so on ...
Here the template parameters l and t represent the exponents of length
and time.
The important thing here is that template classes can be parameterized
with values that can be enumerated (ints and enums) and not only with
types like in Haskell. Additionally it is possible to do computations
with these values at compile time.
Herbert
Re: Units of measure
On Thu, 26 Aug 1999, Christian Sievers wrote: > Anatoli Tubman wrote: > > > I once wrote a C++ template library that did exactly that. Arbitrary > > units, rational exponents -- you can have (m^(3/2)/kg^(5/16)) > > dimensioned value. All at compile time, without runtime checking > > whatsoever. > > Is there any sense physically in rational exponents? Physically? Probably not much, other than if you get them, you might have made a dimensional error (which could be caught, as you suggest below). Well...actually, I take a bit of that back. There are occasional "rules of thumb" that relate various physical quantities in "natural" situations. So, for example, the speed of a fish is more or less proportional to the square root of its length (assuming fish of some reasonably "fishy" shape). Other situations come up with "real" data where you're doing a regression analysis (or something similar) and the limitations of the technique require a data transformation in order for to you fulfill statistical model assumptions. Not a pleasant business... But in both cases it's not clear how (or that) you want to enforce dimensional correctness. > If not, we could use this extra information for less permissive type > checking, for example only allowing a square root from an argument > that has only even exponents. And I can see that logarithmic data transformations are really going to shake your world view. :-) But getting back to Haskell (or functional programming), I did take a look at the suggested Kennedy papers on "Dimension Types". Boy, does this problem turn out to be subtle; I was in over my head in no time. But, in addition to the solution he proposes there (which, by the way, would handle the square root problem you mention), he discusses Wand and O'Keefe's attempt to do a similar thing with an ML-like type system. This is not as general, but might be good enough for some purposes. What you do there is fix the number of base dimension at N and express dimension types as N-tuples, so that if you had dimensions M, L, and T, then Q (n1,n2,n3) represents [M^n1 L^n2 T^n3] in dimensional speak. The "fun" here begins with things like sqrt which can have type Q (n1, n2, n3) -> Q (.5*n1, .5*n2, .5*n3). Oh, and the type inference algorithm requires Gaussian elimination. jking
Re: Units of measure
Not sure it will work... how do you handle Quot (Prod Metres Metres) (Prod Seconds Metres) or make sure that Prod Metres Seconds is the same as Prod Seconds Metres ??? On Aug 26, 10:36, Andreas Rossberg wrote: > Subject: Re: Units of measure > Tom Pledger wrote: > > > > Where do units of measure fit into a type system? > > In Haskell this should be quite easy. Off my head I would suggest > something like > > class Unit a where > unit :: Float -> a > value :: a -> Float > > newtype Metres = Metres Float > newtype Seconds = Seconds Float > > instance Unit Metres where > unit = Metres > value(Metres x) = x > instance Unit Seconds where > unit = Seconds > value(Seconds x) = x > > newtype Prod a b = Prod Float > newtype Quot a b = Quot Float > -- Anatoli Tubman <[EMAIL PROTECTED]> - opinions aren't
Re: Units of measure
"D. Tweed" wrote: > > Isn't the issue a bit weirder than this in that you've also got pure > numbers which ought be usable with the same operators (*$,etc) You are right, I overlooked that. But this is not even the most serious problem, overloading the operators accordingly might be possible with MPTCs, I think. The hard problem is that you cannot establish equalities like Prod a (Quot b a) = b Sigh. - Andreas -- Andreas Rossberg, [EMAIL PROTECTED] :: be declarative. be functional. just be. ::
Re: Units of measure
I once wrote a C++ template library that did exactly that. Arbitrary units, rational exponents -- you can have (m^(3/2)/kg^(5/16)) dimensioned value. All at compile time, without runtime checking whatsoever. Too bad it took eternity to compile a simplest program. Things like that should be built-in right into the language, or at least easy to implement. It would be very nice if Haskell could support this. Hmmm...I think one can do it in Cayenne. Any experts? On Aug 26, 18:56, Tom Pledger wrote: > Subject: Units of measure > Hi. Here's a short question which has been bothering me, and a longer > discussion of why. Apologies if it's a rote. > > Where do units of measure fit into a type system? > -- Anatoli Tubman <[EMAIL PROTECTED]> - opinions aren't
Re: Units of measure
On Thu, 26 Aug 1999, Andreas Rossberg wrote: > Tom Pledger wrote: > > > > Where do units of measure fit into a type system? > > In Haskell this should be quite easy. Off my head I would suggest > something like [snip] > instance (Unit a, Unit b) => Unit(Prod a b) where > unit = Prod > value(Prod x) = x > instance (Unit a, Unit b) => Unit(Quot a b) where > unit = Quot > value(Quot x) = x [snip] Isn't the issue a bit weirder than this in that you've also got pure numbers which ought be usable with the same operators (*$,etc) (so that you don't have to worry as you write the program) but which don't affect the `unit type' of the thing to which they're applied? (If they don't vanish you'll get counter-intuitive things like a +$ a has a different type to 2 *$ a ) ___cheers,_dave__ email: [EMAIL PROTECTED] "He'd stay up all night inventing an www.cs.bris.ac.uk/~tweed/pi.htm alarm clock to ensure he woke early work tel: (0117) 954-5253 the next morning"-- Terry Pratchett
Re: Units of measure
Tom Pledger wrote: > > Where do units of measure fit into a type system? In Haskell this should be quite easy. Off my head I would suggest something like class Unit a where unit :: Float -> a value :: a -> Float newtype Metres = Metres Float newtype Seconds = Seconds Float instance Unit Metres where unit = Metres value(Metres x) = x instance Unit Seconds where unit = Seconds value(Seconds x) = x newtype Prod a b = Prod Float newtype Quot a b = Quot Float instance (Unit a, Unit b) => Unit(Prod a b) where unit = Prod value(Prod x) = x instance (Unit a, Unit b) => Unit(Quot a b) where unit = Quot value(Quot x) = x infix 7 *$, /$ infix 6 +$, -$ (+$) :: (Unit a) => a -> a -> a (-$) :: (Unit a) => a -> a -> a (*$) :: (Unit a, Unit b) => a -> b -> Prod a b (/$) :: (Unit a, Unit b) => a -> b -> Quot a b x +$ y = unit(value x + value y) x -$ y = unit(value x - value y) x *$ y = Prod(value x * value y) x /$ y = Quot(value x / value y) m = Metres 5 s = Seconds 2 m' = m +$ m -- OK: Metres m2 = m *$ m -- OK: Prod Metres Metres v = m /$ s -- OK: Quot Metres Seconds a = m /$ (s *$ s) -- OK: Quot Metres (Prod Seconds Seconds) x = m -$ s -- error It would be nicer if Haskell had infix type constructors: newtype a :* b = Prod Float newtype a :/ b = Quot Float Cheers, - Andreas -- Andreas Rossberg, [EMAIL PROTECTED] :: be declarative. be functional. just be. ::
Re: Units of measure
I think the original poster's idea of using sets of exponents would work better. Then Prod could be a function which adds the relevant exponents, and Quod subtracts, so your units would be automatically reduced. But, I have no idea how to do this in Haskell since I'm still learning the language :) On Thu, 26 Aug 1999, Andreas Rossberg wrote: | You are right, I overlooked that. But this is not even the most serious | problem, overloading the operators accordingly might be possible with | MPTCs, I think. The hard problem is that you cannot establish equalities | like | | Prod a (Quot b a) = b | | Sigh. -- cliff crawford http://www.people.cornell.edu/pages/cjc26/ There are more stars in the sky than there are -><-grains of sand on all the beaches of the world.
RE: Units of measure
Good idea. Andrew Kennedy wrote a whole thesis about this, and a
paper or two besides.
http://research.microsoft.com/~akenn/
> -Original Message-
> From: Tom Pledger
> Sent: Thursday, August 26, 1999 7:56 AM
> To: [EMAIL PROTECTED]
> Cc: [EMAIL PROTECTED]
> Subject: Units of measure
>
>
> Hi. Here's a short question which has been bothering me, and a longer
> discussion of why. Apologies if it's a rote.
>
> Where do units of measure fit into a type system?
>
> Expressions along these lines should ideally be legal:
>
> (x :: Metres) / (y :: Seconds)
>
> (x :: Pounds_sterling_per_kilowatt_hour) * (y :: kilowatt_hours)
>
> ...and there's something to be said for supporting the addition of a
> number of feet to a number of metres,
>
> ...but this should ideally be rejected by the compiler:
>
> (x :: Metres) + (y :: Seconds)
>
> It's tempting to use the type system, but then it runs into these two
> problems (at least):
> - There are infinitely many derivable units of measure. At what
>point do you stop defining them singly and statically?
> - There's a slew of (*) and (/) overloadings, none of which are fit
>to be written by hand.
>
> If a set of units is declared elsewhere than in your program, what
> happens when another currency becomes of concern?
>
> Could every numeric expression be accompanied by a set - inferred
> where possible - of (unit, nonzero exponent) pairs? For example,
> could a force expression have {(kg, 1), (m, 1), (s, -2)} as part of
> its type?
>
> Regards,
> Tom
>
