#

## Issue FUNCTION-TYPE-ARGUMENT-TYPE-SEMANTICS Writeup

    Forum:        Cleanup
    Issue:        FUNCTION-TYPE-ARGUMENT-TYPE-SEMANTICS
    References:   CLtL pp 47-48, 158-159
    Category:     CHANGE
    Related-issues: DECLARE-TYPE-FREE
    Edit history: #1, 7 Sept 1988, Walter van Roggen
                  #2, 13 Sept 1988, Walter van Roggen (costs & proposal limitations)
                  #3,  7-Dec-88, Masinter

    Problem description:

    The current description of the specialized FUNCTION type specifier is not very
    useful to program analysis tools and is not very intuitive to programmers
    because the meaning of the argument type specifiers is not restrictive.

    Programmers find it useful to add information about the types of the arguments
    a function expects and about the type(s) that a function may return. This
    information is useful both to human readers of the code as well as to type
    checking programs such as compilers and cross referencers. The only apparent
    way of providing this information is with the FTYPE declaration
    or the FUNCTION type specifier.

    Furthermore, implementations may wish to provide additional optimizations based
    on avoiding type checking or different methods of argument passing. These
    optimizations require the same sort of information about the argument types.

    However, the current definition of FUNCTION type specifiers on pages 47-48 of
    CLtL states that a function such as CONS that is of type
      (FUNCTION (T T) CONS)
    is also of type
      (FUNCTION (FLOAT STRING) LIST).

    The problem is that the argument types aren't restrictive, so no interesting
    matching of types is possible.

    Proposal (FUNCTION-TYPE-ARGUMENT-TYPE-SEMANTICS:RESTRICTIVE)

    This proposal is written as if DECLARE-TYPE-FREE (Version 6, 06-Oct-88)
    is in effect.

    Specify that a declaration of the form

        (ftype (function (arg0-type arg1-type ...) val-type) f))

    implies that any call of the form (f arg0 arg1 ...) within the scope of
    the declaration can be treated as if it were

      (the val-type (f (the arg0-type arg0) (the arg1-type arg1) ...))

    That is, it is an error for any of the arguments not to be of the specified
    types or the result not to be of the specified type. (In particular,
    If any argument is not of the correct type,  the result is not guaranteed
    to be of the specified type.)

    Thus, an FTYPE declaration for a function describes calls to the function,
    not the actual definition of the function.

    Similarly, specify that a declaration of the form
        (type (function (arg0-type arg1-type ...) val-type) fn-valued-variable)

    has the interpretation that, within the scope of the declaration, it
    is an error to call the value of fn-valued-variable with arguments
    not of the specified type; assert that the value resulting from a valid
    call will be of type val-type.

    As with variable type declarations (cf DECLARE-TYPE-FREE), nested declarations
    imply intersections of types, as follows:

    If two (or more) declarations of the form "ftype" are in effect,
    (ftype (function (arg0-type1 arg1-type1 ...) val-type1) f))
    and
    (ftype (function (arg0-type2 arg1-type2 ...) val-type2) f))

    then within the shared scope of the declarations, calls to f can be
    treated as if it were declared
    (ftype (function ((and arg0-type1 arg0-type2) (and arg1-type1 arg1-type2 ...) ...)
                     (and val-type1 val-type2))
           f))

    (It is legitimate to ignore one or all of the declarations in force.)

    If two (or more) type declarations are in effect for a variable, and
    they are both FUNCTION declarations, the declarations combine similarly.

    This proposal does not alter the status (or lack thereof) of other issues
    related to FUNCTION type specifiers: what lambda-list keywords mean, what the
    VALUES type means, what implications there are w.r.t. argument counts, doing
    multiple PROCLAIMs, doing local DECLAREs that shadow other declarations or
    proclamations, describing generic functions incrementally, the result of TYPEP
    with a specialized FUNCTION type, or the nesting and scoping rules for
    FTYPE declarations.

    Example:

      (DEFUN FFF (F)
        (DECLARE (TYPE (FUNCTION (FLOAT STRING) LIST) F))
        ... (FUNCALL F (FOO ...) ...) ... )

    then #'CONS is a valid argument to be passed to FFF because the declared
    type of the argument is consistent with type (FUNCTION (T T) CONS).
    Within FFF, the declaration permits us, for example, to assume that FOO
    returns a FLOAT.

    Rationale:

    The proposal seems most like what users expect.

    Current Practice:

    VAX LISP assumes and makes use of the semantics different than CLtL
    but not exactly what is specified here. Lucid
    has a RESTRICTIVE-FTYPE declaration with these semantics and ignores the
    standard FTYPE declaration. Gold Hill intends to use these declarations in this
    manner.  Many implementations don't make use of these declarations.  At least
    several users make use of declarations assuming the new semantics.

    Cost to Implementors:

    Since most implementations don't make use of function declarations, and since
    those known to do so can be changed easily, the cost should be minimal.

    Cost to Users:

    There may be some existing "imprecise" function declarations.  However, the
    natural tendency when providing these declarations is to be as "descriptive"
    (i.e., restrictive but complete) as possible, both for documentation purposes
    as well as for potential compiler benefits. There cannot have been any uses of
    the specialized FUNCTION type for discrimination. Thus most existing uses are
    probably compatible with this new definition.

    Cost of Non-Adoption:

    There already exists user code on many implementations that assume the
    proposed semantics.  Not adopting this proposal would continue to render
    such code incorrect or at least non-portable.

    Benefits:

    Better type checking and more compiler optimizations should be possible.

    Esthetics:

    This is the what most programmers expect the specialized FUNCTION type to
    mean, particularly those coming from other languages.

    Discussion:

    A declaration of
     (FUNCTION (FIXNUM FIXNUM) CONS)
    is a not proper global declaration for CONS if any program might
    call CONS with arguments that are not FIXNUM.

    The list form of the FUNCTION type specifier is different from most
    type specifiers because it cannot be used for discrimination.
    Thus, the notion of "subtype" does not make sense, since assertions
    about the functional value of a variable are only partially
    about the actual value of the variable and mainly about the
    values that might be passed to the variables (function) value.

Copyright 1996-2005, LispWorks Ltd. All rights reserved.