Re: Ada.Strings.Bounded

[Eric Hughes <eric.eh9@gmail.com>]

On Apr 14, 3:07 am, "Dmitry A. Kazakov" <mail...@dmitry-kazakov.de>
wrote:
> If you are aiming at Liskov substitutability
> principle,

But I'm not aiming for that.  It's related, to be sure, but it's not
the same.  If you don't acknowledge that a universal type is a
different creature than an ordinary type, then you would have to see
only preexisting relationships.

> > So I can now outline what the relationship ought to be:
> > -- The set of values of an implemented type is
> >       a _subset_ of the terms of the universal type.
>
> Counterexample: NaN of Float.

I take from what you're saying that the ordinary way of bringing
floating point arithmetic into a language is not an implementation of
universal Real numbers.  That's true.

We can talk about optimal encodings and less-than-optimal encodings,
if you'd like, but I really don't see how the exceptional values of
floating point numbers violate the spirit of the rule.  NaN, but even
more so overflow and underflow, even though they're defined for
hardware implementations, could well be forbidden as accessible values
from within the language.  You clearly couldn't eliminate this kind of
type from ordinary use soon, because it's well-embedded in practice
and skills.

The issue then becomes whether it would be beneficial to also have a
Real-implementing type in the pattern I've mentioned.  The differences
would be small.  Since a calculation that results in an exceptional
value raises an exception, such a value that would otherwise be
assigned is simply not assigned (or even made visible).  I think that
takes care of all the modification that would be needed.

> The set of values of a derived type is neither subset or superset. It is a
> different set.

If you insist, but this is not derivation.

> > -- The set of operators on an implemented type
> >       _satisfy_ the axioms of the universal type.
>
> This cannot work because any implementation is necessarily a DFA.

???

Eric