4 ms·

I think there is a strong case that ADTs (algebraic data types) aren't so great after all. Specifically, the "tagged" unions of ADT languages like Haskell are a

by cubefox 10mo ago

I think there is a strong case that ADTs (algebraic data types) aren't so great after all. Specifically, the "tagged" unions of ADT languages like Haskell are arguably pretty clearly inferior to the "untagged" unions of TypeScript or Scala 3. Because the latter actually behave like a logical "or" rather than an artificial construct that needs to be wrapped and unwrapped.

jesse__ 10mo ago
> "tagged" unions of ADT languages like Haskell are arguably pretty clearly inferior to the "untagged" unions of TypeScript dude .. wut?? Explain to me exactly how this is true, with a real world example. From where I stand, untagged unions are useful in an extremely narrow set of circumstances. Tagged unions, on the other hand, are incredibly useful in a wide variety of applications.
- cubefox 10mo ago
  Example: Option<> types. Maybe a function returns an optional string, but then you are able to improve the guarantee such that it always returns a string. With untagged unions you can just change the return type of the function from String|Null to String. No other changes necessary. For the tagged case you would have to change all(!) the call sites, which expect an Option<String>, to instead expect a String. Completely unnecessary for untagged unions. A similar case applies to function parameters: In case of relaxed parameter requirements, changing a parameter from String to String|Null is trivial, but a change from String to Option<String> would necessitate changing all the call sites. > From where I stand, untagged unions are useful in an extremely narrow set of circumstances. Tagged unions, on the other hand, are incredibly useful in a wide variety of applications. Any real world example?
  - rastrian 10mo ago
    I think your Option/String example is a real-world tradeoff, but it’s not a slam-dunk “untagged > tagged.” For API evolution, T | null can be a pragmatic “relax/strengthen contract” knob with less mechanical churn than Option<T> (because many call sites don’t care and just pass values through). That said, it also makes it easier to accidentally reintroduce nullability and harder to enforce handling consistently, the failure mode is “it compiles, but someone forgot the check.” In practice, once the union has more than “nullable vs present”, people converge to discriminated unions ({ kind: "ok", ... } | { kind: "err", ... }) because the explicit tag buys exhaustiveness and avoids ambiguous narrowing. So I’d frame untagged unions as great for very narrow cases (nullability / simple widening), and tagged/discriminated unions as the reliability default for domain states. For reliability, I’d rather pay the mechanical churn of Option<T> during API evolution than pay the ongoing risk tax of “nullable everywhere. My post argues for paying costs that are one-time and compiler-enforced (refactors) vs costs that are ongoing and human-enforced (remembering null checks).
    - cubefox 10mo ago
      I believe there is a misunderstanding. The compiler can check untagged unions just as much as it can check tagged unions. I don't think there is any problem with "ambiguous narrowing", or "reliability". There is also no risk of "nullable everywhere": If the type of x is Foo|Null, the compiler forces you to write a null check before you can access x.bar(). If the type of x is Foo, x is not nullable. So you don't have to remember null checks (or checks for other types): the compiler will remember them. There is no difference to tagged unions in this regard.
      - rastrian 10mo ago
        I think we mostly agree for the nullable case in a sound-enough type system: if Foo | null is tracked precisely and the compiler forces a check before x.bar, then yes, you’re not “remembering” checks manually, the compiler is. Two places where I still see tagged/discriminated unions win in practice: 1. Scaling beyond nullability. Once the union has multiple variants with overlapping structure, “untagged” narrowing becomes either ambiguous or ends up reintroducing an implicit tag anyway (some sentinel field / predicate ladder). An explicit tag gives stable, intention-revealing narrowing + exhaustiveness. 2. Boundary reality. In languages like TypeScript (even with strictNullChecks), unions are routinely weakened by any, assertions, JSON boundaries, or library types. Tagged unions make the “which case is this?” explicit at the value level, so the invariant survives serialization/deserialization and cross-module boundaries more reliably. So I’d summarize it as: T | null is a great ergonomic tool for one axis (presence/absence) when the type system is enforced end-to-end. For domain states, I still prefer explicit tags because they keep exhaustiveness and intent robust as the system grows. If you’re thinking Scala 3 / a sound type system end-to-end, your point is stronger; my caution is mostly from TS-in-the-wild + messy boundaries.
        cubefox 10mo ago
        I think the real promise of "set-theoretic type systems" comes when don't just have (untagged) unions, but also intersections (Foo & Bar) and complements/negations (!Foo). Currently there is no such language with negations, but once you have them, the type system is "functionally complete", and you can represent arbitrary Boolean combination of types. E.g. "Foo | (Bar & !Baz)". Which sounds pretty powerful, although the practical use is not yet quite clear.
  - jesse__ 10mo ago
    > For the tagged case you would have to change all(!) the call sites Yeah, that's exactly why I want a tagged union; so when I make a change, the compiler tells me where I need to go to do updates to my system, instead of manually hunting around for all the sites. --- The only time an untagged union is appropriate is when the tag accounts for an appreciable amount of memory in a system that churns through a shit-ton of data, and has a soft or hard realtime performance constraint. Other than that, there's just no reason to not use a tagged union, except "I'm lazy and don't want to", which, sometimes, is also a valid reason. But it'll probably come back to bite you, if it stays in there too long.
    - cubefox 10mo ago
      > > For the tagged case you would have to change all(!) the call sites > Yeah, that's exactly why I want a tagged union; so when I make a change, the compiler tells me where I need to go to do updates to my system, instead of manually hunting around for all the sites. You don't have to do anything manually. There is nothing to do. Changing the return type of a function from String|Null to String is completely safe, the compiler knows that, so you don't have to do any "manual hunting" at call sites.
      - jesse__ 10mo ago
        The String|null example is just a nullable type; it's not an interesting use of unions either way. The conversation starts when it's Foo|Bar|Baz I'm unfamiliar with typescript, so in that language I don't have an opinion either way, but in C, you pretty much always want the tag
        cubefox 10mo ago
        C doesn't support any untagged unions (or intersections) in the modern sense. In a set-theoretic type system, if you want to call a method of Foo, and the type of your variable is Foo|Bar|Baz, you have to do a type check for Bar and Baz first, otherwise the compiler won't compile.
