Comment by troad
18 hours ago
Underlyingly, all unions are the same concept, exposed by C's `union` keyword, namely overlapping memory (as opposed to `struct`s, which are sequential memory). You can add a discriminator tag to your unions, your call. If it is impossible for there to be ambiguity (e.g. you track the state somewhere else, and you're dealing with a large array), it may be redundant / memory inefficient to tag every item.
Having these tags be a language construct is just a DX feature on top of unions. A very handy one, but it doesn't make tagged and untagged unions spring from different theoretical universes. I enjoy the ADT / set-theoretic debate as much as the next PL nerd, but theory ought to conform to reality, not vice versa.
That's like saying Haskell is really an imperative language just because it's written in C. But it doesn't matter how it is implemented, it matters how it behaves on the surface.
> That's like saying Haskell is really an imperative language just because it's written in C
I honestly don't even remotely understand how you got to that from what I wrote.
Unions already have a definition. You cannot go around claiming that technically unions are not unions (and that "most people don't know" this), because theory X or Y overloads the term union to refer to some unrelated concept. That's fine and well and good, within that theory, but it does not displace the usual CS definition of union. It is a load-bearing definition.
A tagged union is so called because it is a union (overlapping memory) with a field (a tag) containing a discriminator (aka discriminated union). An untagged union is a union without this tag. These terms didn't come out of nowhere. They are transparent descriptors of what's happening.
It doesn't matter whether Haskell is implemented in C or Ruby, and it doesn't matter whether it's functional, object-oriented, or a DSL for modding Elden Ring, none of this changes what a union is. I'm very supportive of type theories exploring the option space for type constructs, but someone's going to have to implement these somehow. Such as with (tagged) unions. You know, that CS concept we have, with a settled and well understood meaning.
To be fair to you, I think you're letting a very narrow definition of 'union' shadow a much more usual and common definition of the word. And that's totally fine if that's the definition pertinent to you and your work, but if that's the case, maybe don't go around pontificating about how most people do not understand unions?
> You cannot go around claiming that 'technically' unions are not unions
I never said this. I said that there are two different kinds of unions with quite different definitions and behaviors.
> A tagged union is so called because it is a union (overlapping memory) with a field (a tag) containing a discriminator (aka discriminated union). An untagged union is a union without this tag.
That alone doesn't sufficiently describe the "unions" in set theoretic type systems like TypeScript. As I said, these unions are not disjoint and don't involve the special constructor that tagged unions/discriminated unions/sum types in algebraic type systems do. They also have logical implications like A implying A|B. Or A|A being equivalent to A, which isn't the case for discriminated/tagged unions. Maybe they are implemented similarly under the hood, but that doesn't negate the difference.
Edit: It's probably fair to say that "untagged unions" in languages like TypeScript, Ceylon or Scala 3 (set theoretic type systems) are different from "untagged unions" in C. It only adds to the confusion...
8 replies →