Goals of cl-form-types

[digikar99]

I am beginning to wonder if we might have underestimated the problem of type checking. Or if I'm misunderstanding the goals of cl-form-types.

In particular, consider cl:the and declare type:

CLHS writes about the:

the specifies that the values[1a] returned by form are of the types specified by value-type. The consequences are undefined if any result is not of the declared type.

As such, in my understanding, cl:the is effectively useless for purposes of type determination or checking. While SBCL checks for types specified using the operator, at least a few other implementations like CCL do not. The run time type of (the foo-type bar-form) is solely determined by bar-form on CCL.

CL-USER> (cl-form-types:form-type `(let (a)
                                     (setq a 5)
                                     (the string a))
                                  nil)
(AND STRING T)
CL-USER> (let (a)
           (setq a 5)
           (the string a))
5

Similarly, about declare type, the consequences are undefined if the run-time type of variable differs from declared type:

The interpretation of a type declaration is as follows:

1. During the execution of any reference to the declared variable within the scope of the declaration, the consequences are undefined if the value of the declared variable is not of the declared type.
2. During the execution of any setq of the declared variable within the scope of the declaration, the consequences are undefined if the newly assigned value of the declared variable is not of the declared type.
3. At the moment the scope of the declaration is entered, the consequences are undefined if the value of the declared variable is not of the declared type.

That. That sounds like declare type is effectively useless on non-SBCL-like implementations, unless it is followed by manual type checks. So, would the goals of cl-form-types be stated as merely to deduce the declared type of the form, rather than (what I understood as) run-time type of form?

[alex-gutev]

The goal of cl-form-types is to deduce the type of a form based on information available at compile-time, such as the forms and type/ftype declarations as well as other information. The type deduced by cl-form-types may be a supertype of the actual runtime type, however it may not be a subtype or a completely unrelated type. I'll get into what happens when a subtype or unrelated type is supplied in a the form or type declaration, further on.

It is intended that this information is used for optimization purposes such as selecting the correct method of a generic-function at compile-time. This library isn't intended as a type checking extension for CL though in theory there is nothing precluding it from being used in the implementation of such an extension. However, implementing such an extension would require a lot more work and a lot more than the basic functionality that is provided by this library. Think of cl-form-types as a slightly more advanced version of trivial-form-types.

Now it is possible that a user, declares a variable to be of a type which is either a subtype of or is completely unrelated to the variable's runtime type. This may lead to incorrect optimizations being applied, such as the wrong generic-function method being chosen at compile-time. However, given that the hyperspec clearly states that the consequences of doing so are undefined, the onus is on the user to not declare a variable's type, and similarly not declare a form's type using the, unless he/she is absolutely sure the variable will hold a value of that type at runtime. This gives us some guarantee that the type information given in type declarations and the forms is correct, or at the very least it should be in order for the program to have a "defined behavior", even without cl-form-types being used. This does however imply that you should not use type declarations or the forms if you're not absolutely sure of what you're doing. This is the reason why I designed static-dispatch as an "opt-in" optimization library, rather than the optimizations being on by default.