Sum Type

Definition

A sum type (or coproduct) is a Type Constructor that represents a choice between two or more types. Given types $A$ and $B$, their sum $A+B$ consists of values that come from either $A$ or $B$, tagged to indicate their origin.

More generally, the sum of types $A_1,A_2,\dots ,A_n$ is written $A_1+A_2+\cdots +A_n$ and contains values from any of these types, each tagged with its index.

Type Rules

Sum types are characterized by their introduction and elimination rules:

Introduction Rules

$\frac{a:A}{\text{inl}(a):A+B}\frac{b:B}{\text{inr}(b):A+B}$

We can inject a value from $A$ into the sum using $\text{inl}$ (inject left) or a value from $B$ using $\text{inr}$ (inject right).

Elimination Rule

$\frac{s:A+Bf:A\to Cg:B\to C}{\text{case}(s,f,g):C}$

To use a sum type, we must handle both cases: provide functions for both possible types and perform case analysis.

Computation Rules (β-rules)

$\text{case}(\text{inl}(a),f,g)=f(a)\text{case}(\text{inr}(b),f,g)=g(b)$

Eta Rule (η-rule)

For any $s:A+B$:

$s=\text{case}(s,\lambda x.\text{inl}(x),\lambda y.\text{inr}(y))$

Category-Theoretic View

In category theory, the sum type corresponds to the categorical coproduct. The type $A+B$ is the coproduct of $A$ and $B$ with injection morphisms $\text{inl}:A\to A+B$ and $\text{inr}:B\to A+B$.

The coproduct satisfies a universal property: for any type $C$ with morphisms $f:A\to C$ and $g:B\to C$, there exists a unique morphism $[f,g]:A+B\to C$ such that $[f,g]\circ \text{inl}=f$ and $[f,g]\circ \text{inr}=g$.

Examples

Common sum types in programming languages:

• $\text{Bool}\cong 1+1$: Boolean as sum of two unit types
• $\text{Maybe}(A)\cong 1+A$: Optional values
• $\text{Either}(A,B)\cong A+B$: Explicit sum type in functional languages
• $\text{Result}(A,E)\cong A+E$: Success or error values

Duality with Product Types

Sum types are dual to product types:

• Product types use conjunction ($A$ and $B$), sum types use disjunction ($A$ or $B$)
• Product introduction requires both components, sum introduction requires one component
• Product elimination extracts one component, sum elimination must handle both cases
• In logic: product corresponds to conjunction ($\wedge$), sum corresponds to disjunction ($\vee$)

Related Concepts

• Dependent Sum: A generalization where types may depend on values
• Type Constructor: Sum types as a fundamental type constructor
• Introduction Rule: The injection operations for sum types
• Elimination Rule: Case analysis on sum types
• Function Type: Related by exponential laws
• Existential: A propositionally truncated sum type.