comp.lang.ada
 help / color / Atom feed
* SI Units Checked and Unchecked
@ 2018-08-09 12:44 AdaMagica
  2018-08-09 13:47 ` Dan'l Miller
                   ` (2 more replies)
  0 siblings, 3 replies; 32+ messages in thread
From: AdaMagica @ 2018-08-09 12:44 UTC (permalink / raw)


This is a complete rework using Ada 2012 predicates.

These packages provide a method to commpute with physical items in full generality under dimensional correctness checking. Dimensioned items are written in a natural style with the unit attached as a string.

The base type is private:

  type Item is private;

There are subtypes defined for all 7 base units defined in the SI system and many more:

  subtype Length is Item with Dynamic_Predicate => has_Dimension (Length, "m");
  subtype Volume is Item with Dynamic_Predicate => has_Dimension (Volume, "m**3");
  subtype Speed  is Item with Dynamic_Predicate => has_Dimension (Speed , "m/s");
  subtype Force  is Item with Dynamic_Predicate => has_Dimension (Force , "N");
  subtype Resistance is Item with Dynamic_Predicate => has_Dimension (Resistance, "Ohm");

Variables are defined like this:

  A: Acceleration := 5.0*"m/s**2";
  V: Speed := 10.0*"km/h";
  T: Time  :=  1.0*"min";
  D: Length := V*T + 0.5*A*T**2;

  D := 1.0*"J";  will raise an exception.

Units and prefixes are case sensitive (as defined in SI): "mS" is millisiemens, "Ms" is megasecond.

Dimensioned IO is also provided:

  V := 1.0*"m/s";          -- output as
  Put (V);                 -- 1.0*m*s**(-1)
  Put (V, Dim => "km/h");  -- 3.6*km/h
  Put (V, Dim => "s");     -- will raise an exception

Download from here:
http://www.christ-usch-grein.homepage.t-online.de/Ada/Dimension/SI.html

If you should use (even like) this method, please drop me a note with your findings.

Have fun.
Christoph

^ permalink raw reply	[flat|nested] 32+ messages in thread

* Re: SI Units Checked and Unchecked
  2018-08-09 12:44 SI Units Checked and Unchecked AdaMagica
@ 2018-08-09 13:47 ` Dan'l Miller
  2018-08-09 14:07   ` Dmitry A. Kazakov
  2018-08-09 14:31   ` AdaMagica
  2018-08-09 16:07 ` Jeffrey R. Carter
  2019-09-04 14:20 ` Shark8
  2 siblings, 2 replies; 32+ messages in thread
From: Dan'l Miller @ 2018-08-09 13:47 UTC (permalink / raw)


On Thursday, August 9, 2018 at 7:44:13 AM UTC-5, AdaMagica wrote:
> This is a complete rework using Ada 2012 predicates.
> 
> These packages provide a method to commpute with physical items in full generality under dimensional correctness checking. Dimensioned items are written in a natural style with the unit attached as a string.
> 
> The base type is private:
> 
>   type Item is private;
> 
> There are subtypes defined for all 7 base units defined in the SI system and many more:
> 
>   subtype Length is Item with Dynamic_Predicate => has_Dimension (Length, "m");
>   subtype Volume is Item with Dynamic_Predicate => has_Dimension (Volume, "m**3");
>   subtype Speed  is Item with Dynamic_Predicate => has_Dimension (Speed , "m/s");
>   subtype Force  is Item with Dynamic_Predicate => has_Dimension (Force , "N");
>   subtype Resistance is Item with Dynamic_Predicate => has_Dimension (Resistance, "Ohm");
> 
> Variables are defined like this:
> 
>   A: Acceleration := 5.0*"m/s**2";
>   V: Speed := 10.0*"km/h";
>   T: Time  :=  1.0*"min";
>   D: Length := V*T + 0.5*A*T**2;
> 
>   D := 1.0*"J";  will raise an exception.

Shouldn't the •entire• point of a units-of-measurement library (or feature of language) be compile-time errors, not run-time exceptions/errors.

> Units and prefixes are case sensitive (as defined in SI): "mS" is millisiemens, "Ms" is megasecond.
> 
> Dimensioned IO is also provided:
> 
>   V := 1.0*"m/s";          -- output as
>   Put (V);                 -- 1.0*m*s**(-1)
>   Put (V, Dim => "km/h");  -- 3.6*km/h
>   Put (V, Dim => "s");     -- will raise an exception
> 
> Download from here:
> http://www.christ-usch-grein.homepage.t-online.de/Ada/Dimension/SI.html
> 
> If you should use (even like) this method, please drop me a note with your findings.

I am an advocate of units-of-measure in programming.

I would be interested in a summary (or even better, an AI) that itemizes all the core-language obstacles in currently-standardized Ada to moving all the incompatible usages of units to be compile-time errors instead of raising exceptions.

^ permalink raw reply	[flat|nested] 32+ messages in thread

* Re: SI Units Checked and Unchecked
  2018-08-09 13:47 ` Dan'l Miller
@ 2018-08-09 14:07   ` Dmitry A. Kazakov
  2018-08-09 15:03     ` Dan'l Miller
  2018-08-09 14:31   ` AdaMagica
  1 sibling, 1 reply; 32+ messages in thread
From: Dmitry A. Kazakov @ 2018-08-09 14:07 UTC (permalink / raw)


On 2018-08-09 15:47, Dan'l Miller wrote:

> Shouldn't the •entire• point of a units-of-measurement library (or feature of language) be compile-time errors, not run-time exceptions/errors.

No, because in most cases the unit is unknown. Consider a widget library 
with instruments indicating dimensioned values, dimensioned calculator, 
serialization of dimensioned data etc.

What is necessary but not sufficient is language support for handling 
statically known constraints using compile-time static operations and 
removing statically known discriminants from the representation.

Note a direct analogy with classes for scalar types. Type tag is in 
essence just a discriminant. For some types we want static discriminants 
and other constraints removed.

> I would be interested in a summary (or even better, an AI) that itemizes all the core-language obstacles in currently-standardized Ada to moving all the incompatible usages of units to be compile-time errors instead of raising exceptions.

The Ada type system is not capable to handle dimensioned types. I posted 
a list of requirements for a dimensioned types support some years ago here.

There are lots of language issues to resolve first before approaching 
dimensioned types.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de


^ permalink raw reply	[flat|nested] 32+ messages in thread

* Re: SI Units Checked and Unchecked
  2018-08-09 13:47 ` Dan'l Miller
  2018-08-09 14:07   ` Dmitry A. Kazakov
@ 2018-08-09 14:31   ` AdaMagica
  2018-08-09 15:19     ` Dan'l Miller
  1 sibling, 1 reply; 32+ messages in thread
From: AdaMagica @ 2018-08-09 14:31 UTC (permalink / raw)


Am Donnerstag, 9. August 2018 15:47:47 UTC+2 schrieb Dan'l Miller:
> I would be interested in a summary (or even better, an AI) that itemizes all the core-language obstacles in currently-standardized Ada to moving all the incompatible usages of units to be compile-time errors instead of raising exceptions.

Dan'l, just go to
http://www.christ-usch-grein.homepage.t-online.de/Ada/Dimension/Dimension.html
there you'll find a summary of attempts to use dimensional arithmetics in Ada.

^ permalink raw reply	[flat|nested] 32+ messages in thread

* Re: SI Units Checked and Unchecked
  2018-08-09 14:07   ` Dmitry A. Kazakov
