I would like to add that optimizations may also be performed in addition to type-checking (type-checking, by the way, depends on safety optimization level). What's also handy is that you can specify the optimization levels (space, safety, speed, debug) per function or per file (or in a `locally' block).

Function return types may also be specified, with serapeum's ->, it may be as simple as (-> f (fixnum fixnum) boolean) for instance, right above the function.

Classes and structs let you specify types for slots.

Expressions may be typed with `the' special operator aka (the fixnum (first list)).

PS CL has gradual typing.

Dang. I didn’t know sbcl did this. I’ve never used it, but now I want to try. Thanks!

Type systems at least as rich as Hindley-Milner are pretty much table stakes in 2022. Common Lisp's type system is not as rich as Hindley-Milner. I believe it doesn't even support user-defined parametric types (so it's kind of like pre-generics Go in that regard). It lets you type function args, but it doesn't incorporate the args' types into the function type.

So no, Common Lisp's type system, even with static type checking enabled, is not adequate for software engineering in the present day. Coalton, however, solves many of these problems.

What languages in common use in 2022 support a Hindley-Milner type system? This sounds a bit like pointless academic gatekeeping…

Basically, any statically typed language with parametric polymorphism, so Ada, C++, Java, C#, Rust, TypeScript, Python with static-typing support, post-Delphi Pascal, and recently Go all qualify.

Parametric polymorphism != Hindley-Milner, not even basically. H-M is a construction for describing and ascertaining types of terms in a lambda calculus. Many of those languages don't even typically idiomatically achieve polymorphism through generic types (though of course it's possible), but instead from subtype and ad hoc polymorphism. I don't think it's accurate to imply their designs orbit H-M.

I don't want to belabor on technicalities. Your original point was about "table stakes" for type systems in order to be relevant for modern-day software engineering. While I agree a language that attempts to incorporate fashionable computational constructs (like variable binding and lambda terms) ought to derive its type system from something H-M-esque—if only because it's so well understood—it's certainly not a requirement for the language to be taken seriously, and it's certainly not without significant peril in the presence of mutation constructions. I honestly think C, vanilla Common Lisp, and pre-generic Go are sufficiently disparate examples of that.

Type inference is hinted at in a 1934 paper by Haskell Curry on "functionality" (i.e. types) for combinatory logic. Max Newman (Turning mentor and leader of the Colossus project at Bletchley Park) published a paper in 1943 giving the first algorithm for type inference for the lambda calculus that I know of.

Comparing Go generics to those other languages is putting on some very rosy colored glasses. The primary design goal of the current generics implementation appears to have been discouraging their use. I hope they'll iterate on it, but at this point they're basically painful and annoying at best.

Table stakes for what? Fucking around with types for 6 months while someone builds a competitor in a weekend?