alt Hacker NewsWhile others have addressed the programming case for tagged unions, I want to add that, to a logician, tagged unions are the natural construct corresponding to "logical or".
In intuitionistic logic (which is the most basic kind from which to view the Curry-Howard or "propositions-as-types" correspondence), a proof of "A or B" is exactly a choice of "left" or "right" disjunct together with a corresponding proof of either A or B. The "choice tag" is part of the "constructive data" telling us how to build our proof of "A or B". Translated back into the language of code, the type "A | B" would be exactly a tagged union.
Replies
I disagree. Something of type "A" should, according to basic propositional logic, also be of type "A or B". That's the case for an untagged union, but not for a tagged union (because of wrapping), which is decidedly illogical.
When A and B are disjoint, you don't need the tag unless you for some reason you require that `Maybe<Maybe<T>> != Maybe<T>` holds true and don't like the collapsing semantics of unions where `Maybe<Maybe<T>> == Maybe<T>`
In practice, the cohabitants in Option/Result types are almost always disjoint. So you spend time wrapping/unwrapping Some/Ok/Err for no value add.