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!news2.google.com!postnews.google.com!b5g2000pri.googlegroups.com!not-for-mail From: Eric Hughes Newsgroups: comp.lang.ada Subject: Re: Ada.Strings.Bounded Date: Sun, 13 Apr 2008 09:31:17 -0700 (PDT) Organization: http://groups.google.com Message-ID: <276e98e3-3b3b-4cbf-b85c-dcae79f11ec5@b5g2000pri.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> 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 1208104277 29703 127.0.0.1 (13 Apr 2008 16:31:17 GMT) X-Complaints-To: groups-abuse@google.com NNTP-Posting-Date: Sun, 13 Apr 2008 16:31:17 +0000 (UTC) Complaints-To: groups-abuse@google.com Injection-Info: b5g2000pri.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:20909 Date: 2008-04-13T09:31:17-07:00 List-Id: On Apr 12, 3:09 pm, "Dmitry A. Kazakov" 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" 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