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=-1.9 required=5.0 tests=BAYES_00 autolearn=ham autolearn_force=no version=3.4.4 X-Google-Thread: 103376,73cb216d191f0fef X-Google-NewGroupId: yes X-Google-Attributes: gida07f3367d7,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII-7-bit X-Received: by 10.180.183.84 with SMTP id ek20mr707033wic.0.1363264703174; Thu, 14 Mar 2013 05:38:23 -0700 (PDT) Path: bp2ni91662wib.1!nntp.google.com!feeder1-2.proxad.net!proxad.net!feeder1-1.proxad.net!ecngs!feeder2.ecngs.de!87.79.20.101.MISMATCH!newsreader4.netcologne.de!news.netcologne.de!newsfeed.arcor.de!newsspool3.arcor-online.net!news.arcor.de.POSTED!not-for-mail Date: Thu, 14 Mar 2013 13:37:44 +0100 From: Georg Bauhaus User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.7; rv:17.0) Gecko/20130307 Thunderbird/17.0.4 MIME-Version: 1.0 Newsgroups: comp.lang.ada Subject: Re: Is this expected behavior or not References: <8klywqh2pf$.1f949flc1xeia.dlg@40tude.net> <513f6e2f$0$6572$9b4e6d93@newsspool3.arcor-online.net> <513faaf7$0$6626$9b4e6d93@newsspool2.arcor-online.net> <51408e81$0$6577$9b4e6d93@newsspool3.arcor-online.net> <1xqmd3386hvns.1og1uql2cgnuf$.dlg@40tude.net> <5140b812$0$6575$9b4e6d93@newsspool3.arcor-online.net> <5140f1ad$0$6634$9b4e6d93@newsspool2.arcor-online.net> <7jct0noryc1v.1rnj5kkzx6m35.dlg@40tude.net> In-Reply-To: <7jct0noryc1v.1rnj5kkzx6m35.dlg@40tude.net> X-Enigmail-Version: 1.5.1 Message-ID: <5141c499$0$6642$9b4e6d93@newsspool2.arcor-online.net> Organization: Arcor NNTP-Posting-Date: 14 Mar 2013 13:37:45 CET NNTP-Posting-Host: 18d981b5.newsspool2.arcor-online.net X-Trace: DXC=T\a_Ym]jKEDFJ3]dH>I?oEA9EHlD;3YcB4Fo<]lROoRA8kFJLh>_cHTX3jM7[0[N_F X-Complaints-To: usenet-abuse@arcor.de Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit Date: 2013-03-14T13:37:45+01:00 List-Id: On 14.03.13 12:18, Dmitry A. Kazakov wrote: > On Wed, 13 Mar 2013 22:37:49 +0100, Georg Bauhaus wrote: > >> On 13.03.13 20:28, Dmitry A. Kazakov wrote: >> >>>> Ada subtypes are not ADTs. Which is the point. >>> >>> And the difference is? >> >> Several: >> Incomparable. >> In Ada, ADT is not defined. > > How exactly Ada's Positive is not an abstract data type? Because ADTs are constructs of human mapping from a model space to the space of language constructs. In this case the latter is defined in Ada terms. The human's mapping activity causes the---legitimate--- problem with subtype constraints. > We don't talk about Positive'Base. We do about Positive. Positive'Succ does *not* declare parameters whose subtype is Positive. This fact answers most of the other comments, I should think. For a start, LRM 3.5 again, 22 S'Succ S'Succ denotes a function with the following specification: 23 function S'Succ(Arg : S'Base) return S'Base We don't talk about Positive'Base, you say? >> subtype V is Integer range -2 .. +34; >> >> does not declare a new type (LRM 3.2.2(1)). > > Nevertheless > > Positive'Base /= Positive > > and both are types. The second claim is not true in Ada as relevant to this discussion, because Positive's subtype constraint does not introduce a type. >>> It is not a problem of definitions. >> >> Is it *solely* a problem of definitions from the non-Ada world. > > So, it is prime numbers which are broken. Good to know... Prime numbers are not defined in Ada, so the definition of Ada cannot break them. The subtype named Prime that was given was essentially a constraining predicate. If anyone thinks that 'Succ can be re-interpreted to refer to a non-interval subset of integral numbers of an Ada type, and it can't, then that's the problem: A plausible assumption about the definition vs the actual definition. >>> I shown that objects of Integer and Positive have different properties. >> >> The difference is entirely a consequence of different constraints on the >> same type that Integer and Positive share. > > Irrelevant. The difference is here. Period. It is proof that Ada subtypes (not Ada types) and LSP (plus, in this case, a re-interpretation of 'Succ based on incorrect premises) causes problems with constraints (not types). The compiler does not reject x : Positive := -1, so there is no Ada typing problem. There are two problems instead: 1) to think that a subtype creates a type 2) to assume that 'Succ is not what it is