Recent

Author Topic: Type checking of units of measurement  (Read 8970 times)

circular

  • Hero Member
  • *****
  • Posts: 4196
    • Personal webpage
Type checking of units of measurement
« on: January 22, 2023, 02:02:45 pm »
In another topic about type system, we talked a bit about type checking of dimensioned quantities (values in meters, time in seconds etc.).
https://forum.lazarus.freepascal.org/index.php/topic,61781.0.html

Few languages handle this natively. Units of measure are handled natively in F# and it can be implemented in Rust.
Code: F#  [Select][+][-]
  1. open Microsoft.FSharp.Data.UnitSystems.SI.UnitNames
  2. [<Measure>] type miles
  3. [<Measure>] type hour
  4. let milesPerMeter = 0.00062137<miles/meter>
  5. let secondPerHour = 3600.0<second/hour>
  6.  
  7. let distance = 1000.0<meter> * milesPerMeter
  8. let time = 60.0<second> / secondPerHour
  9. printfn "Speed: %A mph" (distance / time)

In Rust, using the crate dimensioned:
Code: Text  [Select][+][-]
  1. extern crate dimensioned as dim;
  2. use dim::si;
  3.  
  4. fn main() {
  5.     let user_distance = 10.0 * M;
  6.     let user_time = 5.0 * s;
  7.     let user_speed = user_distance / user_time;
  8.     println!("Speed is {} m/s", user_speed);
  9. }

This is checked at compile time only so there is no overhead and it can be applied to any numeric type.

I was wondering how to do that in FreePascal, playing a little bit I made a unit to have some basic support for meters, seconds and speed.

Attached is the unit to add support for units. It can be used like this:
Code: Pascal  [Select][+][-]
  1. uses UUnits;
  2.  
  3. var
  4.   distance: TLengthInKilometer;
  5.   time: TDurationInHour;
  6.   time2: TDuration; // SI unit is [s]
  7.   speed: TSpeedInKilometerPerHour;
  8.   acceleration, gravity: TAcceleration; // SI unit is [m/s2]
  9.  
  10. begin
  11.   distance := ((10*km + 100*m) * 2).ToKilometer;
  12.   time := 2*h;
  13.   speed := distance/time;
  14.  
  15.   time2 := 10*s;
  16.   acceleration := speed/time2;
  17.  
  18.  
  19.   writeln('The distance is: ', distance.ToString);
  20.   writeln('The number of hundreds of meters is: ', distance / (100*m) );
  21.   writeln('The time is: ', time.ToString);
  22.   // casting to TDuration uses the default unit Second instead of Hour
  23.   writeln('Also: ', TDuration(time).ToString);
  24.   writeln('The speed is: ', speed.ToString);
  25.   writeln('Also: ', TSpeed(speed).ToString);
  26.   writeln;
  27.  
  28.   distance := 50*km;
  29.   // ToVerboseString display the full name of the unit
  30.   writeln('Distance to go: ', distance.ToVerboseString);
  31.   time := distance / speed;
  32.   writeln('Time to get there: ', time.ToString);
  33.   writeln('Also: ', TDuration(time).ToString);
  34.   writeln;
  35.  
  36.   writeln('The time to accelerate is: ', time2.ToString);
  37.   writeln('The acceleration is: ', acceleration.ToString);
  38.   writeln('Also: ', acceleration.ToKilometerPerHourPerSecond.ToString);
  39.   writeln;
  40.  
  41.   gravity := 9.81*(m/s2);
  42.   writeln('Gravity is: ', gravity.ToVerboseString);
  43. end.

Units are checked at compile time, so that's what we wanted. There is a tiny overhead because the compiler adds a few useless assembler instructions, but that's not very significant.

It is a bit tedious though to define all possible cases for operators. Maybe one could generate the code of UUnit, though it kind of makes sense to specify each operator that one actually want to allow.
Conscience is the debugger of the mind

marcov

  • Administrator
  • Hero Member
  • *
  • Posts: 11383
  • FPC developer.
Re: Type checking of units of measurement
« Reply #1 on: January 22, 2023, 02:16:41 pm »
There already is convutils ?

circular

  • Hero Member
  • *****
  • Posts: 4196
    • Personal webpage
Re: Type checking of units of measurement
« Reply #2 on: January 22, 2023, 02:22:52 pm »
It is not about converting values but about type checking at compile time.

For example, with this type checking, you cannot assign a duration to a distance, etc. Also the overhead is minimal.
Conscience is the debugger of the mind

marcov

  • Administrator
  • Hero Member
  • *
  • Posts: 11383
  • FPC developer.
