In computer science, a tagged union, also called a variant, variant record, choice type, discriminated union, disjoint union, sum type, or coproduct, is a data structure used to hold a value that could take on several different, but fixed, types. Only one of the types can be in use at any one time, and a tag field explicitly indicates which type is in use. It can be thought of as a type that has several "cases", each of which should be handled correctly when that type is manipulated. This is critical in defining recursive datatypes, in which some component of a value may have the same type as that value, for example in defining a type for representing trees, where it is necessary to distinguish multi-node subtrees and leaves. Like ordinary unions, tagged unions can save storage by overlapping storage areas for each type, since only one is in use at a time.
Description Tagged unions are most important in functional programming languages such as ML and Haskell, where they are called datatypes (see algebraic data type) and the compiler can verify that all cases of a tagged union are always handled, avoiding many types of errors. Compile-time checked sum types are also extensively used in Rust, where they are called enum. They can, however, be constructed in nearly any programming language, and are much safer than untagged unions, often simply called unions, which are similar but do not explicitly track which member of a union is currently in use. Tagged unions are often accompanied by the concept of a constructor, which is similar but not the same as a constructor for a class. A constructor is a function or an expression that produces a value of the tagged union type, given a tag and a value of the corresponding type. Mathematically, tagged unions correspond to disjoint or discriminated unions, usually written using +. Given an element of a disjoint union A + B {\displaystyle A+B} , it is possible to determine whether it came from A {\displaystyle A} or B {\displaystyle B} . If an element lies in both, there will be two effectively distinct copies of the value in A + B {\displaystyle A+B} , one from A {\displaystyle A} and one from B {\displaystyle B} . In type theory, a tagged union is called a sum type. Sum types are the dual of product types. Notations vary, but usually the sum type A + B {\displaystyle A+B} comes with two introduction forms (injections) inj 1 : A ↦ A + B {\displaystyle {\texttt {inj}}_{1}:A\mapsto A+B} and inj 2 : B ↦ A + B {\displaystyle {\texttt {inj}}_{2}:B\mapsto A+B} . The elimination form is case analysis, known as pattern matching in ML-style languages: if e {\displaystyle e} has type A + B {\displaystyle A+B} and e 1 {\displaystyle e_{1}} and e 2 {\displaystyle e_{2}} have type τ {\displaystyle \tau } under the assumptions x : A {\displaystyle x:A} and y : B {\displaystyle y:B} respectively, then the term c a s e e o f x ⇒ e 1 ∣ y ⇒ e 2 {\displaystyle {\mathsf {case}}\ e\ {\mathsf {of}}\ x\Rightarrow e_{1}\mid y\Rightarrow e_{2}} has type τ {\displaystyle \tau } . The sum type corresponds to intuitionistic logical disjunction under the Curry–Howard correspondence. An enumerated type can be seen as a degenerate case: a tagged union of unit types. It corresponds to a set of nullary constructors and may be implemented as a simple tag variable, since it holds no additional data besides the value of the tag. Many programming techniques and data structures, including rope, lazy evaluation, class hierarchy (see below), arbitrary-precision arithmetic, CDR coding, the indirection bit, and other kinds of tagged pointers, are usually implemented using some sort of tagged union. A tagged union can be seen as the simplest kind of self-describing data format. The tag of the tagged union can be seen as the simplest kind of metadata. In languages with flow-sensitive typing, tagged unions can be implemented by a combination of union types and record types.
… excerpt ends here. Continue reading the full article.
