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: 103376,73f81e5f5d6ee80f X-Google-Attributes: gid103376,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII-7-bit Path: g2news2.google.com!news4.google.com!feeder1-2.proxad.net!proxad.net!feeder2-2.proxad.net!newsfeed.arcor.de!newsspool1.arcor-online.net!news.arcor.de.POSTED!not-for-mail Date: Fri, 12 Dec 2008 15:29:46 +0100 From: Georg Bauhaus User-Agent: Thunderbird 2.0.0.18 (Macintosh/20081105) MIME-Version: 1.0 Newsgroups: comp.lang.ada Subject: Re: MI is sloppy References: <1g29uf1ygl1wc$.1x184o2bk9m0k$.dlg@40tude.net> <1hjx0k7xmfw4n$.14q7chpo1r1ma$.dlg@40tude.net> <49424203$0$31868$9b4e6d93@newsspool3.arcor-online.net> <494255e8$0$31331$9b4e6d93@newsspool4.arcor-online.net> <43lprrmyik2q.1esp72deqcw6o.dlg@40tude.net> In-Reply-To: <43lprrmyik2q.1esp72deqcw6o.dlg@40tude.net> Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit Message-ID: <4942755b$0$31331$9b4e6d93@newsspool4.arcor-online.net> Organization: Arcor NNTP-Posting-Date: 12 Dec 2008 15:29:47 CET NNTP-Posting-Host: 5a88b29c.newsspool4.arcor-online.net X-Trace: DXC=mA21Y<0ad6o>jlK2>IgHGd4IUKP_O7VW]oga;9OJDO8_SKfNSZ1n^B98ijf@@9YM9GZ7n X-Complaints-To: usenet-abuse@arcor.de Xref: g2news2.google.com comp.lang.ada:3948 Date: 2008-12-12T15:29:47+01:00 List-Id: Dmitry A. Kazakov schrieb: >>> Constraint_Error propagation is the contracted behavior. You have signed >>> that contract, enjoy it. >> But the compiler informs you that Constraint_Error will >> be raised if your program is such that it will be raised. >> Anything wrong with correcting the program? > > How? The program is already correct it does what you asked it to do. I had understood that the subprogram in question was *formally* receiving any file, and in addition was constrained to only accept a file object that falls into the correct subset of the File type. This kind of constraint might be interpreted to be a run-time thing, but could be made a compile-time check where possible. What's a correct program? If the program passes an object outside the set, it is not correct, taking "correct" to mean the program operates as intended by the programmer - stopping at type correctness seems comparatively lame (unless you have a type system such as that of Qi, see below). >> If we wanted more of the minor differences covered >> by type hierarchies, we might end up with a Qi type >> system... For Ada? > > 1. Qt is not a programming language. Qi, 'Q' & Character'Val(151), is a programming language that includes the most powerful type system of all type systems ever to be invented (in terms of Turing equivalence). http://www.lambdassociates.org/ > 2. There is no minor differences in terms of correctness. An incorrect > program is incorrect. > > There is no *any* way to predict the effect of incorrectness. The system is > not only instable, it is simply unknown. It does not obey the logic of > (some) physical systems, where you can A) measure the change, B) measure > the effects. There is no metric, no distance, no way to measure things, it > is just non-continuous etc. "minor differences" is meaningless. > > Last but not least, how are you going to make differences visible to the > program reader? By writing comments explaining when and how > Constraint_Error, other exceptions, and program crashes would happen? Minor differences can be formally specified by writing additional constraints that may not be impressive enough to justify yet another type. As you know, it is not possible (according to different sources) to express any significant amount of differentiation employing just a type system *unless* the type system is so powerful that you are expected and willing to wait an indeterminate amount of time until your compiler's type checking parts start commenting on your program, if ever.