@ 2018-08-09 15:03     ` Dan'l Miller
  2018-08-09 15:51       ` Dmitry A. Kazakov
  2018-08-09 18:47       ` Paul Rubin
  0 siblings, 2 replies; 32+ messages in thread
From: Dan'l Miller @ 2018-08-09 15:03 UTC (permalink / raw)


On Thursday, August 9, 2018 at 9:07:23 AM UTC-5, Dmitry A. Kazakov wrote:
> On 2018-08-09 15:47, Dan'l Miller wrote:
> 
> > Shouldn't the •entire• point of a units-of-measurement library (or feature of language) be
> > compile-time errors, not run-time exceptions/errors.
> 
> No, because in most cases the unit is unknown.

No, apparently in “most cases” you are writing either some sort of toy calculator or some sort of excessively over-generalized library marketed to too-wide of an audience.  Apparently in “most cases” you are not writing the •app-domain• controls for actual hardware deployed into an actual physical environment, where the units of measure are a settled topic, not pulled out of thin air on a changing whim.

Well, factually incorrect opinions like yours above would be the reason for losses similar to the Mars Climate Orbiter in the future, even if coded is so-called ‘safety-critical’ Ada.

http://www.cnn.com/TECH/space/9909/30/mars.metric.02

Thinking that units of measure is a run-time choice (instead of an end-to-end agreed-upon engineering-time choice) would cause other such epic engineering failures for no good reason other than units of measure not being strongly-typed in the programming language.

> Consider a widget library 

Yep, library.

> with instruments indicating dimensioned values, dimensioned calculator, 
> serialization of dimensioned data etc.

So, Dmitry, you are making the mistake of excessive reuse in the app-domain of an unfinished library.  Sure, at some deep level in the library, there can be a generic gauge that skeuomorphically represents a swinging black needle on a white circle that has no idea whether it is measuring pressure or amperes or volts or speed.  But at the intended user-interface facade of the library, there should be:
1) a strongly-typed gauge for amperes,
2) a separate strongly-typed gauge for pressure,
3) a separate strongly-typed gauge for volts,
4) a separate strongly-typed gauge for speed,
and so forth that are wrappers around the one shared white circle with swinging black needle as the generic unitless-clueless(-at-engineering-/compile-time) gauge of which you speak.

> What is necessary but not sufficient is language support for handling 
> statically known constraints using compile-time static operations and 
> removing statically known discriminants from the representation.
> 
> Note a direct analogy with classes for scalar types. Type tag is in 
> essence just a discriminant. For some types we want static discriminants 
> and other constraints removed.
> 
> > I would be interested in a summary (or even better, an AI) that itemizes all the core-language
> > obstacles in currently-standardized Ada to moving all the incompatible usages of units to be
> > compile-time errors instead of raising exceptions.
> 
> The Ada type system is not capable to handle dimensioned types. I posted 
> a list of requirements for a dimensioned types support some years ago here.
> 
> There are lots of language issues to resolve first before approaching 
> dimensioned types.

As strongly-typed as Ada is, we often yearn for a more-Ada-than-Ada level of an even stronger-typed Ada.  Even you.  Even for compile-time-enforced strongly-typed units of measure.  (Or else why would you expend that analysis's effort in the first place?)

^ permalink raw reply	[flat|nested] 32+ messages in thread

* Re: SI Units Checked and Unchecked
  2018-08-09 14:31   ` AdaMagica
@ 2018-08-09 15:19     ` Dan'l Miller
  0 siblings, 0 replies; 32+ messages in thread
From: Dan'l Miller @ 2018-08-09 15:19 UTC (permalink / raw)


On Thursday, August 9, 2018 at 9:31:38 AM UTC-5, AdaMagica wrote:
> Am Donnerstag, 9. August 2018 15:47:47 UTC+2 schrieb Dan'l Miller:
> > I would be interested in a summary (or even better, an AI) that itemizes all the core-language
> > obstacles in currently-standardized Ada to moving all the incompatible usages of units to be
> > compile-time errors instead of raising exceptions.
> 
> Dan'l, just go to
> http://www.christ-usch-grein.homepage.t-online.de/Ada/Dimension/Dimension.html
> there you'll find a summary of attempts to use dimensional arithmetics in Ada.

Thank you!  (for both the webpage's useful analysis as well as the link to it)  This will be worth studying deeply.  I am always looking for why C++ ever pulls ahead of Ada on some strong-typing topics.  Compile-time enforcement of units of measure is one of them.  Meticulous typing (especially compile-time enforcement of strong typing) is supposed to be Ada's crowning achievement; C++ or any recent upstart language (e.g., Rust) is not supposed to be able to threaten to usurp the throne from the king on typing-enforcement topics.

(C++ gets an “Oh, nevermind, go forth & prosper” response from me when I track a capability down to needing a Turing-complete template engine to enact the capability only via metatemplate-programming functional-language interpreter in the compiler.  Ada2027 needs a bona fide Turing-complete compile-time source-code generator, not Turing-complete generics as a poor-man's substitute, as C++ has.)


^ permalink raw reply	[flat|nested] 32+ messages in thread

* Re: SI Units Checked and Unchecked
  2018-08-09 15:03     ` Dan'l Miller
@ 2018-08-09 15:51       ` Dmitry A. Kazakov
  2018-08-09 17:32         ` Dan'l Miller
  2018-08-09 18:47       ` Paul Rubin
  1 sibling, 1 reply; 32+ messages in thread
From: Dmitry A. Kazakov @ 2018-08-09 15:51 UTC (permalink / raw)


On 2018-08-09 17:03, Dan'l Miller wrote:

> So, Dmitry, you are making the mistake of excessive reuse in the app-domain of an unfinished library.  Sure, at some deep level in the library, there can be a generic gauge that skeuomorphically represents a swinging black needle on a white circle that has no idea whether it is measuring pressure or amperes or volts or speed.  But at the intended user-interface facade of the library, there should be:
> 1) a strongly-typed gauge for amperes,
> 2) a separate strongly-typed gauge for pressure,
> 3) a separate strongly-typed gauge for volts,
> 4) a separate strongly-typed gauge for speed,
> and so forth that are wrappers around the one shared white circle with swinging black needle as the generic unitless-clueless(-at-engineering-/compile-time) gauge of which you speak.

No, I am speaking about a widget that checks and enforces measurement 
units. If you look how GUI widgets are constructed you would notice 
adjustment objects, events to propagate, properties to set and query, 
MVC and dozens of other things connecting the widget to the world around 
it, all dealing with measurement units. There is no way anybody could 
design this with generics or statically typed.

It can be statically constrained though, in some few cases, because 
widgets are customary stored and restored. There might be some limited 
cases with all static layouts in avionics or medical applications, these 
are an exception from the common rule.

And note that speed and pressure are measured in dozens different units. 
One of the requirements of sane design is that all compatible units were 
allowed. E.g. an adjustment object in kPa should work with a barograph 
indicating mm Hg. And I don't remember a single customer who ever wanted 
his HMI showing speed in SI's m/s.

>> What is necessary but not sufficient is language support for handling
>> statically known constraints using compile-time static operations and
>> removing statically known discriminants from the representation.
>>
>> Note a direct analogy with classes for scalar types. Type tag is in
>> essence just a discriminant. For some types we want static discriminants
>> and other constraints removed.
>>
>>> I would be interested in a summary (or even better, an AI) that itemizes all the core-language
>>> obstacles in currently-standardized Ada to moving all the incompatible usages of units to be
>>> compile-time errors instead of raising exceptions.
>>
>> The Ada type system is not capable to handle dimensioned types. I posted
>> a list of requirements for a dimensioned types support some years ago here.
>>
>> There are lots of language issues to resolve first before approaching
>> dimensioned types.
> 
> As strongly-typed as Ada is, we often yearn for a more-Ada-than-Ada level of an even stronger-typed Ada.  Even you.  Even for compile-time-enforced strongly-typed units of measure.  (Or else why would you expend that analysis's effort in the first place?)

The issues I meant are necessary precondition to make a reasonable AI on 
dimensioned types.

As an example of such an issue consider the problem of constraint 
propagation:

    type Dimensioned is ...;
    type Dimensioned_Array (Positive range <>) of Dimensioned;

Here we want the measurement unit constraint of the array to propagate 
to its elements. And of course we don't want the elements in the array 
to keep their constraints as they must all be coming from the array (or 
a container in general case). Ada type system lacks such mechanism. Note 
that this problem is larger than the problem of measurement units. 
Actually, if the type system were fixed no specific AI might be required 
at all.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de


^ permalink raw reply	[flat|nested] 32+ messages in thread

* Re: SI Units Checked and Unchecked
  2018-08-09 12:44 SI Units Checked and Unchecked AdaMagica
  2018-08-09 13:47 ` Dan'l Miller
