Local Reasoning for Global Properties

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.