Re: Type checking of units of measurement
« Reply #3 on: January 22, 2023, 02:46:59 pm »
Looks nice. But maybe the overloading gets unwieldy. Perhaps a value in the record that gives the subtype of a dimension (any length, including units like angstrom etc)

It would save many, many overload routines even for just all the length units out there.
« Last Edit: January 22, 2023, 02:48:46 pm by marcov »

Bogen85

  • Hero Member
  • *****
  • Posts: 595
Re: Type checking of units of measurement
« Reply #4 on: January 22, 2023, 06:02:12 pm »
It is not about converting values but about type checking at compile time.

For example, with this type checking, you cannot assign a duration to a distance, etc. Also the overhead is minimal.

This looks good, and is the kind of enforcement I was wanting.

circular

  • Hero Member
  • *****
  • Posts: 4196
    • Personal webpage
Re: Type checking of units of measurement
« Reply #5 on: January 22, 2023, 07:09:04 pm »
This looks good, and is the kind of enforcement I was wanting.
I am glad you like it and if it can be useful for you.  :)

Looks nice. But maybe the overloading gets unwieldy. Perhaps a value in the record that gives the subtype of a dimension (any length, including units like angstrom etc)

It would save many, many overload routines even for just all the length units out there.
Yes, the overloading could get out of hand. In this example, I presume that only two units will be used but that's clearly not always the case.

Defining the base unit in the value would not be sufficient to check for type, this needs to be done at compile time.

Another approach is to always store the value in the base unit. So when you would write for example 5*km, it will be in fact computed as 5000*m. This makes things easier but always doing this multiplication can have some effect on the precision of the value and is an additional arithmetic operation. It could be a good compromise though to reduce the amount of overloading.
Conscience is the debugger of the mind

Warfley

  • Hero Member
  • *****
  • Posts: 1499
Re: Type checking of units of measurement
« Reply #6 on: January 22, 2023, 08:29:37 pm »
I personally do like using what I call wrapper types for different semantic concepts for typechecking (e.g. using a type TEmail instead string so I don't accidentally mix an email up with for example the username), but the typecasting can make it a bit tedious sometimes.

What I was wondering, why have a type for every single quantity of basically the same unit? Just talking distances, there are all the metric units from pico to kilometers, then there are the imperials, etc. All needing to be interoperable with each other.

You could just use one unit TDistance and have converters:
Code: Pascal  [Select][+][-]
  1. type
  2.   generic TUnit<const BaseUnit: string> = record
  3.   const Base = BaseUnit;
  4.   type TSelf = specialize TUnit<BaseUnit>;
  5.   public
  6.     value: Double;
  7.     class operator +(const lhs, rhs: TSelf): TSelf;
  8.   end;
  9.  
  10.   generic TConverter<TBaseUnit> = record
  11.     type TSelf = specialize TConverter<TBaseUnit>;
  12.     public Factor: Double;
  13.     class operator *(value: Double; converter: TSelf): TBaseUnit;
  14.   end;
  15.  
  16. type TDistance = specialize TUnit<'m'>;
  17. const m: specialize TConverter<TDistance> = (Factor: 1);
  18. const km: specialize TConverter<TDistance> = (Factor: 1000);
  19. const mm: specialize TConverter<TDistance> = (Factor: 0.001);
  20.  
  21. type TTime = specialize TUnit<'s'>;
  22. const s: specialize TConverter<TDistance> = (Factor: 1);
  23. const min: specialize TConverter<TDistance> = (Factor: 60);
  24. const h: specialize TConverter<TDistance> = (Factor: 3600);
  25.  
  26. implementation
  27.  
  28. class operator TUnit.+(const lhs, rhs: TSelf): TSelf;
  29. begin
  30.   result.value := lhs.value + rhs.value;
  31. end;
  32.  
  33. class operator TConverter.*(value: Double; converter: TSelf): TBaseUnit;
  34. begin
  35.   Result.value := value * converter.Factor;
  36. end;

This still needs a lot of units for combination (such as distance by time being velocity and so on), but it is much more managable
« Last Edit: January 22, 2023, 08:32:23 pm by Warfley »

circular

  • Hero Member
  • *****
  • Posts: 4196
    • Personal webpage
Re: Type checking of units of measurement
« Reply #7 on: January 22, 2023, 10:27:49 pm »
That's a good idea to have this generic converter record. This way you can use the same code for the * operator. Sometimes I don't know what can be done or not with generics. For example, I am surprised that one can put a string constant (BaseUnit) as generic parameter. Thanks for showing me  :)
Conscience is the debugger of the mind