@ 2018-08-09 16:07 ` Jeffrey R. Carter
  2018-08-09 17:41   ` AdaMagica
  2019-09-04 14:20 ` Shark8
  2 siblings, 1 reply; 32+ messages in thread
From: Jeffrey R. Carter @ 2018-08-09 16:07 UTC (permalink / raw)


On 08/09/2018 02:44 PM, AdaMagica wrote:
> 
> The base type is private:
> 
>    type Item is private;
> 
> There are subtypes defined for all 7 base units defined in the SI system and many more:
> 
>    subtype Length is Item with Dynamic_Predicate => has_Dimension (Length, "m");
>    subtype Volume is Item with Dynamic_Predicate => has_Dimension (Volume, "m**3");
>    subtype Speed  is Item with Dynamic_Predicate => has_Dimension (Speed , "m/s");
>    subtype Force  is Item with Dynamic_Predicate => has_Dimension (Force , "N");
>    subtype Resistance is Item with Dynamic_Predicate => has_Dimension (Resistance, "Ohm");
> 
> Variables are defined like this:
> 
>    A: Acceleration := 5.0*"m/s**2";
>    V: Speed := 10.0*"km/h";
>    T: Time  :=  1.0*"min";
>    D: Length := V*T + 0.5*A*T**2;

Is this standard Ada 12, or is it GNAT specific?

-- 
Jeff Carter
"I was in love with a beautiful blonde once, dear.
She drove me to drink. That's the one thing I'm
indebted to her for."
Never Give a Sucker an Even Break
109


^ permalink raw reply	[flat|nested] 32+ messages in thread

* Re: SI Units Checked and Unchecked
  2018-08-09 15:51       ` Dmitry A. Kazakov
@ 2018-08-09 17:32         ` Dan'l Miller
  2018-08-09 19:42           ` Dmitry A. Kazakov
  0 siblings, 1 reply; 32+ messages in thread
From: Dan'l Miller @ 2018-08-09 17:32 UTC (permalink / raw)


On Thursday, August 9, 2018 at 10:51:59 AM UTC-5, Dmitry A. Kazakov wrote:
> On 2018-08-09 17:03, Dan'l Miller wrote:
> 
> > So, Dmitry, you are making the mistake of excessive reuse in the app-domain of an unfinished library. 
> > Sure, at some deep level in the library, there can be a bland gauge that skeuomorphically represents a > > swinging black needle on a white circle that has no idea whether it is measuring pressure or amperes
> > or volts or speed.  But at the intended user-interface facade of the library, there should be:
> > 1) a strongly-typed gauge for amperes,
> > 2) a separate strongly-typed gauge for pressure,
> > 3) a separate strongly-typed gauge for volts,
> > 4) a separate strongly-typed gauge for speed,
> > and so forth that are wrappers around the one shared white circle with swinging black needle as the
> > bland unitless-clueless(-at-engineering-/compile-time) gauge of which you speak.
> 
> No, I am speaking about a widget that checks and enforces measurement 
> units.

as am I

> If you look how GUI widgets are constructed you would notice 
> adjustment objects,

which should utilize the compile-time-enforced strongly-typed types, not unitless scalars

> events to propagate,

which should utilize the compile-time-enforced strongly-typed types, not unitless scalars

> properties to set and query, 

which should utilize the compile-time-enforced strongly-typed types, not unitless scalars

> MVC

which should utilize the compile-time-enforced strongly-typed types, not unitless scalars

> and dozens of other things

which should utilize the compile-time-enforced strongly-typed types, not unitless scalars

> connecting the widget to the world around 
> it, all dealing with measurement units. There is no way anybody could 
> design this with generics or statically typed.

So you can't use /this/ name instead of /that/ name of type.  Gee, your keyboard is so weird that it won't let you type /this/ strongly-typed identifier instead of /that/ weakly-typed identifier in app-domain declarations of instantiations.

> It can be statically constrained though, in some few cases, because 
> widgets are customary stored and restored. There might be some limited 
> cases with all static layouts in avionics or medical applications, these 
> are an exception from the common rule.

Safety-critical uses a different set of rules than “the common rule” of which you speak.

> And note that speed and pressure are measured in dozens different units. 

and they should all be supported, even ones that are out-of-vogue, such as CGS instead of MKS, and SI prefixes thereof

> One of the requirements of sane design is that all compatible units were 
> allowed. E.g. an adjustment object in kPa should work with a barograph 
> indicating mm Hg.

