Question from a non-user: Compile-time Checking
Bennu Strelitzia
will make separate postings about. Sorry if they are obvious or
otherwise-unsuitable questions, but I have spent some time reading
trying to answer them and have not been able to do so.
Compile-time checking
Let's say I am simultaneously a fan and not a fan of compile-time type
checking.
I would like something that happens more-automatically for the user, and
is much more fine grained than it is today, but I like the ability of a
compiler and user to be able to reason mathematically about what
possible results can be returned by a function.
What sorts of mechanisms are commonly built for Lisp implementations
today that allow you to either assert through some sort of annotation or
derive that if this set of values serve as inputs to the function, you
get this possible set of values as returns (considering exceptions also
as returns?)?
It obviously does not have to look like a typical statically typed
language. I would like to be able to do much better than that as a
custom expansion without sticking to typical classes of today's type
systems, i.e. specify that when this function is given positive prime
numbers it is known to return odd integers greater than 1000.
Pillsy
wrote:
[...]
> What sorts of mechanisms are commonly built for Lisp implementations
> today that allow you to either assert through some sort of annotation or
> derive that if this set of values serve as inputs to the function, you
> get this possible set of values as returns (considering exceptions also
> as returns?)?
Lisp implementations provide the ability to make statements about the
types of objects bound to variables or returned by functions using the
DECLARE and DECLAIM forms. There's
no defined, standard way of using that information; it's a quality of
implementation issue. Most implementations will use it to compile more
efficient code in some circumstances; a few implementations will also
use it as a way to provide better run-time or compile-time type-
checking.
One family of implementations[1] actually does do type inference based
on this sort of information/
> It obviously does not have to look like a typical statically typed
> language. I would like to be able to do much better than that as a
> custom expansion without sticking to typical classes of today's type
> systems, i.e. specify that when this function is given positive prime
> numbers it is known to return odd integers greater than 1000.
You actually could specify such a thing, but such a specification
almost certainly wouldn't be used very effectively by the compiler.
The Common Lisp type system *does* allow you to define types based on
whether some prediciate function (like a user-provided PRIMEP or the
standard ODDP) is satisfied, you can specify that a type is an integer
that's confined to a certain range, and that one type is the
intersection of two other types.
Cheers,
Pillsy
[1] Those based on CMUCL. This family includes the popular, free SBCL
implementation.
Rahul Jain
> What sorts of mechanisms are commonly built for Lisp implementations
> today that allow you to either assert through some sort of annotation or
> derive that if this set of values serve as inputs to the function, you
> get this possible set of values as returns (considering exceptions also
> as returns?)?
Type inferencers? SBCL has a really good one.
> It obviously does not have to look like a typical statically typed
> language. I would like to be able to do much better than that as a
> custom expansion without sticking to typical classes of today's type
> systems, i.e. specify that when this function is given positive prime
> numbers it is known to return odd integers greater than 1000.
You can't specify those kind of type dependencies in standard CL. SBCL
allows you to add a type inferencer of your own if you know something
that requires more complex reasoning than SBCL's built-in mechamisms do.
--
Rahul Jain
rj...@nyct.net
Professional Software Developer, Amateur Quantum Mechanicist
Kaz Kylheku
> What sorts of mechanisms are commonly built for Lisp implementations
> today that allow you to either assert through some sort of annotation or
> derive that if this set of values serve as inputs to the function, you
> get this possible set of values as returns (considering exceptions also
> as returns?)?
Good Lisp compilers perform type inference, which can identify obvious
errors.
ANSI Common Lisp provides declarations. Functions, variables, and the
results of expressions, can be annotated with indications of type.
This information can be used by a type inferencing compiler in order
to provide enhanced diagnostics, but that's not its main purpose.
The purpose of type declarations is optimization.
Declarations have to be used with care because they constitute a promise
from the programmer to the implementation: ``trust me, this variable A
really is a fixnum, thanks to other steps that have been taken''.
Duane Rettig
wrote:
> I would appreciate any pointers you may have on a few issues which I
> will make separate postings about. Sorry if they are obvious or
> otherwise-unsuitable questions, but I have spent some time reading
> trying to answer them and have not been able to do so.
>
> Compile-time checking
>
> Let's say I am simultaneously a fan and not a fan of compile-time type
> checking.
You'll make a good Common Lisper.
> I would like something that happens more-automatically for the user, and
> is much more fine grained than it is today, but I like the ability of a
> compiler and user to be able to reason mathematically about what
> possible results can be returned by a function.
Most CL implementations use "type inferencing", or "type propagation",
to reason at compile-time about what kinds of types variables will
hold at run-time.
> What sorts of mechanisms are commonly built for Lisp implementations
> today that allow you to either assert through some sort of annotation or
> derive that if this set of values serve as inputs to the function, you
> get this possible set of values as returns (considering exceptions also
> as returns?)?
In Allegro CL, the type propagation mechanism is available for viewing
in the :explain declaration interface:
http://www.franz.com/support/documentation/8.1/doc/compiling.htm#decl-help-1.
Also available in our newest version (scheduled to be released
shortly) is the ability to perform runtime checks that variables are
indeed receiving types that were declared or inferred.
Duane
Nicolas Neuss
> Most CL implementations use "type inferencing", or "type propagation",
> to reason at compile-time about what kinds of types variables will
> hold at run-time.
>
>> What sorts of mechanisms are commonly built for Lisp implementations
>> today that allow you to either assert through some sort of annotation or
>> derive that if this set of values serve as inputs to the function, you
>> get this possible set of values as returns (considering exceptions also
>> as returns?)?
>
> In Allegro CL, the type propagation mechanism is available for viewing
> in the :explain declaration interface:
> http://www.franz.com/support/documentation/8.1/doc/compiling.htm#decl-help-1.
> Also available in our newest version (scheduled to be released
> shortly) is the ability to perform runtime checks that variables are
> indeed receiving types that were declared or inferred.
A related question: I would be interested in a compilation that takes
into account also existing CLOS method definitions and uses them for
type inference. So, e.g.
(defgeneric testit (obj)
(:method ((obj string)) "Hello")
(:method ((obj integer)) (format nil "~D" obj)))
(defun call-testit ()
(testit 3/5))
should generate a compiler warning that a necessary method is not yet
defined.
Although this should only be used for the generation of warnings during
compilation time, not for actual optimization (at least not by default,
because generating new methods later on is rather often important), I
think that this would be an enormous help. How much work would it be to
enhance the compiler in that way? (This question is also directed to
other CL developers, if they should read this.) Especially, given that
several CL's do some type inference anyhow.
Nicolas
Christophe Rhodes
> A related question: I would be interested in a compilation that takes
> into account also existing CLOS method definitions and uses them for
> type inference. So, e.g.
>
> (defgeneric testit (obj)
> (:method ((obj string)) "Hello")
> (:method ((obj integer)) (format nil "~D" obj)))
>
> (defun call-testit ()
> (testit 3/5))
>
> should generate a compiler warning that a necessary method is not yet
> defined.
I can't really convince myself that this is a good idea in general; the
dynamic nature of CLOS makes it really hard for any concrete inference
to be made, not only because of adding, removal and redefinition of
methods, but also CHANGE-CLASS, redefinition of method combinations, and
so on and so on. For methods mostly working on objects whose classes
are structure classes or built-in-classes, a certain amount could be
done automatically.
> Although this should only be used for the generation of warnings during
> compilation time, not for actual optimization (at least not by default,
> because generating new methods later on is rather often important), I
> think that this would be an enormous help. How much work would it be to
> enhance the compiler in that way? (This question is also directed to
> other CL developers, if they should read this.) Especially, given that
> several CL's do some type inference anyhow.
I think that this is somewhere that users can (with a little bit of
assistance) customize behaviour for their own needs, given their own
knowledge of the characteristics of their codebase -- a CLOS user can
know that they're not going to mess around with CHANGE-CLASS, whereas
the implementation can't in general. Here's an example, with several
details missing, to illustrate what a user can do:
(defun class-for-constant (form env)
(class-of (sb-int:constant-form-value form env)))
(defun class-for-variable (form env)
(let* ((decls (nth-value 2 (sb-cltl2:variable-information form env)))
(type (cdr (assoc 'type decls))))
;; highly conservative
(when (and (symbolp type) (not (eql type t)))
(find-class type nil))))
(defun class-for-form (form env)
(cond
((constantp form env) (class-for-constant form env))
((symbolp form) (class-for-variable form env))
(t nil)))
which could then be used as follows
(defgeneric foo (x))
(define-compiler-macro foo (&whole form &environment env x)
(let ((class (class-for-form x env)))
(when class
(let ((methods (sb-mop:compute-applicable-methods-using-classes
#'foo (list class))))
(when (null methods)
(sb-int:style-warn
"(probably) no applicable methods in call to ~S" 'foo)))))
form)
#| test cases -- compile and evaluate each form in succession:
(defun bar ()
(foo 1))
(defmethod foo ((x number)) 3)
(defun baz ()
(foo 2))
(defun quux (x)
(declare (type string x))
(foo x))
(defmethod foo ((x array)) "hello, world")
(defun frob (x)
(declare (type string x))
(foo x))
|#
Christophe
Nicolas Neuss
very nice:-) I like it.
Thank you,
Nicolas
P.S.: I get the impression that very much in this direction could be
achieved with relatively little work by an expert like you, and I am
astonished that this is not done to a much larger extent. At least for
me, redefinition outside the program development cycle is really rare.
So here is another idea in a similar direction (although probably much
harder to do): I think it would be very helpful if type inference would
be more universally applied for function and method definitions, e.g.:
;;; compiling this could automatically establish the ftype
;;; (function () STRING), recompiling such a form would warn and
;;; establish a new type
(defun foo ()
"Hi")
;;; and compiling this could then warn:
(defun bar ()
(+ 3 (foo)))
;;; same for methods:
(defmethod foox (obj)
(:method ((obj string)) string)
(:method ((obj number)) (* number 2)))
;;; these could generate warnings
(defun bar1 () (+ 3 (foox "Hi")))
(defun bar2 () (concatenate 'string (foox 4)))
Christophe Rhodes <cs...@cantab.net> writes:
--
PD Dr. Nicolas Neuss University Karlsruhe Tel: 0049-721-608-7634
Email: ne...@math.uni-karlsruhe.de
WWW: <http://www.mathematik.uni-karlsruhe.de/~neuss>
Nicolas Neuss
Here is a (slightly more general) wrapper which I want to try out a
little bit to see if it is of help:
(defmacro defgen (name args &body rest)
`(progn
(defgeneric ,name ,args ,@rest)
(define-compiler-macro ,name (&whole form &environment env ,@args)
(let ((classes
(list ,@(loop for arg in args collect
`(or (class-for-form ,arg env) t)))))
(let ((methods (sb-mop:compute-applicable-methods-using-classes
(function ,name) classes)))
(when (null methods)
(sb-int:style-warn
"(probably) no applicable methods in call to ~S" 'foo))))
form)))
(defgen fooz (x y)
(:method (x (y number)) 1) )
(compile nil (lambda () (fooz 2 "Hi"))) ; warning
(compile nil (lambda () (fooz 2 5))) ; no warning
Thanks again,
Nicolas
Christophe Rhodes
> So here is another idea in a similar direction (although probably much
> harder to do): I think it would be very helpful if type inference would
> be more universally applied for function and method definitions, e.g.:
>
> ;;; compiling this could automatically establish the ftype
> ;;; (function () STRING), recompiling such a form would warn and
> ;;; establish a new type
>
> (defun foo ()
> "Hi")
>
> ;;; and compiling this could then warn:
>
> (defun bar ()
> (+ 3 (foo)))
Tom Burdick calls this "turning on the good switch": in SBCL, set
*DERIVE-FUNCTION-TYPES* (a slight misnomer; I think it really means "use
derived function types") to true. The reason it's not on by default is
that you can get to situations where the compiler gets fairly confused;
if I do the above, then redefine FOO to return 3, I get the run-time
error message "The value 3 is not of type NUMBER." from calling (bar)
because the old type information for FOO was in effect when compiling
BAR; you'd have to recompile BAR too in general.
> ;;; same for methods:
> (defmethod foox (obj)
> (:method ((obj string)) string)
> (:method ((obj number)) (* number 2)))
>
> ;;; these could generate warnings
> (defun bar1 () (+ 3 (foox "Hi")))
> (defun bar2 () (concatenate 'string (foox 4)))
Again, I think in simple cases like this things are doable but mostly
CLOS code is not of this general form. I'm willing to be shown examples
where it really does help, though, and there are mechanisms that can be
used to perform this kind of type derivation automatically.
Christophe
Pascal Costanza
> Hello Christophe,
>
> very nice:-) I like it.
>
> Thank you,
> Nicolas
>
> P.S.: I get the impression that very much in this direction could be
> achieved with relatively little work by an expert like you, and I am
> astonished that this is not done to a much larger extent. At least for
> me, redefinition outside the program development cycle is really rare.
This is probably an example of the 80/20 problem: 80% of all CLOS users
probably use only 20% of its features. However, which 20% of its
features are used is varied, to the extent that you cannot make strong
general assumptions.
Although it would probably indeed be interesting to define a
'conservative' subset of CLOS where most of the MOP and some of the ANSI
features are not available, and if you commit to that subset, you would
get some stronger compile-time guarantees...
Pascal
--
My website: http://p-cos.net
Common Lisp Document Repository: http://cdr.eurolisp.org
Closer to MOP & ContextL: http://common-lisp.net/project/closer/
Rainer Joswig
Pascal Costanza <p...@p-cos.net> wrote:
> On 17/12/2009 14:16, Nicolas Neuss wrote:
> > Hello Christophe,
> >
> > very nice:-) I like it.
> >
> > Thank you,
> > Nicolas
> >
> > P.S.: I get the impression that very much in this direction could be
> > achieved with relatively little work by an expert like you, and I am
> > astonished that this is not done to a much larger extent. At least for
> > me, redefinition outside the program development cycle is really rare.
>
> This is probably an example of the 80/20 problem: 80% of all CLOS users
> probably use only 20% of its features. However, which 20% of its
> features are used is varied, to the extent that you cannot make strong
> general assumptions.
>
> Although it would probably indeed be interesting to define a
> 'conservative' subset of CLOS where most of the MOP and some of the ANSI
> features are not available, and if you commit to that subset, you would
> get some stronger compile-time guarantees...
>
>
> Pascal
That problem is not new. See 'Dylan'. But the goal was more in
the direction of runtime efficiency ('application delivery capability')
and not so much 'compile-time guarantees' for
reducing bugs by compile-time type checking.
Nicolas Neuss
> Nicolas Neuss <last...@math.uni-karlsruhe.de> writes:
>
>> So here is another idea in a similar direction (although probably much
>> harder to do): I think it would be very helpful if type inference would
>> be more universally applied for function and method definitions, e.g.:
>>
>> ;;; compiling this could automatically establish the ftype
>> ;;; (function () STRING), recompiling such a form would warn and
>> ;;; establish a new type
>>
>> (defun foo ()
>> "Hi")
>>
>> ;;; and compiling this could then warn:
>>
>> (defun bar ()
>> (+ 3 (foo)))
>
> Tom Burdick calls this "turning on the good switch": in SBCL, set
> *DERIVE-FUNCTION-TYPES* (a slight misnomer; I think it really means "use
> derived function types") to true. The reason it's not on by default is
> that you can get to situations where the compiler gets fairly confused;
> if I do the above, then redefine FOO to return 3, I get the run-time
> error message "The value 3 is not of type NUMBER." from calling (bar)
> because the old type information for FOO was in effect when compiling
> BAR; you'd have to recompile BAR too in general.
OK, this is understandable. However, I agree with Tom Burdick on this.
I remember that when I started using CMUCL/SBCL I liked these kind of
typechecks even if that meant some recompilation. And I also remember
that I was in recent times somewhat disappointed that several type
discrepancies (like the above) went through unnoticed by SBCL. Hmm, was
the default changed at some time, or do I remember those fondly from
CMUCL?
>> ;;; same for methods:
>> (defmethod foox (obj)
>> (:method ((obj string)) string)
>> (:method ((obj number)) (* number 2)))
>>
>> ;;; these could generate warnings
>> (defun bar1 () (+ 3 (foox "Hi")))
>> (defun bar2 () (concatenate 'string (foox 4)))
>
> Again, I think in simple cases like this things are doable but mostly
> CLOS code is not of this general form. I'm willing to be shown
> examples where it really does help, though, and there are mechanisms
> that can be used to perform this kind of type derivation
> automatically.
I can only point to my own missing of that feature, although it did not
hurt me that bad, that I asked about it on the mailing list. (I also
dimly remember one or two quite simple and unnecessary type bugs
occuring when I patched my webserver on-the-fly, but I am not sure if
they would have been prevented by this. I will pay more attention in
the future and report when it would have helped me.)
I think to become really useful it would probably have to be combined
with more frequent use of CLOS slot type declarations (and propagation
of that information to readers/writers).
Nicolas
Nicolas Neuss
> On 17/12/2009 14:16, Nicolas Neuss wrote:
>
>> P.S.: I get the impression that very much in this direction could be
>> achieved with relatively little work by an expert like you, and I am
>> astonished that this is not done to a much larger extent. At least
>> for me, redefinition outside the program development cycle is really
>> rare.
>
> This is probably an example of the 80/20 problem: 80% of all CLOS
> users probably use only 20% of its features. However, which 20% of its
> features are used is varied, to the extent that you cannot make strong
> general assumptions.
>
> Although it would probably indeed be interesting to define a
> 'conservative' subset of CLOS where most of the MOP and some of the
> ANSI features are not available, and if you commit to that subset, you
> would get some stronger compile-time guarantees...
Note that in the ideal case I would only want compile time warnings or
hints, that is, dynamicity always rules and nothing has to be given up.
Perhaps a MOP power user or someone using ContextL might be annoyed by
unnecessary warnings, however, I would have to look more carefully on
ContextL to see if this really is a problem there.
Nicolas
Lars Rune Nøstdal
wrote:
Not user if this has been mentioned already, but DECLAIM + FTYPE will
generate compile-time feedback wrt. types, at least in SBCL:
CL-USER> (progn
(declaim (ftype (function (fixnum fixnum) (values fixnum
&optional))
sum))
(defun sum (x y)
(+ x y)))
SUM
CL-USER> (lambda () (sum 3 2))
#<FUNCTION (LAMBDA ()) {10044FA419}>
CL-USER> (lambda () (sum 3.14 2))
; in: LAMBDA NIL
; (SUM 3.14 2)
;
; caught WARNING:
; Asserted type FIXNUM conflicts with derived type
; (VALUES (SINGLE-FLOAT 3.14 3.14) &OPTIONAL).
; See also:
; The SBCL Manual, Node "Handling of Types"
;
; compilation unit finished
; caught 1 WARNING condition
#<FUNCTION (LAMBDA ()) {10045BF069}>
CL-USER>
Looking at your example, I do not think CL (or any other Lisp) gives
you what you want here out-of-the-box. It provides what you need for
to build exactly what you're looking for (a DSL), though.