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.4 required=5.0 tests=BAYES_00,FORGED_GMAIL_RCVD, FORGED_MUA_MOZILLA,FREEMAIL_FROM autolearn=no autolearn_force=no version=3.4.4 X-Google-Thread: 103376,2078ce7aac45af5b X-Google-NewGroupId: yes X-Google-Attributes: gida07f3367d7,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII-7-bit Received: by 10.66.90.8 with SMTP id bs8mr1031598pab.24.1353069352576; Fri, 16 Nov 2012 04:35:52 -0800 (PST) Path: s9ni19603pbb.0!nntp.google.com!Xl.tags.giganews.com!border1.nntp.dca.giganews.com!nntp.giganews.com!local2.nntp.dca.giganews.com!news.giganews.com.POSTED!not-for-mail NNTP-Posting-Date: Fri, 16 Nov 2012 06:35:51 -0600 Date: Fri, 16 Nov 2012 07:35:51 -0500 From: "Peter C. Chapin" User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:16.0) Gecko/20121028 Thunderbird/16.0.2 MIME-Version: 1.0 Newsgroups: comp.lang.ada Subject: Re: Ada202X : Adding functors References: <0114d327-9f9f-4ad2-9281-56331d11a90c@googlegroups.com> <15w6caje3zsh$.t5nqtwoa77x5$.dlg@40tude.net> In-Reply-To: Message-ID: X-Usenet-Provider: http://www.giganews.com X-Trace: sv3-uh4a+gD+BgfHUxcCIpabWHliRQJ9AGjFAWfbfnnTeZk6wEverdzWWMIE8/qyZed8N/KF+jlKbCNfhLd!tRDFB82iAcTRY4VMnxaxl69y8B9iuOd59+weCbFG6zz29FgiyE9jJNivBba53NE= X-Complaints-To: abuse@giganews.com X-DMCA-Notifications: http://www.giganews.com/info/dmca.html X-Abuse-and-DMCA-Info: Please be sure to forward a copy of ALL headers X-Abuse-and-DMCA-Info: Otherwise we will be unable to process your complaint properly X-Postfilter: 1.3.40 X-Original-Bytes: 3434 Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Date: 2012-11-16T07:35:51-05:00 List-Id: On 11/16/2012 01:09 AM, Randy Brukardt wrote: > There's more to a function contract than just the type-and-result-profile! > To truly statically check such things, you also have to match the > precondition, the postcondition, the exception contract, the global in/out > usage, and so on. (Matching doesn't necessarily mean exact equivalence, of > course, which makes it even harder.) I should probably first make it clear that I'm not necessarily advocating for the addition of lambda expressions to Ada. My posts in this thread are only to say that lambda expressions are not necessarily any more weakly typed than any other kind of expression (as Dmitry asserts). Anyway, it is certainly true that the contract extends beyond the type-and-result-profile. In that respect a function type is a richer entity than, say, type Integer... of course. Yet one could imagine a hypothetical language in which some of this additional richness was packed into the function type either with appropriate syntax or some sort of extra-linguistic annotations. In that case, parameters of higher order subprograms could declare this additional information, making it available for static analysis. The full contract of a function includes its semantics as well. It would be interesting to speculate on what it would take to describe the semantics of a function with some suitable formal notation and decorate declarations with that information for purposes of static analysis. For example: procedure Process_With(X : Integer, F : Some_Function_Type with Semantics => ( -- Semantics of required function written in Z (for example) )) is begin -- etc... end Process_With; This is the other extreme on a scale starting with just the type-and-result profile of F embedded in its type. We can arbitrarily draw a line on the scale and say everything to the left of that line is "weak" and everything to the right is "strong" but the line is still arbitrary. Peter