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,FREEMAIL_FROM autolearn=ham autolearn_force=no version=3.4.4 X-Google-Thread: a07f3367d7,39579ad87542da0e X-Google-Attributes: gida07f3367d7,public,usenet X-Google-NewGroupId: yes X-Google-Language: ENGLISH,UTF8 X-Received: by 10.68.137.71 with SMTP id qg7mr5143021pbb.5.1368583216571; Tue, 14 May 2013 19:00:16 -0700 (PDT) Path: bp1ni2274pbd.1!nntp.google.com!npeer03.iad.highwinds-media.com!news.highwinds-media.com!feed-me.highwinds-media.com!border3.nntp.dca.giganews.com!border1.nntp.dca.giganews.com!border4.nntp.dca.giganews.com!border2.nntp.dca.giganews.com!nntp.giganews.com!newsfeed.news.ucla.edu!nrc-news.nrc.ca!newsflash.concordia.ca!News.Dal.Ca!citadel.nobulus.com!goblin1!goblin.stu.neva.ru!news.mixmin.net!rt.uk.eu.org!aioe.org!.POSTED!not-for-mail From: =?utf-8?Q?Yannick_Duch=C3=AAne_=28Hibou57?= =?utf-8?Q?=29?= Newsgroups: comp.lang.ada Subject: Re: Seeking for papers about tagged types vs access to subprograms Date: Wed, 08 May 2013 18:13:26 +0200 Organization: Ada @ Home Message-ID: References: <17ceq51ydy3s0.s94miqqzbg5w.dlg@40tude.net> <1vrhb7oc4qbob$.q02vuouyovp5$.dlg@40tude.net> <19lrzzbgm77v6.1dzpgqckptaj6.dlg@40tude.net> <1bfhq7jo34xpi.p8n2vq6yjsea.dlg@40tude.net> NNTP-Posting-Host: 7OQr3E3VjE1ZKDv7Xqqyjg.user.speranza.aioe.org Mime-Version: 1.0 X-Complaints-To: abuse@aioe.org User-Agent: Opera Mail/12.15 (Linux) X-Notice: Filtered by postfilter v. 0.8.2 X-Received-Bytes: 6486 Content-Type: text/plain; charset=utf-8; format=flowed; delsp=yes Content-Transfer-Encoding: Quoted-Printable Date: 2013-05-08T18:13:26+02:00 List-Id: Le Wed, 08 May 2013 17:29:33 +0200, Dmitry A. Kazakov = a =C3=A9crit: >> I would say there is no general answer without additional information= s >> about what the whole means, and no language or its compiler can tell = it = >> in >> place of the author (or else, you decide in place of the author, and = are >> back to what it actually is). > > First you should be able to define such entities formally =3D at the = > language > level. Yes, that was the idea. What you say seems equivalent to saying =E2=80=9C= the = language should allow to express it=E2=80=9D. Actually, it's built=E2=80= =91in only (and so = also frozen). By the way, old prover software had a comparable issue in = = the paste, they came with built=E2=80=91in methods to validate this or t= hat kind = of specific inferences technique within this or that kind of specific = domain. Then later came provers with a tiny core engine, on which is = concentrated all the efforts for correctness. The former were more error= = prone (one was even well known as buggy and not soun) and less expressiv= e. = The latter present their own issues, but are more safe and more = expressive, as they allow the user to freely express something above, as= = the core ensure the soundness of the inferences (you can get it wrong to= o, = but that's not the topic). I don't try to say a general purpose = programming language should compare to this, just that the way to go ahe= ad = may be a bit similar: less built=E2=80=91ins, and more support for sound= ness (I = like to say, the value of a language is not in its libraries, this is a = = bit similar here). >> A basic idea (more easy to say than to do): reuse things like >> pre/post/pragma=E2=80=91assert, but whose purpose is to be statically= checked = >> (if >> it's too complicated to be checked, > > Checks if come in question, then only much later after you have = > formalized > it. Static checking is not like dynamic checking. Dynamic checking is just = checking, while static checking really ensure some assertions. There are= = multiple way to formalize, but sooner or later, all have to arrive at th= e = point of providing assertions, or else, you can't derive anything from i= t. = So I believe static check one of the way to the formalization. >> Also to digress but still in some way related, more control on what c= an = >> be >> done of an instance of a type, toward restricting, permitting to deny= = >> the >> use of some part of an interface, > > Each time you do something with a type you get another one. Yes > Otherwise it > becomes untyped. So if you wanted to disallow operations that would ma= ke > another interface. That's what a subtype is to me (I don't know if it's the proper term; at= = least it seems to match with Ada's own wording). > To put it differently, there shall be no preconditions > on types and their operations which aren't trivially true. I don't understand that point. > Another question > is the relationship between the original type and the new one. That = > brings > the issue of LSP with it, if you attempt to bring them into one = > hierarchy. LSP is a handy principle, the only one practicable with most general = purpose languages, but that's not the only way to formalize things and = ensure their correctness; sometime it does not fit. Some relations may b= e = preserved, some may not be. If some are preserved, you can count on it, = = while it suffice some are not preserved to make LSP irrelevant, and wors= t, = reject the system. That's precisely the case with restricted interfaces,= = it's easy to see some relations are preserved but it does not conform to= = LSP. LSP is nice when applicable, because it is a simple principle; ther= e = are times where it is too rigid. That's why I focused on the topic of th= e = relations and properties individually. > Ad-hoc supertypes could possibly help. Yes, that would allow to understand subtypes as any other simply derived= = types. May be the supertype could be automatically or inferred. Or shoul= d = that be always explicit? > Parallel hierarchies could be an > alternative. I will try to imagine what this means or how it works, I don't have a = clear picture in mind right at the moment. -- = =E2=80=9CSyntactic sugar causes cancer of the semi-colons.=E2=80=9D [1] =E2=80=9CStructured Programming supports the law of the excluded muddle.= =E2=80=9D [1] [1]: Epigrams on Programming =E2=80=94 Alan J. =E2=80=94 P. Yale Univers= ity