Re: Issue: FUNCTION-TYPE-REST-LIST-ELEMENT, FUNCTION-DECLARATION issues

[Masinter.pa@Xerox.COM]

I think I understand and agree with most of what you say, in particular "I think
that we should either entirely flush the concept of "function types" or change
the theory behind them.  The CLtL interpretation is well-defined, but not very
useful. " 

There are two components to your proposal: (1) what is allowed (and what it
means), and (2) how it is described in the standard.

I like the part of your proposal which is to change the interpretation of
function declarations to mean an implicit assertion of argument and value types
(the "restrictive interpretation"). 

I like defining  (declare (type (function (frob grid) bunker) x)) to mean

 (funcall x y z) has implicitly means  (the bunker (funcall (the function x)
(the frob y) (the grid z)))


I don't see, however, that there is much leverage to removing FUNCTION from the
section on type specifiers. It would do some violence to the otherwise useful
concept of 
(deftype binary-arithmetic () '(function (number number) number))

to be used in

(declare (ftype binary-arithmetic x y z)) .

I don't see at all that (funcall #'foo x y) doesn't mean (the t (funcall #'foo
(the integer x) (the integer y)))) given (declare (function foo (integer
integer) t)). 

In the type propagation rules, you can transform funcall and apply expressions
using the asserted value of the function argument, and the asserted value type
of #'name is derived from the asserted ftype of name. 

In this interpretation, AND would distribute nicely, 

Given (proclaim '(function foo (s1 t1) v1)) and (declare (function foo (s2 t2)
v2)) you could assert that

(foo x y) => (the (and v1 v2) (foo (the (and s1 s2) x) (the (and t1 t2) y))).

(OR doesn't distribute as nicely, e.g., given (declare (ftype (or (function (s1
t1) v1) (function (s2 t2) v2)) foo)),  there isn't a simple way to describe the
type assertions made for (foo x y). 

 We might even want to explicitly allow FUNCTION declarations in THE
expressions, as in

(funcall (the binary-arithmetic x)  y z).