pastel8739 10mo ago
Most of the time when I use untagged unions, I end up adding a tag and logic to case on it anyway…
adamddev1 10mo ago
I at first thought it was nice to save the wrapping, but you save yourself sooo much pain, ugliness and mistakes pattern matching trying to distinguish the types once you just use tagged unions.
- rastrian 10mo ago
  I think you’re both pointing at the same tradeoff: “untagged” unions feel lighter, but you often pay it back in ad-hoc narrowing (shape checks/heuristics) and ambiguity once variants overlap. Tagged unions/ADTs make the discriminant explicit, which is exactly why they tend to be reliability-friendly: exhaustive matches + explicit constructors reduce “guessing” and refactor breakage. That said, I agree the ergonomics matter, TS-style discriminated unions are basically “tagged” too once you add a kind field, for example.
jonlong 10mo ago
While 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.
- cubefox 10mo ago
  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.
  - jonlong 10mo ago
    Well, I have outlined the usual story of logic as it corresponds to programming (as has been accepted for at least some five decades now); it strains credulity to claim that logic is illogical. Now I do see where you are coming from; under a set-theoretic interpretation with "implies" as "subset", "or" as "union", and "and" as "intersection", the fact that "A implies (A or B)" tells us that an element of the set A is also an element of the set "A union B". However, this is not the interpretation that leads to a straightforward correspondence between logic and programming. For example, we would like "A and B" to correspond to the type of pairs of elements of A with elements of B, which is not at all the set-theoretic intersection. And while "(A and B) implies A", we do not want to say a value of type "(A, B)" also has type "A". (E.g., if a function expects an "A" and receives an "(A, A)", we are at an impasse.) So "implies" should not be read programmatically as a subtyping relation; instead, "A implies B" tells us that there is a function taking a value of type A to a value of type B. In the case of "A implies (A or B)", that function takes its input and tags it as belonging to the left disjunct! Another perspective I must mention: given a proof of "A or B" and another of "(A or B) implies C", how can we combine these into a simpler proof of just "C"? A proof of "(A or B) implies C" must contain both a proof a "A implies C" and a proof of "B implies C", and we could insert into one those proofs a proof of A or a proof of B. But we have to know which one we have! (This is a very short gloss of a much deeper story, where, under Curry-Howard, proof simplification corresponds to computation, and this is another way of describing a function call that does a case-analysis of a tagged union (or "sum type").) Now "union and intersection" types with the set-theoretic properties you are hinting at have indeed been studied (see, for example, Section 15.7 of Pierce's "Types and Programming Languages"). But they do not replace the much more familiar "sum and product types", and do not play the central role of "or" and "and" in the correspondence of programming to logic.

by cubefox 10mo ago

jesse__ 10mo ago

> "tagged" unions of ADT languages like Haskell are arguably pretty clearly inferior to the "untagged" unions of TypeScript dude .. wut?? Explain to me exactly how this is true, with a real world example. From where I stand, untagged unions are useful in an extremely narrow set of circumstances. Tagged unions, on the other hand, are incredibly useful in a wide variety of applications.

cubefox 10mo ago
Example: Option<> types. Maybe a function returns an optional string, but then you are able to improve the guarantee such that it always returns a string. With untagged unions you can just change the return type of the function from String|Null to String. No other changes necessary. For the tagged case you would have to change all(!) the call sites, which expect an Option<String>, to instead expect a String. Completely unnecessary for untagged unions. A similar case applies to function parameters: In case of relaxed parameter requirements, changing a parameter from String to String|Null is trivial, but a change from String to Option<String> would necessitate changing all the call sites. > From where I stand, untagged unions are useful in an extremely narrow set of circumstances. Tagged unions, on the other hand, are incredibly useful in a wide variety of applications. Any real world example?
- rastrian 10mo ago
  I think your Option/String example is a real-world tradeoff, but it’s not a slam-dunk “untagged > tagged.” For API evolution, T | null can be a pragmatic “relax/strengthen contract” knob with less mechanical churn than Option<T> (because many call sites don’t care and just pass values through). That said, it also makes it easier to accidentally reintroduce nullability and harder to enforce handling consistently, the failure mode is “it compiles, but someone forgot the check.” In practice, once the union has more than “nullable vs present”, people converge to discriminated unions ({ kind: "ok", ... } | { kind: "err", ... }) because the explicit tag buys exhaustiveness and avoids ambiguous narrowing. So I’d frame untagged unions as great for very narrow cases (nullability / simple widening), and tagged/discriminated unions as the reliability default for domain states. For reliability, I’d rather pay the mechanical churn of Option<T> during API evolution than pay the ongoing risk tax of “nullable everywhere. My post argues for paying costs that are one-time and compiler-enforced (refactors) vs costs that are ongoing and human-enforced (remembering null checks).
  - cubefox 10mo ago
    I believe there is a misunderstanding. The compiler can check untagged unions just as much as it can check tagged unions. I don't think there is any problem with "ambiguous narrowing", or "reliability". There is also no risk of "nullable everywhere": If the type of x is Foo|Null, the compiler forces you to write a null check before you can access x.bar(). If the type of x is Foo, x is not nullable. So you don't have to remember null checks (or checks for other types): the compiler will remember them. There is no difference to tagged unions in this regard.
    - rastrian 10mo ago
      I think we mostly agree for the nullable case in a sound-enough type system: if Foo | null is tracked precisely and the compiler forces a check before x.bar, then yes, you’re not “remembering” checks manually, the compiler is. Two places where I still see tagged/discriminated unions win in practice: 1. Scaling beyond nullability. Once the union has multiple variants with overlapping structure, “untagged” narrowing becomes either ambiguous or ends up reintroducing an implicit tag anyway (some sentinel field / predicate ladder). An explicit tag gives stable, intention-revealing narrowing + exhaustiveness. 2. Boundary reality. In languages like TypeScript (even with strictNullChecks), unions are routinely weakened by any, assertions, JSON boundaries, or library types. Tagged unions make the “which case is this?” explicit at the value level, so the invariant survives serialization/deserialization and cross-module boundaries more reliably. So I’d summarize it as: T | null is a great ergonomic tool for one axis (presence/absence) when the type system is enforced end-to-end. For domain states, I still prefer explicit tags because they keep exhaustiveness and intent robust as the system grows. If you’re thinking Scala 3 / a sound type system end-to-end, your point is stronger; my caution is mostly from TS-in-the-wild + messy boundaries.
      - cubefox 10mo ago
        I think the real promise of "set-theoretic type systems" comes when don't just have (untagged) unions, but also intersections (Foo & Bar) and complements/negations (!Foo). Currently there is no such language with negations, but once you have them, the type system is "functionally complete", and you can represent arbitrary Boolean combination of types. E.g. "Foo | (Bar & !Baz)". Which sounds pretty powerful, although the practical use is not yet quite clear.
- jesse__ 10mo ago
  > For the tagged case you would have to change all(!) the call sites Yeah, that's exactly why I want a tagged union; so when I make a change, the compiler tells me where I need to go to do updates to my system, instead of manually hunting around for all the sites. --- The only time an untagged union is appropriate is when the tag accounts for an appreciable amount of memory in a system that churns through a shit-ton of data, and has a soft or hard realtime performance constraint. Other than that, there's just no reason to not use a tagged union, except "I'm lazy and don't want to", which, sometimes, is also a valid reason. But it'll probably come back to bite you, if it stays in there too long.
  - cubefox 10mo ago
    > > For the tagged case you would have to change all(!) the call sites > Yeah, that's exactly why I want a tagged union; so when I make a change, the compiler tells me where I need to go to do updates to my system, instead of manually hunting around for all the sites. You don't have to do anything manually. There is nothing to do. Changing the return type of a function from String|Null to String is completely safe, the compiler knows that, so you don't have to do any "manual hunting" at call sites.
    - jesse__ 10mo ago
      The String|null example is just a nullable type; it's not an interesting use of unions either way. The conversation starts when it's Foo|Bar|Baz I'm unfamiliar with typescript, so in that language I don't have an opinion either way, but in C, you pretty much always want the tag
      - cubefox 10mo ago
        C doesn't support any untagged unions (or intersections) in the modern sense. In a set-theoretic type system, if you want to call a method of Foo, and the type of your variable is Foo|Bar|Baz, you have to do a type check for Bar and Baz first, otherwise the compiler won't compile.

pastel8739 10mo ago

Most of the time when I use untagged unions, I end up adding a tag and logic to case on it anyway…

adamddev1 10mo ago

I at first thought it was nice to save the wrapping, but you save yourself sooo much pain, ugliness and mistakes pattern matching trying to distinguish the types once you just use tagged unions.

rastrian 10mo ago
I think you’re both pointing at the same tradeoff: “untagged” unions feel lighter, but you often pay it back in ad-hoc narrowing (shape checks/heuristics) and ambiguity once variants overlap. Tagged unions/ADTs make the discriminant explicit, which is exactly why they tend to be reliability-friendly: exhaustive matches + explicit constructors reduce “guessing” and refactor breakage. That said, I agree the ergonomics matter, TS-style discriminated unions are basically “tagged” too once you add a kind field, for example.

jonlong 10mo ago

While 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.

cubefox 10mo ago
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.
- jonlong 10mo ago
  Well, I have outlined the usual story of logic as it corresponds to programming (as has been accepted for at least some five decades now); it strains credulity to claim that logic is illogical. Now I do see where you are coming from; under a set-theoretic interpretation with "implies" as "subset", "or" as "union", and "and" as "intersection", the fact that "A implies (A or B)" tells us that an element of the set A is also an element of the set "A union B". However, this is not the interpretation that leads to a straightforward correspondence between logic and programming. For example, we would like "A and B" to correspond to the type of pairs of elements of A with elements of B, which is not at all the set-theoretic intersection. And while "(A and B) implies A", we do not want to say a value of type "(A, B)" also has type "A". (E.g., if a function expects an "A" and receives an "(A, A)", we are at an impasse.) So "implies" should not be read programmatically as a subtyping relation; instead, "A implies B" tells us that there is a function taking a value of type A to a value of type B. In the case of "A implies (A or B)", that function takes its input and tags it as belonging to the left disjunct! Another perspective I must mention: given a proof of "A or B" and another of "(A or B) implies C", how can we combine these into a simpler proof of just "C"? A proof of "(A or B) implies C" must contain both a proof a "A implies C" and a proof of "B implies C", and we could insert into one those proofs a proof of A or a proof of B. But we have to know which one we have! (This is a very short gloss of a much deeper story, where, under Curry-Howard, proof simplification corresponds to computation, and this is another way of describing a function call that does a case-analysis of a tagged union (or "sum type").) Now "union and intersection" types with the set-theoretic properties you are hinting at have indeed been studied (see, for example, Section 15.7 of Pierce's "Types and Programming Languages"). But they do not replace the much more familiar "sum and product types", and do not play the central role of "or" and "and" in the correspondence of programming to logic.