From ... Path: archiver1.google.com!news1.google.com!sn-xit-02!supernews.com!news.tele.dk!small.news.tele.dk!193.251.151.101!opentransit.net!newsfeed.icl.net!newsfeed.esat.net!nslave.kpnqwest.net!nloc.kpnqwest.net!nmaster.kpnqwest.net!nreader2.kpnqwest.net.POSTED!not-for-mail Newsgroups: comp.lang.lisp Subject: Re: FUNCTION types References: Mail-Copies-To: never From: Erik Naggum Message-ID: <3223996816584348@naggum.net> Organization: Naggum Software, Oslo, Norway Lines: 41 User-Agent: Gnus/5.09 (Gnus v5.9.0) Emacs/21.1 MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Date: Fri, 01 Mar 2002 18:40:11 GMT X-Complaints-To: newsmaster@KPNQwest.no X-Trace: nreader2.kpnqwest.net 1015008011 193.71.199.50 (Fri, 01 Mar 2002 19:40:11 MET) NNTP-Posting-Date: Fri, 01 Mar 2002 19:40:11 MET Xref: archiver1.google.com comp.lang.lisp:27664 * Christophe Rhodes > I don't know. I would say not, because > (defun foo (x) > (declare (type (function (integer) integer) x)) > ... (funcall #'x 2.5)) > can have different semantics from > (defun foo (x) > (declare (type (function (real) integer) x)) > ... (funcall #'x 2.5)) * Kent M Pitman | I disagree. Semantics here is not formal semantics, but text definition | semantics. The definition of a function is mostly that it returns t for | functionp and that it works as a first argument for funcall. The | difference you are discussing is an efficiency difference that occurs in | the world where the promise you have made is true; if the promise you | have made is not true, you do not have a valid program. And as such, the | semantic effect in the valid program case is unaffected by the | declaration. It seems intuitive to me that validity of a program is a semantic issue. That is, when the former of Christophe's examples is compiled, it should signal an error because the compiler can determine that the promise is a lie. This is the usual definition of "semantics". As for all this function type stuff, it appears to me that most of what we want to know about the function types should fall out from something like (typep #'foo '(function (fixnum fixnum) boolean)), but a quick look at typep dispells any hope of this working: It is in fact an _error_ to use typep to query an object for its function type. End of story. :) | I somehow expect to get beaten up about my newly consed term | "anti-optimization" but I use the term perhaps to provoke discusson if | there is any to be had. You might enjoy . /// 2002-03-01 -- In a fight against something, the fight has value, victory has none. In a fight for something, the fight is a loss, victory merely relief.