by sparkie | 2025-08-14 08:17:26+00:00
> 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