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.86.38 with SMTP id m6mr1246803wiz.0.1364343988282; Tue, 26 Mar 2013 17:26:28 -0700 (PDT) Path: p18ni19746wiv.0!nntp.google.com!feeder1.cambriumusenet.nl!feed.tweaknews.nl!85.12.40.138.MISMATCH!xlned.com!feeder5.xlned.com!newsfeed.xs4all.nl!newsfeed1.news.xs4all.nl!xs4all!border4.nntp.ams.giganews.com!border2.nntp.ams.giganews.com!border2.nntp.dca.giganews.com!nntp.giganews.com!newsgate.cuhk.edu.hk!goblin1!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: Tue, 19 Mar 2013 11:14:38 +0100 Organization: cbb software GmbH Message-ID: References: <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> <5141c499$0$6642$9b4e6d93@newsspool2.arcor-online.net> <18r2kop6fyozu.tctrjnghfxqs.dlg@40tude.net> <1wv3p3nrtejfk$.bwebhg9agt0l.dlg@40tude.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="us-ascii" Content-Transfer-Encoding: 7bit Date: 2013-03-19T11:14:38+01:00 List-Id: On Mon, 18 Mar 2013 17:36:31 -0500, Randy Brukardt wrote: > "Dmitry A. Kazakov" wrote in message > news:hiybjkhz3p5d.1x6dxfr1ptgcg.dlg@40tude.net... >> But I don't see where I disagree with myself. Contract /= type. You can >> have same contract and different types. What about: >> >> type Same is new Integer; > > This definitely has a different contract, as it is not compatible with > Integer's contract. Yes, it has the same set of values and operations with > the same name, profile, and bodies, but it's still a different contract > because the types involved are an intergral part of the contract. See, you just defined a contract in terms of types while using contracts to define type as same/different/non-existent. You cannot have it in both ways. >> You also can have different contracts put on the same type in different >> contexts. You can have contracts on something that does not involve types >> at all. Anyway, I fail to see how contracts are relevant here. > > Because types are an important part of a contract (that is, in Ada terms, > the profile). *if* you want to contract a type, *then* that cannot be a part of. In any case, contract is much less a language term than type. It is more about design and the problem space. It may apply to a type when the type is used to represent some domain entity but it cannot define what types are. A type is values+operations. > Two operations with different profiles are different, even if > everything else is the same (the implementation, names of things, etc.) Ada has *nominal* equivalence of operations. Two operations are different just because they are declared in different places. It is not because of their profiles. On top of that there are rules about overloading/overriding where profiles get involved, but that is not like C where you can repeat declarations. >> I don't see why. How *any* contract could make something like Positive a >> non-type? There is not many possibilities: >> >> A. Positive is not a type. This is what Georg says. I have no idea what >> this is supposed to mean. That 123 is not Positive, or that "+" is not >> applied to positives? He escapes into some kind of vague philosophy each >> time I ask. > > I agree with Georg; Positive is not a type; it *has* a type. Neither is > Integer a type; it *has* a type. Since there is an equivalence between Positive and the type is "has," Positive as a name unambiguously refers to that type, i.e. "Positive" is the name of the type. Unless you have other legal name for it. But you don't in Ada. You have absolutely no language means whatsoever to distinguish Positive and the type of. So, what merits has this distinction if it cannot be observed? > (All types in Ada are anonymous.) Great, then let them be, where there belong to, in the celestial spheres, and let us call type something that indeed exists in the language and has a name. > Types are only about static semantics > (that is, compile-time behavior). Run-time semantics aren't involved. Run-time semantics is what makes program working or not working. Types are all about run-time semantics nothing else counts. Type checks is a way to prove something about [run-time] semantics at compile time. Types neither ensure nor required for a program to behave correctly. They are a tool to ease reaching that goal. > Run-time semantics get added on top of that, but that has no effect on the > legality of a program, so it is completely orthogonal to the type/profile. Legality is irrelevant as we consider only legal Ada programs. There exist legal Ada programs which change their run-time behavior when 'Positive' is replaced by 'Integer' and reverse. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de