Static Type Checking in Common Lisp

Hopefully nobody reading the article ends up disappointed knowing that the type checking presented is SBCL-only, working only for a subset of the Common Lisp type system (which itself is large and elaborate), with only informal guarantees of compile-time support, and doesn’t come close to allowing any sort of type checking with polymorphism or sum-types involved. None of those take away from the value SBCL’s type checking provides; the features presented <i>do</i> catch <i>real</i> bugs in <i>real</i> code, and I’d prefer those features are there than not there. If you are disappointed, however, then...<p>Coalton [1] is a project that adds tried-and-true Hindley-Milner type checking to Common Lisp which allows for gradual adoption, in the same way Typed Racket or Hack allows for. You can think of Coalton as an embedded DSL in Lisp that resembles Standard ML or OCaml, but lets you seamlessly interoperate with non-statically-typed Lisp code (and vice versa).<p>It’s really intended as a practical tool to allow parts or most of your codebase to be statically typed, without compromising the dynamic and interactive nature of Common Lisp.<p>On top of it all you get all of the facilities of Lisp, like macros, compile-time evaluation, etc. Coalton code <i>is</i> truly Lisp code, it’s just—at the end of the day—extra syntax to allow a type checker (also Lisp!) to run. As a benefit, it allows quasi-trivial porting of ML-like code to Lisp. Almost all ML construct has a direct correspondence in Coalton.<p>It’s still a work in progress, especially in terms of polish and documentation, but it works.<p>Shen [2] is another interesting project, but I didn’t generally find it very compatible with the ML style of program construction, and it seemed to have goals diverging from being an extension of Lisp, into being some hyper-portable independent language.<p>[1] <a href="https:&#x2F;&#x2F;github.com&#x2F;stylewarning&#x2F;coalton" rel="nofollow">https:&#x2F;&#x2F;github.com&#x2F;stylewarning&#x2F;coalton</a><p>[2] <a href="http:&#x2F;&#x2F;www.shenlanguage.org&#x2F;" rel="nofollow">http:&#x2F;&#x2F;www.shenlanguage.org&#x2F;</a>

I hereby inaugurate Ron&#x27;s third law: for any perceived shortcoming of Common Lisp you can write a macro that fixes it for less effort than it takes to complain about it.

This method of adding static typing to a dynamically typed language is called gradual typing. It works and is sound but can come at a considerable cost if the compiler doesn&#x27;t support it well.<p>Suppose that you have function that you know only returns fixnum, but isn&#x27;t declared as such, and you use that result as the input to a function declared to only take fixnum then the compiler has to add runtime type checks. Even very cheap type checks can cause massive overhead if they are executed in tight loops.<p>Or suppose the fixnum x is given as input to an identity function: (id x). The compiler knows that x is a fixnum, but unless it is sufficiently smart it has no idea that (id x) is one too.

I have to say these type of articles make me want to get into Common Lisp again. Good stuff, thanks! :)

Fantastic. Apparently I am not the only one that has been digging around for more detailed information about how CL implements static typing. There is so much FUD out there from the ??? community(ies) that I ended up sitting down and finding the relevant sections in my lab&#x27;s copy of CLTL2. This article does an excellent job of laying out the consequences of the standard in a way that is clear and understandable, and probably that also includes knowledge about those consequences that was not entirely known at the time (or maybe it was, but just not documented).<p>I kind of wish the author had named his type defun `defunct` though!

Of course you can invoke a type checker inside a language with compile time macros. Did anyone ever doubt that?<p>The interesting question is: what does that type checker actually <i>check</i>? How does it deal with normal lisp functions? How is non-trivial data represented? And what happens when it stumbles upon a runtime macro?<p>And, on a more practical side, how does it access the environment?