Warfley

  • Hero Member
  • *****
  • Posts: 1499
Re: Type checking of units of measurement
« Reply #8 on: January 23, 2023, 10:20:47 am »
Constants as generics is a new feature thats currently only available in trunk I think, exremely useful for some situations

circular

  • Hero Member
  • *****
  • Posts: 4196
    • Personal webpage
Re: Type checking of units of measurement
« Reply #9 on: January 25, 2023, 11:28:20 pm »
Ok, so using what you suggest to have a variety of units, not using const generic parameter as I don't use trunk, here is what I get:
Code: Pascal  [Select][+][-]
  1. uses UUnits;
  2.  
  3. var
  4.   km_h: TSpeedUnit;
  5.   km_h_s, m_s2: TAccelerationUnit;
  6.  
  7.   distance: TLength;
  8.   time, time2: TDuration;
  9.   speed: TSpeed;
  10.   acceleration, gravity: TAcceleration;
  11.  
  12. begin
  13.   km_h := km/h;
  14.   km_h_s := km_h/s;
  15.   m_s2 := m/s2;
  16.  
  17.   distance := (10*km + 100*m) * 2;
  18.   time := 2*h;
  19.   speed := distance/time;
  20.  
  21.   time2 := 10*s;
  22.   acceleration := speed/time2;
  23.  
  24.   writeln('The distance is: ', km.Format(distance));
  25.   writeln('The number of hundreds of meters is: ', distance / (100*m) );
  26.   writeln('The time is: ', h.Format(time));
  27.   // the default time unit is the Second
  28.   writeln('Also: ', time.ToString);
  29.   writeln('The speed is: ', km_h.Format(speed));
  30.   writeln('Also: ', speed.ToString);
  31.   writeln;
  32.  
  33.   distance := 50*km;
  34.   // VerboseFormat display the full name of the unit
  35.   writeln('Distance to go: ', km.VerboseFormat(distance));
  36.   time := distance / speed;
  37.   writeln('Time to get there: ', h.Format(time));
  38.   writeln('Also: ', time.ToString);
  39.   writeln;
  40.  
  41.   writeln('The time to accelerate is: ', time2.ToString);
  42.   writeln('The acceleration is: ', acceleration.ToString);
  43.   writeln('Also: ', km_h_s.Format(acceleration));
  44.   writeln;
  45.  
  46.   gravity := 9.81*m_s2;
  47.   writeln('Gravity is: ', gravity.ToVerboseString);
  48. end.

It works. Though now, there is always a multiplication by a factor, even when it is not necessary. For example 5*m will multiply the value by 1. Also it will always convert to the base unit, which can give some a slight inaccuracy. Also one need to compute the units (km_h etc.) at the beginning. We could use the notation km/h later but it would actually recompute the unit each time.
Conscience is the debugger of the mind

Warfley

  • Hero Member
  • *****
  • Posts: 1499
Re: Type checking of units of measurement
« Reply #10 on: January 26, 2023, 10:22:34 am »
I've looked at the assembler, direct initialization (https://godbolt.org/z/TaxhMTjrW):
Code: C  [Select][+][-]
  1.         leaq    -8(%rsp),%rsp
  2.         movq    _$OUTPUT$_Ld1,%rax
  3.         movq    %rax,(%rsp)
  4.         leaq    8(%rsp),%rsp
  5.         ret

With a converter:
Code: Pascal  [Select][+][-]
  1.         leaq    -24(%rsp),%rsp
  2.         movq    m(),%rax
  3.         movq    %rax,16(%rsp)
  4.         movsd   _$OUTPUT$_Ld1,%xmm0
  5.         mulsd   16(%rsp),%xmm0
  6.         movsd   %xmm0,8(%rsp)
  7.         leaq    24(%rsp),%rsp
  8.         ret
So it's a 2 move and 1 multiplication instruction more, this is probably around 1ns overhead on a modern CPU.
This is nothign to worry about.

And if you still worry about it, you should try and compile it with LLVM, this will probably completely optmize this away (I don't have an LLVM on this machine right now so I can't test it).

So I wouldn't worry about this. Also the m/s will probably be optimized to just 1 a few extra instructions, or maybe even fully (with llvm)
« Last Edit: January 26, 2023, 10:27:54 am by Warfley »

ccrause

  • Hero Member
  • *****
  • Posts: 845
