[reikonomusha]

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 do catch real bugs in real code, and I’d prefer those features are there than not there. If you are disappointed, however, then...

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).

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.

On top of it all you get all of the facilities of Lisp, like macros, compile-time evaluation, etc. Coalton code is 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.

It’s still a work in progress, especially in terms of polish and documentation, but it works.

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.

[1] https://github.com/stylewarning/coalton

[2] http://www.shenlanguage.org/

[gumby]

MACLISP had state of the art type checking and compiler optimization, for the 1970s state of the art, and produced better math code than I could write by hand in assembler. These capabilities were used extensively for MACSYMA.

The point of the article wasn't to say that all common lisps support type declaration but to show how easy it is to add support for such decoration (and optional support to boot).

Arbitrary amounts of inference could be added in such declarations before feeding the result to the compiler; the same work could be easily extended for other compilers -- and that other pre-analysis would work there too.

[reikonomusha]

The article described a simpler way for writing DECLARE’s—a feature built-in to Lisp (not a feature the user/author is adding)—and discussed the benefits you could get from such declarations from SBCL (and CMUCL). The same code would not provide much benefit in other implementations of Common Lisp, and the passerby of HN might not gather this nuanced but important detail.

No amount of inference can extend Lisp’s type system to support parametric polymorphism. It’s just not an idea Lisp’s type system can express.

[gumby]

> No amount of inference can extend Lisp’s type system to support parametric polymorphism. It’s just not an idea Lisp’s type system can express.

Well of course it has runtime polymorphism. I assume you mean the metasyntactic polymorphism of, say, C++'s std::vector<foobar>. Yeah, you could sort of get there with some macrology (not even extreme macrology) but you'd probably need to add some call-site sugar which wouldn't be very transparent. Clearly the generic type system could handle it, but there's no inherent representation, which I presume is what you mean.

[dreamcompiler]

Coalton looks very interesting. I'll check it out. Shen was the first thing that came to mind when I saw the article title but I haven't played with it much.

Is it your intent that Coalton work with any ANSI Common Lisp or is it dependent on the extra-special type checking that SBCL does?

[reikonomusha]

Any ANSI Common Lisp. It’s is wholly independent of SBCL’s features.