screwlisp proposes kittens

Play static games, win static prizes: Common lisp static typing and static program analysis examples

In the context of this classic article on type systems, 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 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

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). You may peruse the hyperspec on declareing types and the and JMBR’s notes on sbcl declarations here 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 fixnums could be a bignum and the direct superclass of both of those is integer. In fact, I could have left the (values integer) return type 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 myadding 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 #<TYPE-ERROR expected-type: FIXNUM datum: 9223372036854775806>.

→

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 (#<THREAD "repl-thread" RUNNING {1001380003}>)

Backtrace:
  0: (MYADD #<unavailable argument> #<unavailable argument>)
  1: (SB-INT:SIMPLE-EVAL-IN-LEXENV (MYADD MOST-POSITIVE-FIXNUM MOST-POSITIVE-FIXNUM) #<NULL-LEXENV>)
  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 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

When we say cl-series 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 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

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

Common lisp has mature and extremely popular in the sense of wide-spread use:

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

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.

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.

screwlisp proposes kittens