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.9 required=5.0 tests=BAYES_00,FORGED_GMAIL_RCVD, FREEMAIL_FROM autolearn=no autolearn_force=no version=3.4.4 X-Google-Thread: 103376,61e9062c1f23b9d5 X-Google-Attributes: gid103376,public,usenet X-Google-Language: ENGLISH,ASCII-7-bit Path: g2news1.google.com!postnews.google.com!p77g2000hsh.googlegroups.com!not-for-mail From: Maciej Sobczak Newsgroups: comp.lang.ada Subject: Re: Reconsidering assignment Date: Mon, 11 Jun 2007 02:04:19 -0700 Organization: http://groups.google.com Message-ID: <1181552659.785072.44010@p77g2000hsh.googlegroups.com> References: <1181165630.012508.55290@i38g2000prf.googlegroups.com> <19fxsxv1god43$.1pqq8vgfu2itn$.dlg@40tude.net> <1181428673.148991.76570@p77g2000hsh.googlegroups.com> <1nhm7vx3gq7sx.eiq9ay921q42.dlg@40tude.net> NNTP-Posting-Host: 137.138.37.241 Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii" X-Trace: posting.google.com 1181552659 12066 127.0.0.1 (11 Jun 2007 09:04:19 GMT) X-Complaints-To: groups-abuse@google.com NNTP-Posting-Date: Mon, 11 Jun 2007 09:04:19 +0000 (UTC) In-Reply-To: <1nhm7vx3gq7sx.eiq9ay921q42.dlg@40tude.net> User-Agent: G2/1.0 X-HTTP-UserAgent: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.8.0.12) Gecko/20070601 Red Hat/1.5.0.12-0.1.slc3 Firefox/1.5.0.12,gzip(gfe),gzip(gfe) Complaints-To: groups-abuse@google.com Injection-Info: p77g2000hsh.googlegroups.com; posting-host=137.138.37.241; posting-account=Ch8E9Q0AAAA7lJxCsphg7hBNIsMsP4AE Xref: g2news1.google.com comp.lang.ada:16153 Date: 2007-06-11T02:04:19-07:00 List-Id: On 10 Cze, 11:21, "Dmitry A. Kazakov" wrote: > >> New subtypes can also be obtained through generalization, i.e. by lifting > >> constraints. > > > Yes, but then they are not SUBtypes. :-) > > subtype /= subset. Especially if you consider Liskov-Wing definitions. They > defines it in terms of substitutability. A more pragmatic definition would > be: > > S is a subtype of T in an operation f when S inherits the interface of f. I don't see how this might imply anything. If f cares about preconditions on its arguments, then being a subtype means being a subset (and if f doesn't care about preconditions then there is little sense in implying any relation between T and S based on f). Lifting constraints doesn't give subtypes. Supertype is the correct term here. > > BTW - the fact that I cannot make a subtype by selecting non- > > contiguous subranges of enum values is really disappointing. > > That is because you cannot inherit "..", 'Succ and 'Pred. To have > non-contiguous enumerations, you should have them as a base type/interface > first. Yes, this is what I expect: type Color is (Black, Red, Green, Blue, White); I don't want any "..", 'Succ nor 'Pred here. > >> which were ambiguous: > > >> X : Integer := 1 + 1; > > >> is it Positive'(1)+Positive'(1) or Integer'(1)+Integer'(1)? You will need > >> complex preference rules to resolve this mess. > > > It's a compile-time expression with the value 2. > > Not very complex. ;-) > > It is complex, because 1 (as any literal) is a function, an overloaded one. No. Compile-time expression is not executed in the universe of functions overloaded in the program. It can use completely separate rules - what matters is the result and whether it fits in the given type. > >>> S1 : String := "abc"; > >> S4 : String := Read_From_File; > >> Safe_Swap(S1, S4); -- ? > > > Compiler should cowardly refuse it (that's what "conservative" means). > > No, this wouldn't be a typed system anymore. Then let's make the constraint part of the type. > S2 and S4 have exactly the > same type. Then let's make them different. > If you want to distinguish something between legal and an illegal > you need different types. Legality cannot depend on a constraint. The whole point of my speculations is to elevate constraints to the level where they could take part in legality resolutions. I hoped it was clear. > >>> Now - what am I missing? :-) > > >> That Constraint_Error is a valid outcome. > As long as a correct program runs, everything it does is valid. For the appropriate definitioin of "runs". :-) > >> The problem is not that "-" of > >> Integer is inherited by Positive. > > > Sure. Positive gets its own "-" by the same magic that gifted it to > > Integer in the first place. > > And what does the magic say about 0-1? It's not only "-". You can overflow the upper constraints as well. This is, I admit, the place where the whole system gets clunky. It would be insane to expect programmers to write explicit casts (to satisfy the "innocent code doesn't lie") absolutely everywhere where the result of the operation can go out of LHS constraints, because that would basically hit every arithmetic operation, not only "-" (except for modulo types, which would be the only "pure safe"). SPARK solves this outside of the type system, but that was not the intention of my experiment. So, I admit, the common arithmetics is a place where C_E seems to be necessary as a "valid" outcome. If explicit casts would be used everywhere to mark the possibility of having C_E, then we might as well drop the casts and have this possibility implicitly: A := Positive(B + C); -- beware C_E, too much typing X := Y + Z; -- beware C_E anyway -- Maciej Sobczak http://www.msobczak.com/