Great video.

If you want to play with a powerful type system check out Raku. It offers gradual types that are a hybrid of dynamic and statically checked.

Basically, you can define a `subset` of a type with a validation predicate. Subsets can be named or anonymous and inline in function signatures.

Another thing that made me think of Raku was your discussion of NULLs. Any type container can be defined or undefined, an undefined Array container `isa` Array. But you can specify whether your annotation means to be specifically only defined or undefined members of the type. So `Int:D` is a defined integer, whereas `Int:U` is undefined, and `Int` is either.

The type specifications combined with multiple dispatch cam make for pretty code.

It's a really interesting language and, in my opinion, worth checking out. It would be great to hear your thoughts on it.

This video convinced me even further that dynamic typing is superior. The speaker basically admitted that static type checking still requires unit tests because types in statically typed languages have too broad/imprecise granularity. I was also thinking about issues related to timing, race conditions and incorrect state mutations; static typing doesn't prevent any of these. IMO, static typing doesn't even begin to address a tiny fraction of all the possible programming mistakes that one might make. IMO its added utility value is often so low that it's basically not worth the mere hassle of having to come up with type definitions.

Personally, when I write a function definition, I always try to visualize the set of possible values that the function will need to handle - So given that I already have that precise set of possible arguments already in my mind as I write the function, it doesn't add any value for me to then formally generalize my function parameters as being integers or strings or some other types which are too broad to effectively constrain my function input to the required level. With static typed languages, merely specifying that a variable is an integer doesn't save me from having to think about what specific subset of integers I mean. For example, if my function only works with odd numbers as input, using the integer type definition will not offer me any additional safety.

I would argue that most functions are like this. The type definitions are never granular enough to guarantee correctness. The type system only protects you from the most basic/obvious mistakes - So obvious that you don't even need the type checker to tell you.