> At present, I don’t know anyone who has seriously used languages like OCaml or Haskell and was happy to return to languages with less sophisticated type systems (though an interesting project can sometimes justify such a technological regression).

Recovered typeaholic here. I still occasionally use OCaml and I primarily wrote F# and Haskell for years. I've been quite deep down the typing rabbit hole, and I used to scorn at dynamically typed languages.

Now I love dynamic typing - but not the Python kind - I prefer the Scheme kind - latent typing. More specifically, the Kernel[1] kind, which is incredibly powerful.

> I think the negative reputation of static type checking usually stems from a bad experience.

I think this goes two ways. Most people's experience with dynamic typing is the Python kind, and not the Kernel kind.

To be clear, I am not against static typing, and I love OCaml - but there are clear cases where static typing is the wrong tool - or rather, no static typing system is sufficient to express problems that are trivial to write correctly with the right dynamic types.

Moreover, some problems are inherently dynamic. Take for example object-capabilities (aka, security done right). Capabilities can be revoked at any time. It makes no sense to try and encode capabilities into a static type system - but I had such silly thoughts when I was a typeaholic, and I regularly see people making the same mistake. Wouldn't it be better to have a type system which can express things which are dynamic by nature?

And this is my issue with purely statically typed systems: They erase the types! I don't want to erase the types - I want the types to be available at runtime so that I can do things with them that I couldn't do at compile time - without me having to write a whole new interpreter.

My preference is for Gradual Typing[2], which lets us use both worlds. Gradual typing is static typing with a `dynamic` type in the type system, and sensible rules for converting between dynamic and static types - no transitivity in consistency.

People often mistake gradual typing with "optional typing" - the kind that Erlang, Python and Typescript have - but that's not correct. Those are dynamic first, with some static support. Gradual typing is static-first, with dynamic support.

Haskell could be seen as Gradual due to the presence of `Data.Dynamic`, but Haskell's type system, while a good static type system, doesn't make a very good dynamic type system.

Aside, my primary language now is C, which was the first language I learned ~25 years ago. I regressed! I came back to C because I was implementing a gradually typed language and F#/OCaml/Haskell were simply too slow to make it practical, C++/Rust were too opinionated and incompatible with what I want to achieve, and C (GNU dialect) let me have almost complete control over the CPU, which I need to make my own language good enough for practical use. After writing C for a while I learned to love it again. Manually micro-optimizing with inline assembly and SIMD and is fun!

[1]:https://web.cs.wpi.edu/~jshutt/kernel.html

[2]:https://jsiek.github.io/home/WhatIsGradualTyping.html

> Now I love dynamic typing - but not the Python kind - I prefer the Scheme kind - latent typing.

Could you elaborate on the difference? I was under the impression that "latent typing" just means "values, not variables, have types", which would make Python (without type annotations) latently typed as well.

I've had a similar experience. After many years of strict typing, including two years of writing full-time Rust, I've come completely around on dynamic typing. Attempting to encode a system in types creates a host of consequent issues, that in turn need their own complex solutions. At some point you lose sight of the business logic and are sort of just building artifice for the sake of feeding earlier artifice.

(Sort of like how OOP was introduced to solve the problem of structuring code, but then we needed a profusion of ever-more-complex design patterns to fix the issues only ever introduced by OOP in the first place.)

I'm coming to be a big fan of functional dynamic languages. You can just let go of entire categories of CS complexity. No need for generics without types, no need for locks without mutability, etc. Actual fearless concurrency.

This in turn has freed me to write actual business logic, without the constant need to stop and make sacrifices to the CS complexity god.