where “works with” is defined as having an overtly-instantiated converter object between them, where the converter object again assures compile-time physics-correct enforcement of strongly-typed input units of measure to strongly-typed output units of measure.  Indeed, in addition to providing all the customary conversions (e.g., MKS to CGS and vice versa), the library must provide a toolkit for the app-domain programmer to declare a few more conversions than supplied by the less-insightful library designer (e.g., even avoirdupois to metric and vice versa, Queen Anne 1707 system still in wide use in the USA to metric and vice versa,  King George III 1824 system in former use throughout the British Empire to metric and vice versa.

Just like the rule of not hardcoding a single iterator/cursor into a container, don't hardcode conversions or prohibitive lack thereof into the compile-time-enforced strong-typing units-of-measure dimension types.

> And I don't remember a single customer who ever wanted 
> his HMI showing speed in SI's m/s.

Why in the world would a GUI widget library dictate the requirements to the customer, as a tail wagging the dog?  The strongly-type GUI widget library should present a physics-correct plethora of options to the customer so that the customer speaks the language of the customer, not of some library designer (who sought effort reduction).  The purpose of engineering is to serve the customer's expectations, not to the library designer's whim.


^ permalink raw reply	[flat|nested] 32+ messages in thread

* Re: SI Units Checked and Unchecked
  2018-08-09 16:07 ` Jeffrey R. Carter
@ 2018-08-09 17:41   ` AdaMagica
  2018-08-09 20:34     ` Jeffrey R. Carter
  0 siblings, 1 reply; 32+ messages in thread
From: AdaMagica @ 2018-08-09 17:41 UTC (permalink / raw)


Am Donnerstag, 9. August 2018 18:07:25 UTC+2 schrieb Jeffrey R. Carter:
> Is this standard Ada 12, or is it GNAT specific?

Dynamic predicates are standard Ada 2012. But I have no other compiler than GNAT (if there is one at all for Ada 2012), so I cannot be sure. However I didn't find anything in the RM to the contrary.

I avoid all GNAT specifics.

^ permalink raw reply	[flat|nested] 32+ messages in thread

* Re: SI Units Checked and Unchecked
  2018-08-09 15:03     ` Dan'l Miller
  2018-08-09 15:51       ` Dmitry A. Kazakov
@ 2018-08-09 18:47       ` Paul Rubin
  2018-08-09 19:13         ` Dan'l Miller
  1 sibling, 1 reply; 32+ messages in thread
From: Paul Rubin @ 2018-08-09 18:47 UTC (permalink / raw)


"Dan'l Miller" <[email protected]> writes:
> Well, factually incorrect opinions like yours above would be the
> reason for losses similar to the Mars Climate Orbiter in the future,
> even if coded is so-called ‘safety-critical’ Ada.
>
> http://www.cnn.com/TECH/space/9909/30/mars.metric.02

It looks like traditional dimensional analysis wouldn't have helped with
that.  If you switch feet and meters, they are both units of length, so
have the same dimensions.

I get the impression that lots of space stuff is initially coded in
Matlab and then converted to Ada.  In those cases they probably expect
Matlab simulations to catch (some of) the bugs.

> Meticulous typing (especially compile-time enforcement of strong
> typing) is supposed to be Ada's crowning achievement; C++ or any
> recent upstart language (e.g., Rust) is not supposed to be able to
> threaten to usurp the throne from the king on typing-enforcement
> topics.

Ada's type system (due to its origins in the 1980s) is decades behind
current designs.  Ada handles the issue through good integration with
proof systems like SPARK.  That seems like a fine approach.

This exercise is probably doable in Ada though:

http://blog.tmorris.net/posts/understanding-practical-api-design-static-typing-and-functional-programming/

It was pretty easy in Haskell.

^ permalink raw reply	[flat|nested] 32+ messages in thread

* Re: SI Units Checked and Unchecked
  2018-08-09 18:47       ` Paul Rubin
@ 2018-08-09 19:13         ` Dan'l Miller
  0 siblings, 0 replies; 32+ messages in thread
From: Dan'l Miller @ 2018-08-09 19:13 UTC (permalink / raw)


On Thursday, August 9, 2018 at 1:47:15 PM UTC-5, Paul Rubin wrote:
> "Dan'l Miller" writes:
> > Well, factually incorrect opinions like yours above would be the
> > reason for losses similar to the Mars Climate Orbiter in the future,
> > even if coded is so-called ‘safety-critical’ Ada.
> >
> > http://www.cnn.com/TECH/space/9909/30/mars.metric.02
> 
> It looks like traditional

Apparently the “traditional” dimension type of which you speak is weakly typed as a fatal flaw, not strongly typed as I am consistently describing.  The USA's 1707 Queen Anne gallon (and fractions & multiples thereof:  quart, pint, cup, butt) would be strongly-typed as a different type than the 1824 King George so-called Imperial gallon (and fractions & multiples thereof:  Imperial quart, Imperial pint, Imperial cup, Imperial butt), which in turn would be strongly-typed as a different type than the SI liter (and SI prefixes thereof).  Likewise for every other strongly-type unit-of-measure in each widely-utilized system in each dimensionality.

> dimensional analysis wouldn't have helped with
> that.  If you switch feet and meters, they are both units of length, so
> have the same dimensions.

Then that should-have-been-strongly-typed units-of-measure library (or language feature) was maldesigned as merely a weakly-type dimension library (or language feature).

> I get the impression that lots of space stuff is initially coded in
> Matlab and then converted to Ada.  In those cases they probably expect
> Matlab simulations to catch (some of) the bugs.
> 
> > Meticulous typing (especially compile-time enforcement of strong
> > typing) is supposed to be Ada's crowning achievement; C++ or any
> > recent upstart language (e.g., Rust) is not supposed to be able to
> > threaten to usurp the throne from the king on typing-enforcement
> > topics.
> 
> Ada's type system (due to its origins in the 1980s) is decades behind
> current designs.  Ada handles the issue through good integration with
> proof systems like SPARK.

How precisely would SPARK subset & mark-up emulate a strongly-typed units-of-measure capabilities that I describe to catch mixing scalars •implicitly• containing 1707 Queen Anne units of measure or avoirdupois units of measure with scalars •implicitly• containing SI/MKS/CGS units of measure?  That seems quite a stretch for SPARK subset & markup alone to automagically have almost AI-esque ESP insight into what the human-being's meaning of the scalar datum's bits actually semantically mean (without the strongly-typed per-unit-of-measure types that I describe).  Any markup for SPARK to have that deep of a level of insight would be tantamount to a strongly-type units-of-measure library/language-feature capability that would overtly call out Queen Anne's 1707 gallon versus King George III's 1824 gallon versus SI's liter, as I consistently describe.

^ permalink raw reply	[flat|nested] 32+ messages in thread

* Re: SI Units Checked and Unchecked
  2018-08-09 17:32         ` Dan'l Miller
@ 2018-08-09 19:42           ` Dmitry A. Kazakov
  2018-08-09 22:12             ` Dan'l Miller
  0 siblings, 1 reply; 32+ messages in thread
From: Dmitry A. Kazakov @ 2018-08-09 19:42 UTC (permalink / raw)


On 2018-08-09 19:32, Dan'l Miller wrote:
> On Thursday, August 9, 2018 at 10:51:59 AM UTC-5, Dmitry A. Kazakov wrote:
>> On 2018-08-09 17:03, Dan'l Miller wrote:
>>
>>> So, Dmitry, you are making the mistake of excessive reuse in the app-domain of an unfinished library.
>>> Sure, at some deep level in the library, there can be a bland gauge that skeuomorphically represents a > > swinging black needle on a white circle that has no idea whether it is measuring pressure or amperes
>>> or volts or speed.  But at the intended user-interface facade of the library, there should be:
>>> 1) a strongly-typed gauge for amperes,
>>> 2) a separate strongly-typed gauge for pressure,
>>> 3) a separate strongly-typed gauge for volts,
>>> 4) a separate strongly-typed gauge for speed,
>>> and so forth that are wrappers around the one shared white circle with swinging black needle as the
>>> bland unitless-clueless(-at-engineering-/compile-time) gauge of which you speak.
>>
>> No, I am speaking about a widget that checks and enforces measurement
>> units.
> 
> as am I
> 
>> If you look how GUI widgets are constructed you would notice
>> adjustment objects,
> 
> which should utilize the compile-time-enforced strongly-typed types, not unitless scalars

The scalars are not unitless. The unit is a discriminant:

    http://www.dmitry-kazakov.de/ada/units.htm

The point is that like in the design proposed by Christoph the 
constraint is not static.

[...]

>> connecting the widget to the world around
>> it, all dealing with measurement units. There is no way anybody could
>> design this with generics or statically typed.
> 
> So you can't use /this/ name instead of /that/ name of type.  Gee, your keyboard is so weird that it won't let you type /this/ strongly-typed identifier instead of /that/ weakly-typed identifier in app-domain declarations of instantiations.

There is no usable design based on unrelated types [*]. There must exist 
dimensioned objects capable to hold values of different units. Similarly 
to class-wide objects this by no means constitutes weak typing.

>> One of the requirements of sane design is that all compatible units were
>> allowed. E.g. an adjustment object in kPa should work with a barograph
>> indicating mm Hg.
> 
> where “works with” is defined as having an overtly-instantiated converter object between them, where the converter object again assures compile-time physics-correct enforcement of strongly-typed input units of measure to strongly-typed output units of measure.

No converter objects needed. Operations are defined directly on the 
dimensioned values. You can add 5 m/s to 10 km/h, the result is always 
physically correct.

This design has its drawbacks, e.g. it would prevent use of fixed-point 
types, because you would lose control over precision.

> Just like the rule of not hardcoding a single iterator/cursor into a container, don't hardcode conversions or prohibitive lack thereof into the compile-time-enforced strong-typing units-of-measure dimension types.

As I said there no hard-coded conversions whatsoever.

>> And I don't remember a single customer who ever wanted
>> his HMI showing speed in SI's m/s.
> 
> Why in the world would a GUI widget library dictate the requirements to the customer, as a tail wagging the dog?

Right. That is why the measurement unit of a widget cannot be a part of 
its type and why the widgets cannot deploy a fixed system of units.

> The strongly-type GUI widget library should present a physics-correct plethora of options to the customer so that the customer speaks the language of the customer, not of some library designer (who sought effort reduction).  The purpose of engineering is to serve the customer's expectations, not to the library designer's whim.

That is one of the requirements, which BTW precludes type-based 
solutions. All production code used in automation systems is based on 
subtypes.

----------------------
* Note that dimensioned types could build a class. Then they would be 
related and there would be class-wide objects to hold values of any 
dimension. This sort of design is thinkable, but it would possibly 
require even deeper changes of the Ada type system than a design based 
on subtypes/constraints.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

^ permalink raw reply	[flat|nested] 32+ messages in thread

