Subject: Re: FUNCTION types
From: Erik Naggum <erik@naggum.net>
Date: Fri, 01 Mar 2002 18:40:11 GMT
Newsgroups: comp.lang.lisp
Message-ID: <3223996816584348@naggum.net>

* 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 <url http://www.pgh.net/~newcomer/optimization.htm>.

///                                                             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.