Despite our progress most of the conversation continues to be about safety. But, there is another dimension of type checking that people rarely consider, and I think it is at the root of much of the disagreement. It has to do with the ergonomics of checking itself.
When I work in a dynamically typed language, I spend a lot of time at the REPL. I create some candidate data and then an expression, and I see how the expression evaluates it. It’s a very fluid style of working and it is practicable even in non-REPL environments. What it has in its favor is immediacy. Quite often you can focus on the core of an algorithm and do a proof of concept without a questioning bystander (the type checker) breaking your flow.
Working in Haskell or any other statically typed language, is a different experience. The type checker has questions, and it is adamant about them, refusing to let you move forward until they are answered. Often, I’m ok with that. They are good questions, and most of the time they really should be answered. The question is: when?
I often wish I worked in a language where I could start dynamic and end statically. There are a number of languages with optional type systems, but they aren’t the ones that I use. I can imagine writing the core of an algorithm and then gradually tightening the conditions as it comes into focus. More than a tool, this would be a practice: progressive type elaboration. To get there, we probably need as much control of our type system, minute to minute as we program, as we have of our tests.