* Re: SI Units Checked and Unchecked
  2018-08-09 17:41   ` AdaMagica
@ 2018-08-09 20:34     ` Jeffrey R. Carter
  2018-08-10  9:13       ` AdaMagica
  0 siblings, 1 reply; 32+ messages in thread
From: Jeffrey R. Carter @ 2018-08-09 20:34 UTC (permalink / raw)


On 08/09/2018 07:41 PM, AdaMagica wrote:
> Am Donnerstag, 9. August 2018 18:07:25 UTC+2 schrieb Jeffrey R. Carter:
>> Is this standard Ada 12, or is it GNAT specific?
> 
> Dynamic predicates are standard Ada 2012. But I have no other compiler than GNAT (if there is one at all for Ada 2012), so I cannot be sure. However I didn't find anything in the RM to the contrary.
> 
> I avoid all GNAT specifics.

Yes, GNAT is the only Ada-12 compiler. I am unable to access your web site, so I 
can't look at the code, but am curious about how it's implemented. IIRC, AdaCore 
has a similar capability, so I wondered if yours offered greater portability 
than theirs.

-- 
Jeff Carter
"I was in love with a beautiful blonde once, dear.
She drove me to drink. That's the one thing I'm
indebted to her for."
Never Give a Sucker an Even Break
109

^ permalink raw reply	[flat|nested] 32+ messages in thread

* Re: SI Units Checked and Unchecked
  2018-08-09 19:42           ` Dmitry A. Kazakov
@ 2018-08-09 22:12             ` Dan'l Miller
  2018-08-10  6:45               ` Dmitry A. Kazakov
  0 siblings, 1 reply; 32+ messages in thread
From: Dan'l Miller @ 2018-08-09 22:12 UTC (permalink / raw)


On Thursday, August 9, 2018 at 2:42:47 PM UTC-5, Dmitry A. Kazakov wrote:
> On 2018-08-09 19:32, Dan'l Miller wrote:
> > On Thursday, August 9, 2018 at 10:51:59 AM UTC-5, Dmitry A. Kazakov wrote:
> >> On 2018-08-09 17:03, Dan'l Miller wrote:
> >>
> >>> So, Dmitry, you are making the mistake of excessive reuse in the app-domain of an unfinished library.
> >>> Sure, at some deep level in the library, there can be a bland gauge that skeuomorphically represents
> >>> a swinging black needle on a white circle that has no idea whether it is measuring pressure or
> >>> amperes or volts or speed.  But at the intended user-interface facade of the library, there should be:
> >>> 1) a strongly-typed gauge for amperes,
> >>> 2) a separate strongly-typed gauge for pressure,
> >>> 3) a separate strongly-typed gauge for volts,
> >>> 4) a separate strongly-typed gauge for speed,
> >>> and so forth that are wrappers around the one shared white circle with swinging black needle as the
> >>> bland unitless-clueless(-at-engineering-/compile-time) gauge of which you speak.
> >>
> >> No, I am speaking about a widget that checks and enforces measurement
> >> units.
> > 
> > as am I

Actually, I am talking about compile-time checks within Ada source code for a gauge as would be utilized on the GUI control screen of a chemical plant or a nuclear reactor, not some toy string-processing app that is the analogue of GNU Units.

> >> If you look how GUI widgets are constructed you would notice
> >> adjustment objects,
> > 
> > which should utilize the compile-time-enforced strongly-typed types, not unitless scalars
> 
> The scalars are not unitless. The unit is a discriminant:
> 
>     http://www.dmitry-kazakov.de/ada/units.htm

It looks like a string-processing library to support a toy units converter app, which is the X Window analogue of GNU Units*.  This doesn't look at all like compile-time units-of-measure enforcement via strong-typing.  A mere string-processing interpreter helping the UI/UX level is missing the •entire• point of this whole thread, including the OPer's OPing.  This mere string-processing interpreter thoroughly misses the entire point of strong typing each scalar datum in throughout all millions of lines of Ada source code of a compiled imperative programming language in a large software-controls-hardware-within-a-physics-device product.

Dmitry, this work is impressive for what it is, but a string-processing toy unit-conversion calculator is far far off-topic (as is GNU Units* too).

* https://en.wikipedia.org/wiki/GNU_Units

> The point is that like in the design proposed by Christoph the 
> constraint is not static.
> 
> [...]
> 
> >> connecting the widget to the world around
> >> it, all dealing with measurement units. There is no way anybody could
> >> design this with generics or statically typed.
> > 
> > So you can't use /this/ name instead of /that/ name of type.  Gee, your keyboard is so weird that it
> > won't let you type /this/ strongly-typed identifier instead of /that/ weakly-typed identifier in
> > app-domain declarations of instantiations.
> 
> There is no usable design based on unrelated types [*]. There must exist 
> dimensioned objects capable to hold values of different units. Similarly 
> to class-wide objects this by no means constitutes weak typing.
> 
> >> One of the requirements of sane design is that all compatible units were
> >> allowed. E.g. an adjustment object in kPa should work with a barograph
> >> indicating mm Hg.
> > 
> > where “works with” is defined as having an overtly-instantiated converter object between them, where
> > the converter object again assures compile-time physics-correct enforcement of strongly-typed input
> > units of measure to strongly-typed output units of measure.
> 
> No converter objects needed. Operations are defined directly on the 
> dimensioned values. You can add 5 m/s to 10 km/h, the result is always 
> physically correct.
> 
> This design has its drawbacks, e.g. it would prevent use of fixed-point 
> types, because you would lose control over precision.
> 
> > Just like the rule of not hardcoding a single iterator/cursor into a container, don't hardcode
> > conversions or prohibitive lack thereof into the compile-time-enforced strong-typing units-of-measure
> > dimension types.
> 
> As I said there no hard-coded conversions whatsoever.
> 
> >> And I don't remember a single customer who ever wanted
> >> his HMI showing speed in SI's m/s.
> > 
> > Why in the world would a GUI widget library dictate the requirements to the customer, as a tail
> > wagging the dog?
> 
> Right. That is why the measurement unit of a widget cannot be a part of 
> its type and why the widgets cannot deploy a fixed system of units.
> 
> > The strongly-type GUI widget library should present a physics-correct plethora of options to the
> > customer so that the customer speaks the language of the customer, not of some library designer
> > (who sought effort reduction).  The purpose of engineering is to serve the customer's expectations,
> > not to the library designer's whim.
> 
> That is one of the requirements, which BTW precludes type-based 
> solutions. All production code used in automation systems is based on 
> subtypes.
> 
> ----------------------
> * Note that dimensioned types could build a class. Then they would be 
> related and there would be class-wide objects to hold values of any 
> dimension. This sort of design is thinkable, but it would possibly 
> require even deeper changes of the Ada type system than a design based 
> on subtypes/constraints.
> 
> -- 
> Regards,
> Dmitry A. Kazakov
> http://www.dmitry-kazakov.de


^ permalink raw reply	[flat|nested] 32+ messages in thread

* Re: SI Units Checked and Unchecked
  2018-08-09 22:12             ` Dan'l Miller
@ 2018-08-10  6:45               ` Dmitry A. Kazakov
  2018-08-10 13:59                 ` Dan'l Miller
  0 siblings, 1 reply; 32+ messages in thread
From: Dmitry A. Kazakov @ 2018-08-10  6:45 UTC (permalink / raw)


On 2018-08-10 00:12, Dan'l Miller wrote:

> Actually, I am talking about compile-time checks within Ada source code for a gauge as would be utilized on the GUI control screen of a chemical plant or a nuclear reactor, not some toy string-processing app that is the analogue of GNU Units.

As I explained this design is technically not viable. Even taking an 
insanely huge overhead of making all components generic with measurement 
unit as a formal parameter, that would be less safe than a design based 
on constraints. With generics you can only pass same actual parameter or 
use a generic instance as a parameter, you cannot constraint generic 
instances in a way the algebra of measurement units works, e.g. length 
divided to time gives speed. So you will end up with generic instances 
for each particular unit but no mechanism to combine instances (of 
different generic types) in a unit-safe way. It will be in effect 
*untyped*. (Which is does not really matter since internal mechanisms 
like queuing of events, callbacks etc cannot be made generic anyway.)

Compile-time unit checks can only be used in some numeric problems, for 
instance in the control loop. Everywhere else checks are run-time, which 
in case of widgets does not mean any real safety loss because 
practically all these checks are done upon initialization. When you 
create a gauge you connect a signal from a slider widget to it. Doing so 
the units of the gauge and of the slider's signal get checked. That 
happens once before the system starts. If you use a GUI design tool then 
this check could be performed even earlier before deployment. Chances of 
getting a run-time check fail are zero.

>> The scalars are not unitless. The unit is a discriminant:
>>
>>      http://www.dmitry-kazakov.de/ada/units.htm
> 
> It looks like a string-processing library to support a toy units converter app,

No string processing involved. It is same as saying that Integer is 
string processing because there exists Integer'Image.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

^ permalink raw reply	[flat|nested] 32+ messages in thread

* Re: SI Units Checked and Unchecked
  2018-08-09 20:34     ` Jeffrey R. Carter
