On Fri, 5 Apr 2013, Dmitry A. Kazakov wrote:

> On Fri, 5 Apr 2013 16:44:53 +0200, Stefan.Lucks@uni-weimar.de wrote:

>> But the same is true for N and Z: every in Z has an additive inverse, but
>> not every number in N. If the non-existence of a multiplicative inverse
>> would justify different root types for Z and R, why should the
>> non-existence of an additive inverse not justify different root types for
>> N and Z (Universal_Positive versus Universal_Integer).
>
> That depends solely on the application domain.

Ada is a general-purpose language. We are discussing Ada's type concept 
and not any specific application, so there is not "the application domain" 
anything could possibly depend on.

>> As it turns out, the fact that Naturals and Positives have the same
>> representation as Integers, while Float has a different one, matters more
>> than any "mathematical structure" ...
>
> Nope, representation never matter. Employee ID and task ID may have same
> representation. That does not mean anything. Nominal type equivalence was a
> corner stone of Ada design.

Dmitry, I admire your ability to make some correct claim, being out of 
topic, and then pretending that this claim makes your point! ;-)

Sure, one of the main strengths of Ada from its beginning is allowing the 
programmer to define different and intentionally incompatible types with 
identical representations.

But you are actually proposing the opposite: Making different types with 
different representations intentionally compatible by introducing some 
universal super-type and then formally deriving the different types from 
the super-type.

Actually another corner stone of Ada has been the language designers' 
reluctance to introduce implicit conversions between types with different 
representations. Sure, some cases where implicit conversions take place 
exist, but only very few. One example is the conversion of constants of 
type Universal_Something into the right type.



------  I  love  the  taste  of  Cryptanalysis  in  the morning!  ------
     <http://www.uni-weimar.de/cms/medien/mediensicherheit/home.html>
--Stefan.Lucks (at) uni-weimar.de, Bauhaus-Universität Weimar, Germany--