FWIW, SBCL is pretty good at optimizing away dynamic type checks if you help it out.

Here are some examples under:

    (declaim (optimize (speed 2)))

First example is a generic multiplication. x and y could be _any_ type at all.

    (defun fn (x y) (* x y))

If we disassemble this function, we get the following:

    ; disassembly for FN
    ; Size: 34 bytes. Origin: #x1001868692                        ; FN
    ; 92:       488975F8         MOV [RBP-8], RSI
    ; 96:       4C8945F0         MOV [RBP-16], R8
    ; 9A:       498BD0           MOV RDX, R8
    ; 9D:       488BFE           MOV RDI, RSI
    ; A0:       FF142540061050   CALL [#x50100640]                ; SB-VM::GENERIC-*
    ; A7:       4C8B45F0         MOV R8, [RBP-16]
    ; AB:       488B75F8         MOV RSI, [RBP-8]
    ; AF:       C9               LEAVE
    ; B0:       F8               CLC
    ; B1:       C3               RET
    ; B2:       CC0F             INT3 15                          ; Invalid argument count trap

Note that it calls `GENERIC-*` which probably checks a lot of things and has a decent overhead.

Now, if we tell it that x and y are bytes, it's going to give us much simpler code.

    (declaim (ftype (function ((unsigned-byte 8) (unsigned-byte 8)) (unsigned-byte 16)) fn-t))
    (defun fn-t (x y) (* x y))

The resulting code uses the imul instruction.

    ; disassembly for FN-T
    ; Size: 15 bytes. Origin: #x1001868726                        ; FN-T
    ; 26:       498BD0           MOV RDX, R8
    ; 29:       48D1FA           SAR RDX, 1
    ; 2C:       480FAFD7         IMUL RDX, RDI
    ; 30:       C9               LEAVE
    ; 31:       F8               CLC
    ; 32:       C3               RET
    ; 33:       CC0F             INT3 15                          ; Invalid argument count trap*

I think it's three things:

1. Bringing abstractions that are only possible with static types, like ad hoc polymorphism via type classes. For example, type classes allow polymorphism on the return type rather than the argument types. Something like

    (declare stringify (Into :a String => :a -> :a -> String))
    (define (stringify a b)
      (str:concat (into a) (into b)))

    ; COALTON-USER> (coalton (stringify 1 2))
    ; "12"

The function `into` is not possible in a typical dynamically typed language, at least if we aim for the language to be efficient. It only takes one argument, but what it does depends on what it's expected to return. Here, it's expected to return a string, so it knows to convert the argument type to a string (should knowledge of how to do that be known by the compiler). Common Lisp's closest equivalents would be

    (concatenate 'string (coerce a 'string) (coerce b 'string))

which, incidentally, won't actually do what we want.

2. Making high performance more accessible. It's possible to get very high performance out of Common Lisp, but it usually leads to creating difficult or inextensible abstractions. A lot of very high performance Common Lisp code ends up effectively looking like monomorphic imperative code; it's the most practical way to coax the compiler into producing efficient assembly.

Coalton, though, has an optimizing compiler that does (some amount of) heuristic inlining, representation selection, stack allocation, constant folding, call-site optimization, code motion, etc. Common Lisp often can't do certain optimizations because the language must respect the standard, which allows things to be redefined at run-time, for example. Coalton's delineation of "development" and "release" modes gives the programmer the option to say "I'm done!" and let the compiler rip through the code and optimize it.

3. Type safety, of course, in the spirit of ML/Haskell/etc.

In CL you can't declare, for example, a proper-list-of type, which is to say a type which accepts a second type and represents a proper list containing only members of that second type.

  (deftype Proper-List-Of (subtype)
    `(or Null
         (Cons ,subtype
               (Proper-List-Of ,subtype))))

Doesn't work (for example). There kind of are ways to work around it to some extent with satisfies and ad-hoc predicate generation, but Coalton is a true value add in that aspect.

I highly recommend watching [0] for an introduction to Coalton in the context of CL. Specifically it provides an excellent example of how the type system makes the language more expressive (by making it more composable) while also improving performance (e.g. because it can prove that certain optimizations are safe and thus can automatically generate the type annotations).

0. https://www.youtube.com/watch?v=of92m4XNgrM

CL is strongly typed but not statically typed. The compiler generally doesn't complain ahead of time that your function is going to do math on a string because it was called incorrectly. Typically a runtime condition will be signalled when it hits that point and you can sort it out from there.

Coalton moves that to the compilation step so you get an error back the instant you send the form to the REPL.

I’ve looked at it rather than used it, but what it brings is ML-style polymorphism. Type safety is a given in that case, which may or may not be the case with CL (I’ll let others argue that one).

Strong static typing is an absolute must for large scale software engineering. CL code can be made very performant without it, but there are enormous development speed and correctness gains to be had by type-checking programs before they are executed rather than at runtime.

It's 2025, people. Dynamic languages for serious projects were a 90s fad, hopefully never to be repeated.