# Terms for different models of sum types

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?

• 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. – Andrej Bauer Jul 29 at 11:26

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.
• 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). – Andrej Bauer Jul 29 at 11:25
• 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. – varkor Jul 29 at 12:03
• Unless I can make the type "$A + A$" which is in general different from $A$, it's not really a sum type. – Andrej Bauer Jul 29 at 14:47