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.180.109.111 with SMTP id hr15mr1644967wib.1.1368583579783; Tue, 14 May 2013 19:06:19 -0700 (PDT) Path: hg5ni110155wib.1!nntp.google.com!feeder1.cambriumusenet.nl!feed.tweaknews.nl!193.141.40.65.MISMATCH!npeer.de.kpn-eurorings.net!npeer-ng0.de.kpn-eurorings.net!border2.nntp.ams2.giganews.com!border4.nntp.ams.giganews.com!border2.nntp.ams.giganews.com!border2.nntp.dca.giganews.com!nntp.giganews.com!newsfeed.news.ucla.edu!nrc-news.nrc.ca!News.Dal.Ca!news.litech.org!news.stack.nl!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: Fri, 10 May 2013 05:29:53 +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> <12gn9wvv1gwfk.10ikfju4rzmnj.dlg@40tude.net> NNTP-Posting-Host: uGUognJZXpdb++Da0QvCqg.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 Content-Type: text/plain; charset=utf-8; format=flowed; delsp=yes Content-Transfer-Encoding: Quoted-Printable Date: 2013-05-10T05:29:53+02:00 List-Id: Le Fri, 10 May 2013 00:19:14 +0200, Randy Brukardt = a =C3=A9crit: > "Dmitry A. Kazakov" wrote in message > news:12gn9wvv1gwfk.10ikfju4rzmnj.dlg@40tude.net... >> On Wed, 8 May 2013 15:27:50 -0500, Randy Brukardt wrote: >> >>> "Dmitry A. Kazakov" wrote in message >>> news:nd22gfeezrwf$.tlj4yyygrwq3$.dlg@40tude.net... >>> ... >>>> Each time you do something with a type you get another one. Otherwi= se = >>>> it >>>> becomes untyped. >>> >>> That way leads to madness, I think. It's better for "types" to be = >>> fairly >>> weak and interoperable. >> >> Weak typing is better? > > Yes, because we need to move beyond typing to other forms of static er= ror > detection. Typing is too rigid to do a good job -- you need to include= > statically known information about the contents of variables and = > parameters, > which can change from line-to-line in a program. I feel the same. I often though typing can't do everything if it comes = with value type checking, while in some occasions, I tried to express ea= ch = validity condition with types and then type checking (that ends to be = crazy, indeed). A simple example, is paired invocation, where whenever a= = sub=E2=80=91program is is invoked, sooner or later, another sub=E2=80=91= program must be = invoked too on the same argument, ex. like `Open` and later `Close`. Thi= s = cannot be expressed with types and indeed requires assertions. But saying =E2=80=9Cweak=E2=80=9D may be erroneously interpreted, and th= en, the type is = still the first place to holds the validity rules. In the example above,= = the paired invocation requirement, could be expressed in the type owning= = these two primitives (there is no way to do it actually, except with = external checking tools and custom rules for this tool). That's just tha= t = showing the type is used according to the rules it defines, could not be= = ensured with classic type checking (there is no type checking to apply = here), it would needs assertions in the sources. In summary I would say: the type is the source of validity rules, but = can't help to check it, so there is a need for something along to types.= = At least, it would have to go beyond values (so far, types just describe= = values). -- = =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