@ 2018-08-10  9:13       ` AdaMagica
  2018-08-10 20:20         ` Jeffrey R. Carter
  0 siblings, 1 reply; 32+ messages in thread
From: AdaMagica @ 2018-08-10  9:13 UTC (permalink / raw)


Am Donnerstag, 9. August 2018 22:34:05 UTC+2 schrieb Jeffrey R. Carter:
> Yes, GNAT is the only Ada-12 compiler. I am unable to access your web site, so I 
> can't look at the code, but am curious about how it's implemented. IIRC, AdaCore 
> has a similar capability, so I wondered if yours offered greater portability 
> than theirs.

That's a pity. If you're interested in the code, just email me and we can find a way.

christ(m)usch.grein(a)t(m)online.de
replace (m) by -, (a) by @



^ permalink raw reply	[flat|nested] 32+ messages in thread

* Re: SI Units Checked and Unchecked
  2018-08-10  6:45               ` Dmitry A. Kazakov
@ 2018-08-10 13:59                 ` Dan'l Miller
  2018-08-10 14:50                   ` Dmitry A. Kazakov
  0 siblings, 1 reply; 32+ messages in thread
From: Dan'l Miller @ 2018-08-10 13:59 UTC (permalink / raw)


On Friday, August 10, 2018 at 1:45:47 AM UTC-5, Dmitry A. Kazakov wrote:
> On 2018-08-10 00:12, Dan'l Miller wrote:
> 
> > Actually, I am talking about compile-time checks within Ada source code for a gauge as would be utilized on the GUI control screen of a chemical plant or a nuclear reactor, not some toy string-processing app that is the analogue of GNU Units.
> 
> As I explained this design is technically not viable.

in today's Ada.

> Even taking an 
> insanely huge overhead of making all components generic with measurement 
> unit as a formal parameter, that would be less safe than a design based 
> on constraints. With generics you can only pass same actual parameter or 
> use a generic instance as a parameter, you cannot constraint generic 
> instances in a way the algebra of measurement units works, e.g. length 
> divided to time gives speed. So you will end up with generic instances 
> for each particular unit but no mechanism to combine instances (of 
> different generic types) in a unit-safe way. It will be in effect 
> *untyped*. (Which is does not really matter since internal mechanisms 
> like queuing of events, callbacks etc cannot be made generic anyway.)
> 
> Compile-time unit checks can only be used in some numeric problems, for 
> instance in the control loop. Everywhere else checks are run-time, which 
> in case of widgets does not mean any real safety loss because 
> practically all these checks are done upon initialization. When you 
> create a gauge you connect a signal from a slider widget to it. Doing so 
> the units of the gauge and of the slider's signal get checked. That 
> happens once before the system starts. If you use a GUI design tool then 
> this check could be performed even earlier before deployment. Chances of 
> getting a run-time check fail are zero.
> 
> >> The scalars are not unitless. The unit is a discriminant:
> >>
> >>      http://www.dmitry-kazakov.de/ada/units.htm
> > 
> > It looks like a string-processing library to support a toy units converter app,
> 
> No string processing involved. It is same as saying that Integer is 
> string processing because there exists Integer'Image.
> 
> -- 
> Regards,
> Dmitry A. Kazakov
> http://www.dmitry-kazakov.de


^ permalink raw reply	[flat|nested] 32+ messages in thread

* Re: SI Units Checked and Unchecked
  2018-08-10 13:59                 ` Dan'l Miller
@ 2018-08-10 14:50                   ` Dmitry A. Kazakov
  2018-08-10 17:04                     ` Dan'l Miller
  0 siblings, 1 reply; 32+ messages in thread
From: Dmitry A. Kazakov @ 2018-08-10 14:50 UTC (permalink / raw)


On 2018-08-10 15:59, Dan'l Miller wrote:
> On Friday, August 10, 2018 at 1:45:47 AM UTC-5, Dmitry A. Kazakov wrote:
>> On 2018-08-10 00:12, Dan'l Miller wrote:
>>
>>> Actually, I am talking about compile-time checks within Ada source code for a gauge as would be utilized on the GUI control screen of a chemical plant or a nuclear reactor, not some toy string-processing app that is the analogue of GNU Units.
>>
>> As I explained this design is technically not viable.
> 
> in today's Ada.

In any Ada. Either way, classes of dimensioned object built as subtypes 
with the unit being a constraint or as related types with the unit being 
the type tag, most designs will use subtype- or class-wide objects.

We need a type system capable of static checks when constraints or tags 
are statically known, a way to convert "Unit_Error may be raised" into 
hard type error.

Then we will have both static checks and zero run-time overhead in 
static cases and fallback to dynamic checks in class-wide cases.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de


^ permalink raw reply	[flat|nested] 32+ messages in thread

* Re: SI Units Checked and Unchecked
  2018-08-10 14:50                   ` Dmitry A. Kazakov
@ 2018-08-10 17:04                     ` Dan'l Miller
  2018-08-10 17:34                       ` Dmitry A. Kazakov
  0 siblings, 1 reply; 32+ messages in thread
From: Dan'l Miller @ 2018-08-10 17:04 UTC (permalink / raw)


On Friday, August 10, 2018 at 9:50:53 AM UTC-5, Dmitry A. Kazakov wrote:
> On 2018-08-10 15:59, Dan'l Miller wrote:
> > On Friday, August 10, 2018 at 1:45:47 AM UTC-5, Dmitry A. Kazakov wrote:
> >> On 2018-08-10 00:12, Dan'l Miller wrote:
> >>
> >>> Actually, I am talking about compile-time checks within Ada source code for a gauge as would be
> >>> utilized on the GUI control screen of a chemical plant or a nuclear reactor, not some toy string
> >>> processing app that is the analogue of GNU Units.
> >>
> >> As I explained this design is technically not viable.
> > 
> > in today's Ada.
> 
> … Either way, classes of dimensioned object built as subtypes 
> with the unit being a constraint or as related types with the unit being 
> the type tag, most designs will use subtype- or class-wide objects.
> 
> We need a type system capable of static checks when constraints or tags 
> are statically known, a way to convert "Unit_Error may be raised" into 
> hard type error.

Well, now there is something that we can agree on.

> Then we will have both static checks and zero run-time overhead in 
> static cases and fallback to dynamic checks in class-wide cases.

I take it …

> In any Ada.

… that you don't think that “Then we … class-wide cases” sentence is achievable at all in any derivative of Ada due to some fundamental flaw in Ada, and that a significantly not-Ada language is the only hope of achieving that sentence.  Why so?

^ permalink raw reply	[flat|nested] 32+ messages in thread

* Re: SI Units Checked and Unchecked
  2018-08-10 17:04                     ` Dan'l Miller
@ 2018-08-10 17:34                       ` Dmitry A. Kazakov
  2018-08-11  4:42                         ` Paul Rubin
  0 siblings, 1 reply; 32+ messages in thread
From: Dmitry A. Kazakov @ 2018-08-10 17:34 UTC (permalink / raw)


