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: a07f3367d7,73cb216d191f0fef X-Google-Attributes: gida07f3367d7,public,usenet X-Google-NewGroupId: yes X-Google-Language: ENGLISH,ASCII-7-bit X-Received: by 10.180.10.230 with SMTP id l6mr1279462wib.3.1363398717086; Fri, 15 Mar 2013 18:51:57 -0700 (PDT) Path: bp2ni94692wib.1!nntp.google.com!feeder1.cambriumusenet.nl!82.197.223.108.MISMATCH!feeder2.cambriumusenet.nl!feeder3.cambriumusenet.nl!feed.tweaknews.nl!85.12.40.138.MISMATCH!xlned.com!feeder5.xlned.com!newsfeed10.multikabel.net!multikabel.net!newsfeed20.multikabel.net!news.mi.ras.ru!goblin1!goblin.stu.neva.ru!news.swapon.de!fu-berlin.de!newsfeed.arcor.de!newsspool1.arcor-online.net!news.arcor.de.POSTED!not-for-mail Date: Wed, 13 Mar 2013 18:32:01 +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> In-Reply-To: <1xqmd3386hvns.1og1uql2cgnuf$.dlg@40tude.net> X-Enigmail-Version: 1.5.1 Message-ID: <5140b812$0$6575$9b4e6d93@newsspool3.arcor-online.net> Organization: Arcor NNTP-Posting-Date: 13 Mar 2013 18:32:02 CET NNTP-Posting-Host: 2fdbf0f7.newsspool3.arcor-online.net X-Trace: DXC=c;ZLh>_cHTX3j]9eggWRL57?T X-Complaints-To: usenet-abuse@arcor.de Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit Date: 2013-03-13T18:32:02+01:00 List-Id: On 13.03.13 16:51, Dmitry A. Kazakov wrote: > LRM is irrelevant here. See The Ada LRM seems somewhat relevant when discussing the workings of Ada type attributes and predicates. > http://en.wikipedia.org/wiki/Abstract_data_type Ada subtypes are not ADTs. Which is the point. > Well, well, according to you Ada's Positive has -1 as a value? The Ada type of Positive includes -1 as a value. > 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. 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. > 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. (There is an X such that grapefruits and oranges are not same X. There is an X such that Positive and Integer are not same X.) >> 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.