From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-0.9 required=5.0 tests=BAYES_00,FORGED_GMAIL_RCVD, FREEMAIL_FROM autolearn=no autolearn_force=no version=3.4.4 X-Google-Thread: 103376,640b65cbfbab7216 X-Google-Attributes: gid103376,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII-7-bit Path: g2news1.google.com!postnews.google.com!s13g2000prd.googlegroups.com!not-for-mail From: Eric Hughes Newsgroups: comp.lang.ada Subject: Re: Ada.Strings.Bounded Date: Sun, 13 Apr 2008 16:20:24 -0700 (PDT) Organization: http://groups.google.com Message-ID: <013e1d52-c25f-49ea-83ef-6ac4860858bf@s13g2000prd.googlegroups.com> References: <47F26C46.3010607@obry.net> <44d88b93-6a90-4c18-8785-2164934ba700@a9g2000prl.googlegroups.com> <47F652F7.9050502@obry.net> <47f7028d$1_6@news.bluewin.ch> <47F749CB.30806@obry.net> <96x8my4o4m7e.fskzcb6i31ty$.dlg@40tude.net> <276e98e3-3b3b-4cbf-b85c-dcae79f11ec5@b5g2000pri.googlegroups.com> NNTP-Posting-Host: 166.70.57.218 Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit X-Trace: posting.google.com 1208128825 8414 127.0.0.1 (13 Apr 2008 23:20:25 GMT) X-Complaints-To: groups-abuse@google.com NNTP-Posting-Date: Sun, 13 Apr 2008 23:20:25 +0000 (UTC) Complaints-To: groups-abuse@google.com Injection-Info: s13g2000prd.googlegroups.com; posting-host=166.70.57.218; posting-account=5RIiTwoAAACt_Eu87gmPAJMoMTeMz-rn User-Agent: G2/1.0 X-HTTP-UserAgent: Mozilla/5.0 (Windows; U; Windows NT 5.1; en-US; rv:1.8.1.13) Gecko/20080311 Firefox/2.0.0.13,gzip(gfe),gzip(gfe) Xref: g2news1.google.com comp.lang.ada:20926 Date: 2008-04-13T16:20:24-07:00 List-Id: On Apr 13, 2:02 pm, Robert A Duff 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