--- layout: ../Site.layout.js --- # Play static games, win static prizes: Common lisp static typing and static program analysis examples - «.sbcl static types» (to "sbcl static types") - «.cl-series compiler-time lazy traversal generation» (to "cl-series compiler-time lazy traversal generation") - «.A Computational Logic For Applicative Common Lisp» (to "A Computational Logic For Applicative Common Lisp") - «.Conclusion» (to "Conclusion") - «.Fin» (to "Fin") In the context of [this classic article on type systems](https://blogs.perl.org/users/ovid/2010/08/what-to-know-before-debating-type-systems.html), I will look at three popular static program analysers that are used with common lisp. These are by no means the only static program analysers popular in lisp. A different example of the perennial lisp obsession with creating programs in concert with static analysis of knowledge is [Kent M. Pitman's Cross Referenced Editor Facility in the interview discussion here](/show/kmp-whither-original-thought) which shows that there is and has been mountains of lisp work in this mileiu over the last century. # steel bank common lisp compiler static type warnings and cost estimates - «sbcl static types» (to ".sbcl static types") ANSI common lisp has many top-tier compilers and two major commercial implementations, but steel bank common lisp (nee, Carnegie Melon University Common Lisp Python Compiler) is the most popular one. When someone tells you oddly fervently that common lisp does not have static typing, privately picture the below while looking into their eyes. You can just scroll down past this. I am just making the point of what detractors are calling lisp's lack of static typing. `~/loady.lisp` is just `(defun myadd (x1 x2) (+ x1 x2))`. ``` CL-USER> (compile-file "~/loady.lisp") ; compiling file "~/loady.lisp" (written 12 JUN 2025 10:31:11 PM): ; file: ~/loady.lisp ; in: DEFUN MYADD ; (+ X1 X2) ; ; note: unable to ; open-code float conversion in mixed numeric operation ; due to type uncertainty: ; The first argument is a NUMBER, not a RATIONAL. ; The second argument is a NUMBER, not a FLOAT. ; ; note: unable to ; open-code float conversion in mixed numeric operation ; due to type uncertainty: ; The first argument is a NUMBER, not a FLOAT. ; The second argument is a NUMBER, not a RATIONAL. ; ; note: unable to ; open-code float conversion in mixed numeric operation ; due to type uncertainty: ; The first argument is a NUMBER, not a RATIONAL. ; The second argument is a NUMBER, not a (OR (COMPLEX SINGLE-FLOAT) ; (COMPLEX DOUBLE-FLOAT)). ; ; note: unable to ; open-code float conversion in mixed numeric operation ; due to type uncertainty: ; The first argument is a NUMBER, not a (OR (COMPLEX SINGLE-FLOAT) ; (COMPLEX DOUBLE-FLOAT)). ; The second argument is a NUMBER, not a RATIONAL. ; ; note: unable to ; open-code float conversion in mixed numeric operation ; due to type uncertainty: ; The first argument is a NUMBER, not a SINGLE-FLOAT. ; The second argument is a NUMBER, not a DOUBLE-FLOAT. ; ; note: unable to ; open-code float conversion in mixed numeric operation ; due to type uncertainty: ; The first argument is a NUMBER, not a DOUBLE-FLOAT. ; The second argument is a NUMBER, not a SINGLE-FLOAT. ; ; note: unable to ; open-code float conversion in mixed numeric operation ; due to type uncertainty: ; The first argument is a NUMBER, not a SINGLE-FLOAT. ; The second argument is a NUMBER, not a (COMPLEX DOUBLE-FLOAT). ; ; note: unable to ; open-code float conversion in mixed numeric operation ; due to type uncertainty: ; The first argument is a NUMBER, not a (COMPLEX DOUBLE-FLOAT). ; The second argument is a NUMBER, not a SINGLE-FLOAT. ; ; note: forced to do GENERIC-+ (cost 10) ; unable to do inline float arithmetic (cost 2) because: ; The first argument is a T, not a DOUBLE-FLOAT. ; The second argument is a T, not a DOUBLE-FLOAT. ; The result is a (VALUES NUMBER &OPTIONAL), not a (VALUES DOUBLE-FLOAT ; &OPTIONAL). ; unable to do inline float arithmetic (cost 2) because: ; The first argument is a T, not a SINGLE-FLOAT. ; The second argument is a T, not a SINGLE-FLOAT. ; The result is a (VALUES NUMBER &OPTIONAL), not a (VALUES SINGLE-FLOAT ; &OPTIONAL). ; etc. ; ; compilation unit finished ; printed 9 notes ; wrote ~/loady.fasl ; compilation finished in 0:00:00.059 ``` Whatever your feeling is, I take it as a comment ([on the Mastodon](https://gamerplus.org/@screwlisp/114673648006484070)). You may peruse the hyperspec [on `declare`ing `types`](https://www.lispworks.com/documentation/HyperSpec/Body/d_type.htm) and [`the`](https://www.lispworks.com/documentation/HyperSpec/Body/s_the.htm) and [JMBR](https://superadditive.com)'s [notes on sbcl declarations here](/programming/jmbrs-short-addendum-on-common-lisp-types/) which contains the references to the CMUCL python compiler reference manual. Let's fix that line: `(defun myadd (x1 x2) (+ x1 x2))` ⮕ `(defun myadd (x1 x2) (declare (fixnum x1 x2) (values integer)) (+ x1 x2))` and `(compile-file #p"~/loady.lisp")` again: ``` CL-USER> (compile-file "~/loady.lisp") ; compiling file "~/loady.lisp" (written 13 JUN 2025 10:32:13 AM): ; file: ~/loady.lisp ; in: DEFUN MYADD ; (+ X1 X2) ; ; note: doing signed word to integer coercion (cost 20), for: ; the first result of inline (signed-byte 64) arithmetic ; ; compilation unit finished ; printed 1 note ; wrote ~/loady.fasl ; compilation finished in 0:00:00.043 ``` I declared that value as an integer, because the sum of two large [fixnum](https://www.lispworks.com/documentation/HyperSpec/Body/t_fixnum.htm)s could be a [bignum](https://www.lispworks.com/documentation/HyperSpec/Body/t_bignum.htm) and the direct superclass of both of those is [integer](https://www.lispworks.com/documentation/HyperSpec/Body/t_intege.htm). In fact, I could have left the `(values integer)` return [type](https://www.lispworks.com/documentation/HyperSpec/Body/d_type.htm) declaration out because the compiler will statically infer that the return is an `integer` rather than a `fixnum` (and estimate this cost) for me anyway, but I was being verbose. I guess a better type declaration might be ``` (defun myadd (x1 x2) (declare ((integer -2305843009213693952 2305843009213693951) x1 x2)) (+ x1 x2)) ``` whence ``` CL-USER> (compile-file "~/loady.lisp") ; compiling file "~/loady.lisp" (written 13 JUN 2025 10:48:34 AM): ; wrote ~/loady.fasl ; compilation finished in 0:00:00.064 ``` where those two numbers are `(truncate most-negative-fixnum 2)` and `(truncate most-positive-fixnum 2)`. On the other hand, I can also just tell `sbcl` that the value's type will be a fixnum: ``` (defun myadd (x1 x2) (declare (fixnum x1 x2) (values fixnum)) (+ x1 x2)) ``` which sbcl will accept ``` CL-USER> (compile-file "~/loady.lisp") ; compiling file "~/loady.lisp" (written 13 JUN 2025 10:53:46 AM): ; wrote ~/loady.fasl ; compilation finished in 0:00:00.084 ``` Let's try `myadd`ing `most-positive-fixnum` to `most-negative-fixnum` then `most-positive-fixnum`. ``` CL-USER> (myadd most-positive-fixnum most-negative-fixnum) -1 CL-USER> (myadd most-positive-fixnum most-positive-fixnum) ; Evaluation aborted on #. ``` → ``` The value 9223372036854775806 is not of type FIXNUM [Condition of type TYPE-ERROR] Restarts: 0: [RETRY] Retry SLIME REPL evaluation request. 1: [*ABORT] Return to SLIME's top level. 2: [ABORT] abort thread (#) Backtrace: 0: (MYADD # #) 1: (SB-INT:SIMPLE-EVAL-IN-LEXENV (MYADD MOST-POSITIVE-FIXNUM MOST-POSITIVE-FIXNUM) #) 2: (EVAL (MYADD MOST-POSITIVE-FIXNUM MOST-POSITIVE-FIXNUM)) --more-- ``` The dynamic type checking caught us violating our earlier static type declaration. Interactive debugging and dynamic types are not my topic here particularly though they are fundamental to lisp. We can see that, confusingly from the famous article above's perspective, common lisp programmers use both incredible static type checking and dynamic type checking, which that article did not expect programming languages would do. Our nuance I guess is that how to do your compile-time static program analysis *is not defined by the ANSI common lisp standard*. This does *not* mean that it is not done - the compiler above is an *extremely* popular one and can be used for static type checking even if your deployment target is another compiler. The [CMUCL reference manual](https://cmucl.org/doc/index.html) basis for this static type checking it refers to can be considered a popular substandard. This is NOT the only *substandard* static program analysis that is popular in common lisp! # The `cl-series` portable macro package - «cl-series compiler-time lazy traversal generation» (to ".cl-series compiler-time lazy traversal generation") When we say [`cl-series`](https://gitlab.common-lisp.net/rtoy/cl-series/\-/wikis/Series-User's-Guide) is a macro package, what we are saying is that all *its* code runs at compile time, around the same step that *sbcl* was reporting all those type warnings and estimated costs above. It uses advanced static analysis to introduce lazy evaluation of `series` to common common lisp useage. (Its mechanism is that it temporarily replaces common constructs like 'let' with 'let-but-it's-also-an-entry-point-to-series'-static-program-analysis`, where it replaces your series code with a tight/efficient in-order lazy traversal in pure common lisp. Since Series is concerned with Series nature expressions rather than ANSI CL expressions per se, it provides its [own static analysis and warnings](https://gitlab.common-lisp.net/rtoy/cl-series/\-/wikis/Series-User's-Guide#basic-restrictions) of restrictions (where it detects that something not-very-statically-optimizable is happening) and violations (something defined to be forbidden in terms of series is happening but success can be faked), where these warning types are documented, focusing on helpful advice on what fixing this restriction or violation warning normally means. # [A Computational Logic For Applicative Common Lisp](https://www.cs.utexas.edu/~moore/acl2/current/manual/index.html?topic=ACL2____ACL2) - «A Computational Logic For Applicative Common Lisp» (to ".A Computational Logic For Applicative Common Lisp") The grandchild of PureLISP by Nqthm theorem prover, ACL2 is a *large* common lisp program that is a first order logic automatic theorem prover where instead of introducing a whole cloth new system such as type-theory proof languages, ACL2's approach is to directly support a huge subset of ANSI common lisp directly - so you can load the same common lisp source file from your common lisp common lisp package into ACL2 to prove a 'book' of ACL2 theorems about your code in a literally equivalent sense that type theorists refer to them as having proved types. However, the approach is fundamentally different to type-theory compile-time-type-checking languages. Instead of introducing a new formal-methods language to learn and perform manually, ACL2 does work in the other direction: A large subset of the common lisp *you already use* is simply available for theorems, and ACL2 takes a fair whack at proving the theorems on its own. (Though ACL2's description of its algorithm, "the waterfall" is that it is 'fully automatic in the sense that once it starts moving, you have no way to control it'. In practice, because ACL2 proves your theorems about your regular lisp source automatically, when it fails to prove your `thm`, this cues you to make a new `defun` or lemma `defthm` that makes the step ACL2 failed on more obvious (or you provide a `:hint`). While it is a subset of common lisp, it has several extensions and restrictions for its first-order-logic proving to work: ACL2 requires that recursive functions obviously terminate (i.e. have a strictly decreasing and finite `measure`). `loop` is replaced by a much-reduced `loop$`, and lambda has an interesting `lambda$` implementation amenable to proving theorems about your common lisp code. # Conclusion - «Conclusion» (to ".Conclusion") Common lisp has mature and extremely popular in the sense of wide-spread use: - aggressive compile-time static type checking as seen in the sbcl compiler - Lazy evaluation pure lisp generating compile-time static program analysis of potentially infinite series with cl-series - Automatic first-order formal theorem proving of literally your regular common lisp source code with ACL2. We modestly addressed the confusion by people who have never used lisp that these three static program analysis programs are programs written in common lisp for use in writing common lisp, rather than static program analysis of common lisp being defined by the standard. This distinction between ANSI common lisp's definition and programs used for analysis of ANSI common lisp programs is probably one reason why the ANSI common lisp standard is apparently immortal. # Fin - «Fin» (to ".Fin") This was a tricky article that I felt I had to write since the demographic is kind of non-lisp-programmers and beginning-lisp-programmers who might get misled by lisp's detractors saying that lisp users do not use static type checking, static program analysis, formal mathematical proofs of their programs and so forth. For that reason, please vigorously critique what I have presented [in this Mastodon thread](https://gamerplus.org/@screwlisp/114673648006484070). My intent continues to be to share tied-up-cultural-knowledge of lisp useage both for newer members of the lisp community, and even to help lisp's detractors at least make less trivially incorrect and not-even-wrong statements about lisp. So please share this article in whatever means and mediums you move in.