Re: Ada.Strings.Bounded

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

On Apr 13, 2:02 pm, Robert A Duff <bobd...@shell01.TheWorld.com>
wrote:
> The analogy is not perfect.  You can create arbitrarily large strings
> (within the limits of available memory, and the bounds of Integer,
> which is pretty big).  It's just that any particular string object
> cannot change length.  Integers are much more restricted -- you can't
> create an integer bigger than some implementation-defined limit,
> such as 32 or 64 bits.

The perspective I have is that of the relationship between groupoids
and groups (and for strings, semigroupoids and semigroups).  A
groupoid, briefly, is just like a group except that its binary
operation is a partial function rather than a total function.  The
inverse function is also partial.  This terminology means that the
binary operation isn't defined on certain pairs.  The groupoid axioms
agree with the group axioms with the proviso that this is only
required where all the groupoid operations are defined.  There also
axioms to ensure that the operation is defined where it's possible to
define it symbolically.

The canonical example of a groupoid is a checkerboard.  This is
clearly like an infinite, bi-colored plane pattern, but it doesn't
have translational group symmetries because of the boundaries.  It
does have, however, translational groupoid symmetries.

From this perspective, the analogy is exact.  Raising an exception is
the computer-language way of indicating the difference between the
domain of a total function and that of a partial function.  Arithmetic
out-of-bounds raises Constraint_Error.  Concatenating strings to make
one that's too large raises Storage_Error.  If you don't get these
exceptions, your operations are known to satisfy the defining axioms
of the type.

I don't know if anybody has developed an "-oid" morphism for category
theory that takes an axiomatic theory and maps it to its "theory-oid"
version.  This is the mathematics for a proper formal theory of the
relationship between universal types and programming-language types.
(Note: when the set of elements of a universal type are finite, the "-
oid" morphism would be the identity.)  Yet I don't think there's a
practical reason to wait for this bit of research.  Map partial
function non-definition to an exception and otherwise assume that any
defining axioms are satisfied.


Switching subjects slightly, your comment points out (to me, at least)
a small deficiency in Ada's Integer types.  I think it should be
possible to define
   type Really_Long_Natural is range 0 .. 2**256 - 1 ;
with a mandate that it always compile.  This is the proper analogue
within integer types (as I think you took it) to fixed length
strings.  In this meaning, a more direct one, the analogue of an
integer is a string of length 1.  (BTW, such a type would be useful
for implementing symmetric ciphers.)

As you point out, there's already a bignum facility within a compiler,
so doing bignum arithmetic with fixed bounds should also be possible.
Indeed, evaluating the range expression itself requires that
facility.  The same bignum facility, with small modifications, could
also serve as the implementation basis of Unbounded_Integer, presented
as a library function rather than a native type.


> Well, the limits on bignums are fundamentally different from the limits
> on Ada's integer types.  In a language with bignums, the _language_
> places no limit on the size of integers.  An implementation can
> of course run out of memory, [...]
> Unbounded strings would be similar, if they were indexed by bignums.

I take this as a report of a language defect.  An unbounded string
*must* to be indexed by an unbounded natural.  If it's not, then the
string is bounded or it's not a string (since it would then break the
indexing axioms).  Changing this shouldn't create any backward-
compatibility problems for existing code, since there's a natural
inclusion map on values from word-length-limited Naturals into
unbounded Naturals.

Caveat: For the above to make sense, the phrase "unbounded string"
preceding does not mean "Ada.Strings.Unbounded_String", but rather the
well-defined-but-not-implemementable (i.e. universal) type
universal_string.

> I don't quite understand all this stuff about user-defined
> universal types (you give syntax, but didn't fully explain
> the semantics).  But anyway, you seem to be inventing something
> like abstract types, and/or class-wide types.

I wasn't trying to completely precise because of space limitations.
But let me say outright that I am sure this idea is not an abstract
type and not a class-wide type.  For an Ada-relevant means of entry to
this idea, here's a quotation from ARM 4.5.3/1:
> The binary adding operators + (addition) and - (subtraction)
> are predefined for every specific numeric type T with their
> conventional meaning.
So where does the "conventional meaning" come from?  Imprecisely, it's
been around as long as history.  Recall, Euclid had a proof that there
was no largest number.  Precisely, it dates to the earliest days of
modern formal logic, say, the late nineteenth century.  Neither of
these definitions have anything to do with programming languages.  But
that's the key to the whole puzzle.  The mental ideas that constitute
types as values and their manipulations originate outside computers
and their programming languages.  The way that humanity has found to
think precisely about these is with the tools of formal logic.

> Note that universal_integer is conceptually the same thing
> as root_integer'Class.  The RM doesn't say that, but the
> language designers had that analogy in mind.

As I've said in so many words just above, I believe this analogy is
infelicitous.  (I really do _not_ mean "wrong" here.)  It takes the
discussion inward to more programming language ideas and leads to
infinite regress--and lack of progress.

My idea of universal_integer is the following.  Start with the symbol
"0" and the unary function "S".  All the terms (in the predicate
calculus sense) of these two symbols constitute the set of integers.
By doing this, I eliminate non-standard models.  Add the axioms of
Peano arithmetic to get addition.  Add the rest of the axioms of
arithmetic to get its ordinary operator behavior.  That set of terms
with such axioms constitute universal_integer.

There's a canonical injective interpretation mapping from Ada's
Integer into universal_integer.  This is the value map.  It is not an
identity map, because the domain and range are not the same.  This
point is subtle and critical.  The domain is the valid values of Ada's
type Integer *as it is defined in the ARM* and its range is set of
symbols paired with a set of axioms.  These aren't the same.  They
cannot possibly be the same.  Any programming language has to down-
convert the total functions of a universal type to partial functions
of an implementable one.

There's a corresponding representation mapping in the other direction;
it's a partial function (necessarily).


> The above is an odd mixture of C-like syntax and Ada-like syntax.
> And "T2 x;" should be "X: T2;"

Yeah, my slip.  I've been on a C++ project lately.

> Surely "is private and U" should be "is new U with private".

But this one I meant.  A universal type should not be directly derived
from a universal type.  So I lifted the interface syntax.  Why
shouldn't you derive from a universal type?  Because it's not
implementable!  Universal types have a whole set of interrelationships
I'm avoiding; entirely within the set of universal types there's
something just like derivation.

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.
-- The set of operators on an implemented type
      _satisfy_ the axioms of the universal type.
Satisfaction here is framed in terms of preconditions, postconditions,
and invariants, in other words, all the specification apparatus of
program correctness.

> I don't know what "equal as universal values" means, either.

It means (now that I've put out some apparatus) that the values of the
interpretations maps are equal as terms of the universal type.
Symbolically, its the predicate "interpretation( y1 ) =
interpretation( y2 )", where "interpretation" is a (mathematical)
function Ada.Integer --> universal_integer.

Eric