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,UTF8 X-Received: by 10.180.89.133 with SMTP id bo5mr1342742wib.6.1363401704169; Fri, 15 Mar 2013 19:41:44 -0700 (PDT) Path: g1ni68464wig.0!nntp.google.com!feeder1.cambriumusenet.nl!feed.tweaknews.nl!94.232.116.12.MISMATCH!feed.xsnews.nl!border-2.ams.xsnews.nl!multikabel.net!newsfeed20.multikabel.net!news.mi.ras.ru!goblin1!goblin.stu.neva.ru!noris.net!newsfeed.arcor.de!newsspool4.arcor-online.net!news.arcor.de.POSTED!not-for-mail Date: Wed, 13 Mar 2013 22:37:49 +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> In-Reply-To: Message-ID: <5140f1ad$0$6634$9b4e6d93@newsspool2.arcor-online.net> Organization: Arcor NNTP-Posting-Date: 13 Mar 2013 22:37:49 CET NNTP-Posting-Host: 786fccfc.newsspool2.arcor-online.net X-Trace: DXC=kjIIBo<>D0CA@P]\DA9EHlD;3YcB4Fo<]lROoRA8kFejVH^;ba9;cBJdIW1TbGX\;TaD X-Complaints-To: usenet-abuse@arcor.de Content-Type: text/plain; charset=UTF-8; format=flowed Content-Transfer-Encoding: 8bit Date: 2013-03-13T22:37:49+01:00 List-Id: 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. An ADT is a model of thought that can be mapped to constructs. I find it moderately useful to insist on problems with predicates that only exist in the ADT/LSP model, but not in Ada (where there simply is no variance in this case due to the definition of 'Succ). >>> 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): ARM 3.2(8/2) implies that "the type of Positive includes the value -1" (the type of Positive is not the subtype Positive). For example, with one compiler, values_of(Positive) = { x : x ∈ values_of(type_of(Positive)) | x ≧ 1 & x ≦ 2³¹-1 } The paragraph you have quoted from the LRM thus indicates that the value -1 belongs to the type of Positive, but -1 does not belong to what Ada calls a subtype. Hence, again, the type of Positive includes the value -1, but the subtype Positive does not. Let me see if I understand the claim that a subtype declarations is a type-algebraic operation correctly, with Ada in mind: One starts from types to produce new types. type V is array (S) of T; declares a new type (and its ...). But subtype V is Integer range -2 .. +34; does not declare a new type (LRM 3.2.2(1)). Only some re-interpretation of Ada terms creates a notion of subtype that Ada does not seem to support, really. One can do this, but when solving a problem with (a misreading of) 'Succ, doing so only emphasizes the cause of the problem, which is assuming that a subtype can be treated the same way as a type or ADT. > You are welcome to show how problems of substitutability get solved without > these explanations. There is no substitutability issue whatsoever for parameters of 'Succ because 'Succ is not defined in terms of types that could introduce the problem. This definition may not be as desired, but the problem is extraneous from an Ada perspective. Instead, I could define (like you have done many times before): type T is private ...; function Succ (X : T) return T with ...; when I need to map T to an algebraic data type. > It is not a problem of definitions. Is it *solely* a problem of definitions from the non-Ada world. > 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. I wondered why you have avoided the word "type" here and use "properties" instead?