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.3 required=5.0 tests=BAYES_00, REPLYTO_WITHOUT_TO_CC autolearn=no autolearn_force=no version=3.4.4 X-Google-Thread: a07f3367d7,73cb216d191f0fef X-Google-Attributes: gida07f3367d7,public,usenet X-Google-NewGroupId: yes X-Google-Language: ENGLISH,ASCII-7-bit X-Received: by 10.180.76.235 with SMTP id n11mr1338619wiw.0.1363400350275; Fri, 15 Mar 2013 19:19:10 -0700 (PDT) Path: g1ni68432wig.0!nntp.google.com!feeder1.cambriumusenet.nl!82.197.223.103.MISMATCH!feeder3.cambriumusenet.nl!feed.tweaknews.nl!85.12.40.130.MISMATCH!xlned.com!feeder1.xlned.com!news.astraweb.com!border3.a.newsrouter.astraweb.com!newsfeed10.multikabel.net!multikabel.net!newsfeed20.multikabel.net!news.mi.ras.ru!goblin2!goblin.stu.neva.ru!aioe.org!.POSTED!not-for-mail From: "Dmitry A. Kazakov" Newsgroups: comp.lang.ada Subject: Re: Is this expected behavior or not Date: Wed, 13 Mar 2013 20:28:57 +0100 Organization: cbb software GmbH Message-ID: 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> Reply-To: mailbox@dmitry-kazakov.de NNTP-Posting-Host: pQ928Up2OZ3uIq9RKW9GMg.user.speranza.aioe.org Mime-Version: 1.0 X-Complaints-To: abuse@aioe.org User-Agent: 40tude_Dialog/2.0.15.1 X-Notice: Filtered by postfilter v. 0.8.2 Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: 7bit Date: 2013-03-13T20:28:57+01:00 List-Id: On Wed, 13 Mar 2013 18:32:01 +0100, Georg Bauhaus wrote: > On 13.03.13 16:51, Dmitry A. Kazakov wrote: > >> http://en.wikipedia.org/wiki/Abstract_data_type > > Ada subtypes are not ADTs. Which is the point. And the difference is? >> Well, well, according to you Ada's Positive has -1 as a value? > > The Ada type of Positive includes -1 as a value. This is where ARM becomes relevant again: ARM 3-2(8/2): "A subtype of a given type is a combination of the type, a constraint on values of the type, and certain attributes specific to the subtype. The given type is called the type of the subtype. Similarly, the associated constraint is called the constraint of the subtype." and the final blow: "The set of values of a subtype consists of the values of its type that satisfy its constraint and any exclusion of the null value. Such values belong to the subtype." >> How a type theory may not apply to a programming language? Anyway if you >> don't like the theory X, you should propose another theory. > > Type as defined by the LRM; when the discussion is about how > you dislike what subtypes are, fine. Where I said I dislike them? What I said is that Ada subtype is a type-algebraic operation that produces a new type which properties are described in ARM. There are other type algebraic operations which produce array, record types, tagged extension, class-wide types, generic expansions/instantiations etc. They all are used to construct new *types* from existing ones. > However, seeing how > constraints and predicates work in Ada is not easier if > by some twist of the discussion the explanation becomes one > of how LSP and proper subsets create a well known problem in > a hypothetical or otherwise non-Ada language that involves > two different types, not Ada subtypes. > Let "subtype" be an Ada subtype, nothing else, and everything > becomes consistent again. Not necessarily clear, but consistent. > Maybe confusing, but consistent. Maybe counterintuitive, but > consistent. You are welcome to show how problems of substitutability get solved without these explanations. 'Succ has the problem of substitutability because of these problems. It is due to multiple inheritance. Pred'Succ inherits some ordered interface from Integer and from its own problem space. 'Succ is an operation of the interfaces. These interfaces collide in Prime. Ada's design choice was in favor of Integer's order: 'Succ (3)=4. But user's expectation was the order from the problem space 'Succ(3)=5. Now whatever definitions you take the problem is there. It is not a problem of definitions. >> But whichever theory you take, it cannot be consistent with Integer and >> Positive being same type, while considering Ada typed. >> >> Ada is typed. Integer and Positive are not same. > > Not same what? Need a reference here. Use any name you want for the corresponding entities. Whatever name you choose, I am still able to construct a program which semantics would change when Integer is substituted by Positive. Positive is not always substitutable for Integer. However you re-write ARM, that fact is to stay. >>> The difference only means that different range constraints yield >>> different programs. >> >> The difference exists. q.e.d. > > You have shown that different constraints on objects of the > same type yield different programs. But this is not q.e.d. I shown that objects of Integer and Positive have different properties. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de