On 2018-08-10 19:04, Dan'l Miller wrote:
> On Friday, August 10, 2018 at 9:50:53 AM UTC-5, Dmitry A. Kazakov wrote:

>> In any Ada.
> 
> … that you don't think that “Then we … class-wide cases” sentence is achievable at all in any derivative of Ada due to some fundamental flaw in Ada, and that a significantly not-Ada language is the only hope of achieving that sentence.  Why so?

No language change can make dynamic cases static.

What the language can is to make dynamic cases type-safe, which Ada 
already does.

Where Ada fails is in smooth transition between dynamic and static and 
support for user-defined semantics in static cases. E.g. in order to 
handle units statically we need user-defined static operations to 
compute the constraint of the result from the constraints of the 
arguments in dimensioned numeric operations. We need a mechanism to 
split an operation like "/" into a static part that computes the new 
constraint (unit) and a dynamic part that computes the value.

This is a much more general issue than measurement units. The same thing 
is required to have static initialization of objects like constant 
look-up tables and maps, components of records, array elements. This is 
why I keep on saying that it is not about an AI on measurements units, 
it is about empowering the type system to make it capable to express 
complex structures like dimensioned types.

ARG should take the problem seriously. See where ad-hoc hacking the 
language led us. Dynamic predicates and expression functions do not 
solve the problem yet significantly damaged the language. Ada 2020 will 
have array initialization constructs. The price of hacking.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de


^ permalink raw reply	[flat|nested] 32+ messages in thread

* Re: SI Units Checked and Unchecked
  2018-08-10  9:13       ` AdaMagica
@ 2018-08-10 20:20         ` Jeffrey R. Carter
  2018-08-13  8:57           ` AdaMagica
  0 siblings, 1 reply; 32+ messages in thread
From: Jeffrey R. Carter @ 2018-08-10 20:20 UTC (permalink / raw)


On 08/10/2018 11:13 AM, AdaMagica wrote:
> 
> That's a pity. If you're interested in the code, just email me and we can find a way.

I was able to look at it today. Other than the checks being done by the 
predicates rather than manually, and the string parsing, it doesn't seem too 
different from the discriminant version I used over 20 yrs ago in Ada 83.

-- 
Jeff Carter
"I wave my private parts at your aunties."
Monty Python & the Holy Grail
13

^ permalink raw reply	[flat|nested] 32+ messages in thread

* Re: SI Units Checked and Unchecked
  2018-08-10 17:34                       ` Dmitry A. Kazakov
@ 2018-08-11  4:42                         ` Paul Rubin
  2018-08-11  5:46                           ` Dmitry A. Kazakov
  0 siblings, 1 reply; 32+ messages in thread
From: Paul Rubin @ 2018-08-11  4:42 UTC (permalink / raw)


"Dmitry A. Kazakov" <[email protected]> writes:
> No language change can make dynamic cases static.

I think the idea is to allow constraints on generic instantiation
precise enough to use them for unit checking.

It looks like they added a watered-down version of concepts and
constraints to C++20: https://en.cppreference.com/w/cpp/language/constraints

This kind of thing can be done more fundamentally in dependently typed
languages, but I get the impression that it's still an impractical
academic exercise.

^ permalink raw reply	[flat|nested] 32+ messages in thread

* Re: SI Units Checked and Unchecked
  2018-08-11  4:42                         ` Paul Rubin
@ 2018-08-11  5:46                           ` Dmitry A. Kazakov
  2018-08-11 19:57                             ` Paul Rubin
  0 siblings, 1 reply; 32+ messages in thread
From: Dmitry A. Kazakov @ 2018-08-11  5:46 UTC (permalink / raw)


On 2018-08-11 06:42, Paul Rubin wrote:
> "Dmitry A. Kazakov" <[email protected]> writes:
>> No language change can make dynamic cases static.
> 
> I think the idea is to allow constraints on generic instantiation
> precise enough to use them for unit checking.

Dynamic is not static.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de


^ permalink raw reply	[flat|nested] 32+ messages in thread

* Re: SI Units Checked and Unchecked
  2018-08-11  5:46                           ` Dmitry A. Kazakov
@ 2018-08-11 19:57                             ` Paul Rubin
  2018-08-11 21:01                               ` Dmitry A. Kazakov
  0 siblings, 1 reply; 32+ messages in thread
From: Paul Rubin @ 2018-08-11 19:57 UTC (permalink / raw)


"Dmitry A. Kazakov" <[email protected]> writes:
>>> No language change can make dynamic cases static.
>> I think the idea is to allow constraints on generic instantiation
>> precise enough to use them for unit checking.
> Dynamic is not static.

Well the idea is to check the constraints statically.  Obviously in
cases where values can be introduced at runtime, there must be a way to
connect them up with units, through protected methods or whatever.
Once they are in the system, the types track them.

I don't understand why there is even a desire in a scientific-style
program to track quantities in more than one dimensionally equivalent
unit (e.g. liters vs gallons).  Just convert everything to a uniform set
of units (probably SI) when they come into the system, and then do all
internal calculations with that unit set.


^ permalink raw reply	[flat|nested] 32+ messages in thread

* Re: SI Units Checked and Unchecked
  2018-08-11 19:57                             ` Paul Rubin
@ 2018-08-11 21:01                               ` Dmitry A. Kazakov
  0 siblings, 0 replies; 32+ messages in thread
From: Dmitry A. Kazakov @ 2018-08-11 21:01 UTC (permalink / raw)


On 2018-08-11 21:57, Paul Rubin wrote:
> "Dmitry A. Kazakov" <[email protected]> writes:
>>>> No language change can make dynamic cases static.
>>> I think the idea is to allow constraints on generic instantiation
>>> precise enough to use them for unit checking.
>> Dynamic is not static.
> 
> Well the idea is to check the constraints statically.

The constraints are not static.

> Obviously in
> cases where values can be introduced at runtime, there must be a way to
> connect them up with units, through protected methods or whatever.
> Once they are in the system, the types track them.

Tracking is a run-time action. If you know units statically you don't 
need to track them. In most cases as a value propagates the system it 
crosses barriers when one or another side does not know the unit. 
Reading a measurement value is only the first such barrier.

> I don't understand why there is even a desire in a scientific-style
> program to track quantities in more than one dimensionally equivalent
> unit (e.g. liters vs gallons).

Because it is a requirement. When designing an automation and control 
system, you have an HMI, which must show gallons because the operator 
wants to see gallons. The fuel flow measurement system may use liters 
per hour. The network protocol to transport measurement data will use a 
SI unit etc. No installation I ever saw used strictly SI units. Even in 
Europe temperature is reported in Celsius degree, speed is in km/s, 
inclination is in crazy percents of tangent. Who ever used ks instead of 
hour?

> Just convert everything to a uniform set
> of units (probably SI) when they come into the system, and then do all
> internal calculations with that unit set.

What calculations you mean? The calculations used in the controlling 
loop is well under 5% of all code and this is the only part that could 
have statically known units. Even that is not fully true because things 
like restbus simulation, computable user-defined channels do not have 
statically known units. Any other calculations used in logging, 
databases, interfacing the ERP, reporting, health monitoring, 
plausibility checking and hell knows other components deal with dynamic 
units. And all the non-calculating rest is dynamic too.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

^ permalink raw reply	[flat|nested] 32+ messages in thread

