[codingkoi]

I’m not sure I follow your analogy. I think the dynamism of a list is separate from the type system. I can say I have a list of integers but that doesn’t limit its size.

I can think of instances where that might be useful and I think there’s even work being done in that direction in things like Idris that I really know very little about.

There are trade offs in everything. I’m definitely a fan of dynamic type systems especially things like Lisp and Smalltalk where I can interact with the running system as I go, and not having to specify types up front helps with that. Type inference will get you close to that in a more static system, but it can only do so much.

The value I see in static type systems comes from being able to rely on the tooling to help me reason about what I’m trying to build, especially as it gets larger. I think of this as being something like what Doug Englebert was pointing at when he talked about augmented intelligence.

I use Python at work and while there are tools that can do some pretty decent static analysis of it, I find myself longing for something like Rust more and more.

Another example I would point to beyond the blog post I previously mentioned is Rust’s serde library. It totally allows you to round trip data while only specifiying the parts you care about. I don’t think static type systems are as static as most like to think. It’s more about knowns and unknowns and being explicit about them.