3 ms·
The concept is brilliant and excellently demonstrated, but I do want to nitpick the examples a little! Type narrowing can represent “this cannot happen” situat
by cadamsdotcom 4mo ago
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.
- vatsachak 3mo agoType checking is the same as proof verification. It is called the Curry-Howard correspondence
- ltratt 3mo ago> The downside of manually narrowing is more code, but the upside is clarity. This, IMHO, is where things get tricky: quite often, writing more code is at odds with clarity. I don't think there's a simple relation here -- more sometimes is better! -- and for me at least I don't know how to define it any better than "I know it when I see it".