* Re: SI Units Checked and Unchecked
  2018-08-10 20:20         ` Jeffrey R. Carter
@ 2018-08-13  8:57           ` AdaMagica
  2018-08-20 17:55             ` AdaMagica
  0 siblings, 1 reply; 32+ messages in thread
From: AdaMagica @ 2018-08-13  8:57 UTC (permalink / raw)


Am Freitag, 10. August 2018 22:20:12 UTC+2 schrieb Jeffrey R. Carter:
> I was able to look at it today. Other than the checks being done by the 
> predicates rather than manually, and the string parsing, it doesn't seem too 
> different from the discriminant version I used over 20 yrs ago in Ada 83.

That's correct. I like the GNAT method principally how it works with units. What I absolutely dislike is that (since Ada is case insensitive) they invent new unit and prefix symbols. Their dimensioned text output (they call it IO, which is a lie) is catastrophic. see
http://www.christ-usch-grein.homepage.t-online.de/Ada/Dimension/Physical_units_with_GNAT_GPL_2013-AUJ35.1.pdf

All this is corrected in my design. If these ideas could influence the GNAT method, this would be ideal. But there does not seem to be much interest in the method by their clients since nothing has changed since 2013.


^ permalink raw reply	[flat|nested] 32+ messages in thread

* Re: SI Units Checked and Unchecked
  2018-08-13  8:57           ` AdaMagica
@ 2018-08-20 17:55             ` AdaMagica
  0 siblings, 0 replies; 32+ messages in thread
From: AdaMagica @ 2018-08-20 17:55 UTC (permalink / raw)


A bug fix and complete documentation has been added


^ permalink raw reply	[flat|nested] 32+ messages in thread

* Re: SI Units Checked and Unchecked
  2018-08-09 12:44 SI Units Checked and Unchecked AdaMagica
  2018-08-09 13:47 ` Dan'l Miller
  2018-08-09 16:07 ` Jeffrey R. Carter
@ 2019-09-04 14:20 ` Shark8
  2019-09-04 17:11   ` AdaMagica
  2 siblings, 1 reply; 32+ messages in thread
From: Shark8 @ 2019-09-04 14:20 UTC (permalink / raw)


On Thursday, August 9, 2018 at 6:44:13 AM UTC-6, AdaMagica wrote:
> This is a complete rework using Ada 2012 predicates.
> 
> […]
> 
> Download from here:
> http://www.christ-usch-grein.homepage.t-online.de/Ada/Dimension/SI.html
> 
> If you should use (even like) this method, please drop me a note with your findings.
> 
> Have fun.
> Christoph

I am working on a project that will make use of SI (FITS file format, specifically the tagged metadata). I have a copy of the zip but as yet haven't gotten to the point where I can integrate SI into the project; however, the site appears to be down.


^ permalink raw reply	[flat|nested] 32+ messages in thread

* Re: SI Units Checked and Unchecked
  2019-09-04 14:20 ` Shark8
@ 2019-09-04 17:11   ` AdaMagica
  2019-09-06 21:01     ` Shark8
  0 siblings, 1 reply; 32+ messages in thread
From: AdaMagica @ 2019-09-04 17:11 UTC (permalink / raw)


Am Mittwoch, 4. September 2019 16:20:04 UTC+2 schrieb Shark8:
> ... the site appears to be down.

As I have been in retirement for 8 years now, I've closed my homepage. The few things I deemed to be worth to preserve have been put by courtesy of Randy at this place:

https://www.adaic.org/ada-resources/tools-libraries/

(see Christoph Grein’s Essentials).

Ths SI units package you are looking for (linked from the URL above) is here:

http://archive.adaic.com/tools/CKWG/Dimension/SI.html

My Ada Magica column is here (Förderverein Ada Deutschland):

https://www.ada-deutschland.de/sites/default/files/AdaTourCD/AdaTourCD2004/Ada%20Magica/Contents.html

^ permalink raw reply	[flat|nested] 32+ messages in thread

* Re: SI Units Checked and Unchecked
  2019-09-04 17:11   ` AdaMagica
@ 2019-09-06 21:01     ` Shark8
  2020-08-13 12:24       ` SI Units Checked and Unchecked - Completela overhauled version AdaMagica
  0 siblings, 1 reply; 32+ messages in thread
From: Shark8 @ 2019-09-06 21:01 UTC (permalink / raw)


On Wednesday, September 4, 2019 at 11:11:16 AM UTC-6, AdaMagica wrote:
> Am Mittwoch, 4. September 2019 16:20:04 UTC+2 schrieb Shark8:
> > ... the site appears to be down.
> 
> As I have been in retirement for 8 years now, I've closed my homepage. The few things I deemed to be worth to preserve have been put by courtesy of Randy at this place:
> 
> https://www.adaic.org/ada-resources/tools-libraries/
> 
> (see Christoph Grein’s Essentials).
> 
> Ths SI units package you are looking for (linked from the URL above) is here:
> 
> http://archive.adaic.com/tools/CKWG/Dimension/SI.html
> 
> My Ada Magica column is here (Förderverein Ada Deutschland):
> 
> https://www.ada-deutschland.de/sites/default/files/AdaTourCD/AdaTourCD2004/Ada%20Magica/Contents.html

Thank you for the links, as well as the work on the SI units.
Browsing around, it looks like a lot of the library can be made Pure, with the exception of the irritating provision/prohibition of "statically composed compound constants" that appeared in the "Why can't objects be static in Ada?" thread: https://groups.google.com/forum/#!msg/comp.lang.ada/8dMIIAOV7YQ/sscqy-tlCQAJ — I think your SI-Units library is an extremely good motivating example of *WHY* this needs to be changed, and will push for this change in the upcoming meeting of the ARG. (Indeed, changing this limitation is orders of magnitude more useful than adding square-brackets.)

BTW
Are there any tips, in particular for using the library?


^ permalink raw reply	[flat|nested] 32+ messages in thread

* SI Units Checked and Unchecked - Completela overhauled version
  2019-09-06 21:01     ` Shark8
@ 2020-08-13 12:24       ` AdaMagica
  0 siblings, 0 replies; 32+ messages in thread
From: AdaMagica @ 2020-08-13 12:24 UTC (permalink / raw)


Simplified design now available:
http://archive.adaic.com/tools/CKWG/Dimension/SI.html 
The choice of using dimension checking or not is now made via a generic signature package. The user interface is unchanged.

^ permalink raw reply	[flat|nested] 32+ messages in thread

end of thread, back to index

Thread overview: 32+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2018-08-09 12:44 SI Units Checked and Unchecked AdaMagica
2018-08-09 13:47 ` Dan'l Miller
2018-08-09 14:07   ` Dmitry A. Kazakov
2018-08-09 15:03     ` Dan'l Miller
2018-08-09 15:51       ` Dmitry A. Kazakov
2018-08-09 17:32         ` Dan'l Miller
2018-08-09 19:42           ` Dmitry A. Kazakov
2018-08-09 22:12             ` Dan'l Miller
2018-08-10  6:45               ` Dmitry A. Kazakov
2018-08-10 13:59                 ` Dan'l Miller
2018-08-10 14:50                   ` Dmitry A. Kazakov
2018-08-10 17:04                     ` Dan'l Miller
2018-08-10 17:34                       ` Dmitry A. Kazakov
2018-08-11  4:42                         ` Paul Rubin
2018-08-11  5:46                           ` Dmitry A. Kazakov
2018-08-11 19:57                             ` Paul Rubin
2018-08-11 21:01                               ` Dmitry A. Kazakov
2018-08-09 18:47       ` Paul Rubin
2018-08-09 19:13         ` Dan'l Miller
2018-08-09 14:31   ` AdaMagica
2018-08-09 15:19     ` Dan'l Miller
2018-08-09 16:07 ` Jeffrey R. Carter
2018-08-09 17:41   ` AdaMagica
2018-08-09 20:34     ` Jeffrey R. Carter
2018-08-10  9:13       ` AdaMagica
2018-08-10 20:20         ` Jeffrey R. Carter
2018-08-13  8:57           ` AdaMagica
2018-08-20 17:55             ` AdaMagica
2019-09-04 14:20 ` Shark8
2019-09-04 17:11   ` AdaMagica
2019-09-06 21:01     ` Shark8
2020-08-13 12:24       ` SI Units Checked and Unchecked - Completela overhauled version AdaMagica

comp.lang.ada

Archives are clonable: git clone --mirror https://archive.legitdata.co/comp.lang.ada

Example config snippet for mirrors


AGPL code for this site: git clone https://public-inbox.org/public-inbox.git