Re: Type checking of units of measurement
« Reply #11 on: January 26, 2023, 11:56:20 am »
This is an interesting topic with a lot of promise for type safe general calculations involving dimensioned values.  Consider that there are 7 base quantities from which all other quantities (or physical units of measure) can be derived.  If the current concept can be extended to handle arbitrary units of measure in a type safe way it would be mind blowing.  Take the following example calculation:
Code: Pascal  [Select][+][-]
  1. var
  2.   F: TForce;         // SI base units [kg.m/s/s]
  3.   m: TMass;          // SI base units [kg]
  4.   a: acceleration;   // SI base units [m/s/s]
  5. begin
  6.   m := 100;  // kg
  7.   F := 1000; // Newton, or kg.m/s/s
  8.   a := F / a;
  9. end;

A complicated mix of units which is difficult to keep track of manually, but if the compiler can ensure that the LHS and RHS base units simplify to the same (i.e. kg.m/s/s) then the expression is dimensionally consistent.  Also, converting to any derived units become relatively simple, perhaps by having a table that map between the base units and any desired derived units.

A slight complication is converting quantities that involve offsets, for example converting temperatures (K <-> °C, or R <-> °F) or gauge to absolute pressure.

440bx

  • Hero Member
  • *****
  • Posts: 3946
Re: Type checking of units of measurement
« Reply #12 on: January 26, 2023, 04:41:14 pm »
This is an interesting topic with a lot of promise for type safe general calculations involving dimensioned values.  Consider that there are 7 base quantities from which all other quantities (or physical units of measure) can be derived.  If the current concept can be extended to handle arbitrary units of measure in a type safe way it would be mind blowing. 
I agree.  It really is extremely interesting because it has the potential to be extremely useful.

Currently, using FPC (and Delphi), I see two major hurdles to getting it done right.

The first one is, the compiler does not recognize _true_ typed constants, e.g, "const SomeTime : TSECONDS = 10;" that declaration would not result in a compiler constant but a variable which is a problem because their treatment by the compiler is very different.

The other one is, in FPC, there does not seem to be a way to create "hard" new types other than using "record".  Without using "record" saying e.g, TMYTYPE = type integer; is just declaring a synonym for integer instead of declaring a new type.  IOW, TMYTYPE is still assignment compatible with "integer" which is a problem when using this or similar construction to create units of measurement.

I think that circumventing the above two problems would make a general implementation of units of measure very difficult and cumbersome to use, if possible at all.

(FPC v3.0.4 and Lazarus 1.8.2) or (FPC v3.2.2 and Lazarus v3.2) on Windows 7 SP1 64bit.

circular

  • Hero Member
  • *****
  • Posts: 4196
    • Personal webpage
Re: Type checking of units of measurement
« Reply #13 on: January 27, 2023, 01:48:42 pm »
A complicated mix of units which is difficult to keep track of manually, but if the compiler can ensure that the LHS and RHS base units simplify to the same (i.e. kg.m/s/s) then the expression is dimensionally consistent.  Also, converting to any derived units become relatively simple, perhaps by having a table that map between the base units and any desired derived units.
Basically, the compiler would need to have some counters that can be added and subtracted, that can be attached to a type. For example, s, s2 and 3 would be derived from the same generic type with a const parameter 1, 2 and 3.
Code: Pascal  [Select][+][-]
  1. type
  2.   TUnit<const Symbol: string; const Name: string; const Exponent: integer> = class
  3.     class operator *(
  4.       const ALeft: specialize TUnit<Symbol, Name, ExponentLeft>;
  5.       const ARight: specialize TUnit<Symbol, Name, ExponentRight>):
  6.       specialize TUnit<Symbol, Name, ExponentLeft+ExponentRight>;  
  7.   end;
  8.  
  9. class operator TUnit.*(
  10.   const ALeft: specialize TUnit<Symbol, Name, ExponentLeft>;
  11.   const ARight: specialize TUnit<Symbol, Name, ExponentRight>):
  12.   specialize TUnit<Symbol, Name, ExponentLeft+ExponentRight>;
  13. begin
  14.   result := nil; // don't need an actual instance
  15. end;  
  16.  
Conscience is the debugger of the mind

avra

  • Hero Member
  • *****
  • Posts: 2514
    • Additional info
Re: Type checking of units of measurement
« Reply #14 on: January 27, 2023, 03:12:46 pm »
Nice work. Potentially very useful. When polished I would like to see it as FPC package available out of the box.

Although I fully understand the reasoning for uunits.pas naming, pascal developers have strong relation to unit term so to avoid confusion maybe something like dimunits.pas or dimensions.pas would be better. What do you think?
ct2laz - Conversion between Lazarus and CodeTyphon
bithelpers - Bit manipulation for standard types
pasettimino - Siemens S7 PLC lib

 

TinyPortal © 2005-2018