There seem to be at least a couple different possible ways of modeling sum types in a type system, but I haven't been able to find consistent terms for referring to them:

  1. A sum type is formed from a set of "data constructors", which are function-like entities that notionally map values of a summand type to values of the sum type. This is the model adopted by e.g. Haskell and the various flavors of ML.

  2. A sum type is formed directly from the underlying summand types, with no data constructors, and as a consequence the sum type is a supertype of the summands (or at least behaves very much like one). This model seems to be much less common, but it's the model adopted by Ceylon, and by C++'s std::variant.

Note that this is separate from the distinction between discriminated and non-discriminated unions: both models permit the sum type to be discriminated (although only if the summands are disjoint, in the case of #2).

Are there settled terms for distinguishing these two models?

  • $\begingroup$ The first one is a sum type. The second one is a union type. Note that Ceylon and C++ implement union types in strange ways, with restrictions on what can be done etc. $\endgroup$ Jul 29 '20 at 11:26
  1. The first concept you mention is that of an algebraic data type (or ADT). These are (recursive) sum-of-product types, though in many languages the product types are not first-class in that you may not refer to them directly, but only as part of the sum.
  2. The second concept is a true sum type. However, in both the examples mentioned, the sum type has a restriction that the summands must be unique, e.g. you cannot describe the type $A + A$, because summands are referenced nominally, rather than by their index.

Note that ADTs suffice to describe sum types (even with non-unique summands), by wrapping their summands in new constructors. However, they are more general, as they can describe fixed point types, like binary trees.

  • $\begingroup$ Well, it's not a sum type if there is a restriction about disjointness. At best it is a disjoint union, and also I don't see anywhere in the documentation that Ceylon X|Y and C++ std::variant have any tags (although Ceylon probably has enough type information stored at runtime that essentially functions as tags). $\endgroup$ Jul 29 '20 at 11:25
  • $\begingroup$ It is a sum type; they just don't represent all sum types. Though perhaps you're making a distinction between disjoint unions and sums that I'm not? In Ceylon, you can use is to deduce the discriminant, while in C++, you can use holds_alternative. $\endgroup$
    – varkor
    Jul 29 '20 at 12:03
  • $\begingroup$ I think we're mostly discussing terminology. I would call someting "sum types" if it resembles coproducts, and "union types" if it's one of those less reasonable constructions. All of these can only be approximated in languages such as C++, as the language is full of historical accidents and design decisions that were not originally motivated by having theoretically reasonable design. $\endgroup$ Jul 29 '20 at 14:46
  • $\begingroup$ Unless I can make the type "$A + A$" which is in general different from $A$, it's not really a sum type. $\endgroup$ Jul 29 '20 at 14:47

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.