Re: Ada.Strings.Bounded

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

On Apr 12, 3:09 pm, "Dmitry A. Kazakov" <mail...@dmitry-kazakov.de>
wrote:
> So a comparable case would be Integer vs. BigNum. The latter
> (arbitrary-precision arithmetic) plays same role for integers as
> Unbounded_String does for strings. Now, if ARM had BigNum defined, we would
> experience exactly same problems with both, as we have with Strings and
> Unbounded_String.

Well, yes; that's a good second example, although let's call it
Unbounded_Integer.  The mechanisms are identical for dealing with
universal_string/String/Unbounded_String and univeral_integer/Integer/
Unbounded_Integer.  In the first case we have (0=absent,1=present)
0/1/1 and in the second we have 1/1/0.  In the first case we have
endless type conversions to do ordinary work.  In the second we have
an absence in the standard.


On Sat, 12 Apr 2008 11:50:56 -0700 (PDT), Eric Hughes wrote:
> I believe many of the issues involving strings could be addressed by
> introducing a predefined type universal_string.

On Apr 12, 3:09 pm, "Dmitry A. Kazakov" <mail...@dmitry-kazakov.de>
wrote:
> I don't see it this way.

I have a strong counterclaim--I don't think it can be solved without
introducing such a type.

Here's the real rub: universal_integer and universal_string are each
_unimplementable_ as executable types.  As abstract mathematical
types, they're perfectly well-defined.  The origin of the difference
is that universal types have no possible bound in size.  Since every
computer type has such a bound, there's a fundamental disjunct between
these two.  An unbounded type actually does have a bound--it throws an
exception when its internal bounds are exceeded.  A hypothetical
implementation of a universal type would be unable *in principle* to
throw such an exception.  This is clearly contrary to fact, where
every program can run out of memory.

If this sounds like my idea for partial type specification (one
without code), it should.  These ideas come from the same perspective.

There's no concept (except _ad hoc_ in the ARM) of what a universal,
unimplementable type is; there's certainly no way of declaring one.
So here's the very beginning of a proposal.  To declare and define
such a type:

    universal_type_definition ::= *universal* *type*
defining_identifier [known_discriminant_part] *;*

Notice the absence of the keyword "is".  Also notice that the
declaration and definition are the same.  The point is that a
universal type _is not_ anything insofar as record declaration or
anything else that might act as a representation.  A universal type
can not have a representation (not just "may not").  If it had a
representation, it would not be universal.  This is not merely a
practicality; this is categorical.

Now like other types, you could declare operations on universal
types.  But every such operation would also be unimplementable, so
they're declaration-only.  They cannot be defined, since there's no
representation to work with.

As with an interface, an ordinary type T could derive from a universal
type U.  It could override operations from the universal type.  But
since U has no implementation, such a derivation has no effect on the
representation of T.  The result of overriding would be to bind both
the syntax and semantics of U to that of T.  With only a single such
T, an overriding declaration would be meaningless and of no effect.
With two such declarations, however, the benefits begin.  The meaning
of such a pair of declarations says that the semantics of the two
operations are identical when values of one type are substituted for
that of the other _when those values are considered as universal
values_ (and thus not as represented values within an implementation).

With such a syntax, you obtain the ability to make a well-formed
formula with clearly defined semantics.  It says nothing about
compilation.  I consider this an advantage, as it is the essence of
separate compilation.  Getting to an unambiguous expression is the
first step.

Now, about compilation, a formula with well-defined semantics does not
(in general) have well-defined pragmatics.  The formula itself does
not specify how long execution should take, what functions must be
called, etc.  All the formula as such says is what the results should
be.  A simple example:

   universal type U ;
   function op( U Object ) return U ;
   type T1 is private and U ;
   type T2 is private and U ;
   overriding function op( T1 Object ) return T1 ;
   overriding function op( T2 Object ) return T2 ;
   function U( T2 Object ) return T1 ;
   T2 x ;
   T1 y1 := T1.op( U( x ) ) ;
   T1 y2 := U( T2.op( x ) ) ;
   T1 y := x.op ;

The expressions for y1 and y2 should be interchangeable as
implementations for the expression for y.  The point of the
declarations is to give unambiguous semantics to the expression
"x.op", so that it does not matter to the correctness of the program
what implementation expression the compiler chooses.  If Usenet had
better formatting, I'd draw a commutative diagram as an illustration.

There's special meaning behind the conversion function U.  Its
mandatory semantics is to convert an object of T2 to one of T1, such
that their values are equal as universal values.

Eric