Why I still Lisp

> I have never had a static type checker (regardless of how sophisticated it is) help me prevent anything more than an obvious error (which should be caught in testing anyway).

This is the static vs dynamic type debate in a nutshell. Personally I think Typescript hits a sweet spot of static typing by default with an escape hatch (via the `any` type) when you need it. I think more self-documenting code makes the tradeoff well worth it (with the added guarantee that the documentation is correct). And most importantly, I like getting feedback from the editor as I'm typing rather than having to write code then run tests, then write some more and perhaps modify the tests, etc.

> I also noticed there is a tendency in lispy languages to avoid introducing variable bindings just for the sake of naming the subexpression, because it often comes with a `(let ((name (subexpression))) rest-of-code)`, which also results in extra tabulation for the rest of the body. Compare with variable introduction in languages like python/js/c++/rust, etc., where such thing wouldn't cause touching the rest of the function/clause. I guess it's more of a 'functional language' artifact, e.g. in Haskell you'd probably have a similar issue.

I have found myself thinking about "Should I really introduce another let form for naming these things I am going to use at the next procedure call, to make it more readable? Or would it make the code less readable, because of the additional indent?". So there is something to this point. Right now, while not writing code, I would say:

The indentation make the scope of the bindings clear. It tells you exactly, until where a binding will be defined. It also allows you to shadow a binding from an outer scope for the purpose of using it in the inner scope. However shadowing should be used with care, because it can also get in the way of readability, if used wrongly. It can however also increase readability, if used well.

In a language like Python, you can only write things at the same level of indentation. It does not make it clear until where these bindings might possibly be used. The scopes are not as separated as in Lispy languages with the let form. That inherently makes it not as readable, I think. "The rest of the function" is not a very precise scope specification. Many bindings might only be used for one or a few subexpressions and not everywhere until the function ends. This only makes sense though, if the code has side effects. Otherwise there will be no difference in where the bindings still exist, because what in Python is the rest of the "function", will be the inner parts of the expression of a procedure in Lispy languages.

I have found myself looking for a thing like let in Python though. I have sometimes thought: "Hey, can't I use a with-block for making a temporary binding?", but that has never worked for me, because I think you need to make a context manager for that? It has never materialized in my style of Python code. (I know Hy, but until it can offer me TCO and lambdas and let forms like Scheme, I am not sure I would like to use it.)

EDIT: Ah and not to forget about let* which can often reduce the amount of indentation a lot. Sometimes I find it good to make use of it.

On the other hand, I've worked with Erlang systems where almost all issues we saw in production would have been prevented by a type-checker.

There are, however, very few ergonomic type systems. At the moment I think Rust is, sadly, the only one.

>I have never had a static type checker (regardless of how sophisticated it is) help me prevent anything more than an obvious error (which should be caught in testing anyway).

Obvious in retrospect is not the same as obvious. And such errors happen all the time, the same way without syntax checks typos happen all the time.

And "caught in testing" is 2 extra steps removed from caught immediately by the syntax checker running as you type or save: writing the tests and running the tests (and being thorough/lucky enough that this part of the code is covered in a test).

>But it is a stupid tool. It can only do so much. So, you now end up with artificial rules about how to satisfy this tool. And things that I know (and can justify or even formally prove for my use cases) are perfectly fine to do are suddenly not.

What thing that violates a type check would be "perfectly fine to do"?

Dynamic languages still have types (since you still need to pass around the right object with the right methods or fields to the call site, else it will raise an exception when you use a method/access a field/run a function on the wrong type).

  def square(value):
     return value*value

If value is not a numeric type, square is not going to be happy. And that's the case with most (all?) dynamic code.

What would be a counter-example that something not satisfying to a type checker would be "perfectly fine to do" in a dynamic language?

(I do accept that the static typed language is better to have generic and/or algebraic types, no make lots of invariants easier to express without ceremony).

What makes it ergonomic in your opinion?