The concept is brilliant and excellently demonstrated, but I do want to nitpick the examples a little!
Type narrowing can represent “this cannot happen” situations!
List -> NonEmptyList, for example. NonEmptyList would refuse to be constructed from an empty list & check for emptiness in its remove() method..
Same for narrowing states A, B and C down to “state A cannot happen here” ie. only B and C are possible. That’s just a new enum!
Typescript’s compiler can automatically perform narrowing.
The downside of manually narrowing is more code, but the upside is clarity. The other downside is the system ends up fussier about what it’ll accept.
What’s a thought experiment though, is the huge value of codifying enforcement mechanisms for properties we desire. This lets the computer verify those properties itself without human intervention. “Does the code compile?” on steroids. There’s tremendous leverage in giving the nondeterministic part of the computer tools to verify things deterministically, and letting it use them itself.
Defensive checks are good and it's the compiler's job to optimize them away.
A simple comment can tell future readers that it's not actually expected to be possible.
Interesting. In the Rust world extensions like Verus, I think, are trying to enable exactly what the author is discussing. Perhaps worth a look:
https://github.com/verus-lang/verus
The concept is brilliant and excellently demonstrated, but I do want to nitpick the examples a little!
Type narrowing can represent “this cannot happen” situations!
List -> NonEmptyList, for example. NonEmptyList would refuse to be constructed from an empty list & check for emptiness in its remove() method..
Same for narrowing states A, B and C down to “state A cannot happen here” ie. only B and C are possible. That’s just a new enum!
Typescript’s compiler can automatically perform narrowing.
The downside of manually narrowing is more code, but the upside is clarity. The other downside is the system ends up fussier about what it’ll accept.
What’s a thought experiment though, is the huge value of codifying enforcement mechanisms for properties we desire. This lets the computer verify those properties itself without human intervention. “Does the code compile?” on steroids. There’s tremendous leverage in giving the nondeterministic part of the computer tools to verify things deterministically, and letting it use them itself.
Type checking is the same as proof verification. It is called the Curry-Howard correspondence