I wish there was a Lisp-like language that was statically typed and compiled to optimized native code. The closest thing I know of is Nim, which has the programmability, but not the simple syntax.
Coalton* is a language that interoperates natively with Common Lisp, and has a type system that exceeds the expressiveness of Haskell 98 (but not modern GHC Haskell).
It compiles to native, highly optimized machine code.
CL is often seen as "dynamic" but it's better than that: we compile our code with a keystroke and we instantly get compile-time type warnings and errors. It is not fully statically typed, but it is still way better than say Python. Usually, type checks happen at the functions' boundaries: this expected a int but was given a string, this argument is declared but unused etc. Add in Coalton, and you're approaching a Haskell experience. And that happens in our tight read-eval-print-loop, the feedback is instant. We can also do many things at compile time (macros etc). It's better than one might think.
Probably doesn't cover the 'optimized native code' part but it obviously could, like many programming languages it is, practically speaking, a one-man show.
Not only is Shen inherently statically-typed (it's not annotations over a dynamic core language) but the type system is based on sequent calculus and is expressive and powerful. It would be nice to see what a Nim-sized community could do with it over five to ten years.
Shen looks interesting, but I can't figure out how to install it. I've entered a Common Lisp REPL in the downloaded directory and entered (load "install.lsp"), which printed out a lot of stuff. Now what?
I do not have much personal experience, but SBCL's type inference is supposed to be decent/comparable to the Franz/Allegro/Lisp Works commercial options. I'm not sure if anyone has done "declare-density needed to achieve xyz perf" cross comparisons or the like.
There is also https://en.wikipedia.org/wiki/Stalin_(Scheme_implementation) which was doing lifetime analysis waaay back in the mid 90s, but I don't think Suskind had a declare system at all in Stalin. So, places where inference did not work were probably just "slow to be fixed by users tweaking code" to make inference better. I think he was mostly his own main user.
Both Coalton & Carp do look interesting. There can be complaints with how "prefix notation" scales to large expressions. Cython is a gradually typed Python, but late noughties ideas in metaprogramming/macros/etc. never quite took off.
There can be an undesirable effect of gradual/optional static types that code starts off "lazy" and then can require surprisingly large efforts to tighten down, especially in team settings. Even with profiling/90-10 heuristic rules, a later dev trying to optimize earlier lazy work can still be 10X, especially if type dynamism was really leaned upon. So, at least having an easy switch to force early/in-development static typing on original authors is likely a good thing (or at least strongly encourage with warnings...).
The experience of writing nim is very different from the experience of writing common lisp. Nim may be more mutable than c, but that is not saying much.
> How do you optimize code without knowing the types of variables?
Guesswork, static analysis, experiment etc. JSC does all kinds of black magic to make JavaScript run fast.
For a large amount of programs (basically all "classical" programs like you'd read about in the past rather than modern apps) you have a fairly clear path through the code for their data, this means that you can optimize that path.
This doesn't mean the performance will be as good as a statically typed language but keep in mind 90% of compiler optimization is basically useless on many programs vs. the 10% that makes the important bits run fast.
The Mike Pall method uses a typed SSA intermediate language, and adds trace guards anywhere it can't guarantee a single type. LuaJIT optimizes fairly well.
Because Common Lisp is dynamic, you can redefine adder with more information for the compiler to optimize with (such as types or ability to freely inline). The compiler is part of the runtime (which really ups the programmability of the language too, you can teach SBCL's compiler new optimization rules to output even better assembly). So if you Know What You're Doing, you can get rid of the generic add by declaring the expected argument and return types (e.g. a fixnum) and redefining the function:
Note SBCL still has some safety and debugging bits in there. You can tell it you Really Know What You're Doing, and do so locally so you don't put the rest of your code at risk:
Because of the use of ftype, SBCL will let you know against certain kinds of errors elsewhere, at compile time:
* (defun mistake () (adder 5 "5"))
; in: DEFUN MISTAKE
; (ADDER 5 "5")
;
; caught WARNING:
; Constant "5" conflicts with its asserted type FIXNUM.
; See also:
; The SBCL Manual, Node "Handling of Types"
;
; compilation unit finished
; caught 1 WARNING condition
MISTAKE
* (defun mistake2 () (adder 5 (subseq "555" 0 1)))
; in: DEFUN MISTAKE2
; (ADDER 5 (SUBSEQ "555" 0 1))
;
; caught WARNING:
; Derived type of (SB-KERNEL:VECTOR-SUBSEQ* SB-C::SEQ SB-C::START SB-C::END) is
; (VALUES (SIMPLE-ARRAY CHARACTER (1)) &OPTIONAL),
; conflicting with its asserted type
; FIXNUM.
...
(You would normally see these as you go as you send forms or whole files/buffers to the REPL from your editor, but you can also hook up a sort of 'linting' tool to catch them earlier, or at least fail CI jobs. I use vim rather than emacs and can detect such issues at file save-time; with some work on the underlying tooling it would be possible to detect them when leaving insert mode or switching buffers.)
Of course, because Lisp is dynamic, these are just "warnings" because you can always just redefine (and recompile) these things to fix issues without having to restart your program, or recompile the whole system yet again. And when you leave debugging on or even increase its priority during development, you get an experience in iterative creation unmatched by anything else.