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: 103376,73cb216d191f0fef X-Google-NewGroupId: yes X-Google-Attributes: gida07f3367d7,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII X-Received: by 10.180.24.132 with SMTP id u4mr5395683wif.6.1363189802312; Wed, 13 Mar 2013 08:50:02 -0700 (PDT) Path: bp2ni89915wib.1!nntp.google.com!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 16:51:14 +0100 Organization: cbb software GmbH Message-ID: <1xqmd3386hvns.1og1uql2cgnuf$.dlg@40tude.net> 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> Reply-To: mailbox@dmitry-kazakov.de NNTP-Posting-Host: FbOMkhMtVLVmu7IwBnt1tw.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="iso-8859-1" Content-Transfer-Encoding: 8bit Date: 2013-03-13T16:51:14+01:00 List-Id: On Wed, 13 Mar 2013 15:34:41 +0100, Georg Bauhaus wrote: > On 13.03.13 14:31, Dmitry A. Kazakov wrote: >> On Wed, 13 Mar 2013 10:45:54 +0100, J-P. Rosen wrote: >> >>> Le 13/03/2013 09:49, Dmitry A. Kazakov a �crit : >>>> In Ada subtype >>>> (here subtype is Ada-subtype) operations are inherited per composition with >>>> conversion to the base type which is null for in-arguments and sometimes >>>> range-check of outs (not always, though). E.g. >>>> >>>> F (X : S) = F (S'Base (X)) >>>> >>>> S is a subtype *because* it inherits F. >>> >>> Not at all. In Ada, a type is a set of values. >> >> A type is a set of values bound by operations defined on them. It is >> values+operations. > > The LRM does not define what it means for sets of values being > "bound by operations". It does define subtypes and types. LRM is irrelevant here. See http://en.wikipedia.org/wiki/Abstract_data_type >> Even under your (wrong) definition Positive is still different from Integer >> because Positive does not have values like -1. > > I don't think this is true. Well, well, according to you Ada's Positive has -1 as a value? >> Ada subtypes are proper types > > External observations inspired by whichever type theory do > not apply when judging things from the Ada perspective. 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. 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. >> E.g. these two programs are not equivalent: >> >> X : Integer := -1; > ... >> You cannot replace Integer with Positive without changing the semantics of >> any possible program, hence they are different. > > The difference only means that different range constraints yield > different programs. The difference exists. q.e.d. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de