Re: SI Units Checked and Unchecked

["Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>]

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