Sum Types
Many data structures involve different types of data, e.g. in a tree, nodes have children but leaves do not. The type of the value determines the structure of the data. These types are called sum types and include the binary sum (choice of two things) and the nullary sum (the choice of no things). Finite sums generalise these cases to an arbitrary number in a finite set and have both an eager and lazy interpretation.
Nullary and Binary Sum
| Element | Abstract Syntax | Conrete Syntax | Description |
|---|---|---|---|
Typ t ::= |
void |
void |
nullary sum |
sum(t1;t2) |
t1+t2 |
binary sum |
|
Exp e ::= |
abort[t](e) |
abort(e) |
abort |
in[t1;t2][l](e) |
l.e |
left injection |
|
in[t1;t2][r](e) |
r.e |
right injection |
|
case(e; x1.e1; x2.e2) |
case e {l.x ⇒ e1 or r.x ⇒ e2} |
case analysis |
The nullary sum has a choice of zero and therefore has no values. The value abort(e) aborts the computation in the event that e evaluates to a value, which it cannot do. A value can be drawn from the left or the right and we can discriminate on the two choices using case analysis.
Application
-
Unit - The type with just one element <>
-
Void - The type with no elements, if e: void then e must not give a value
-
Booleans - Two state values
-
Enumerations - Case analysis over a finite set
-
Options - The type containing no value or one value. Nulls are commonly used to represent the Option type in object oriented languages. Tony Hoare has talked about this being his billion dollar mistake.
Object oriented languages also often lack case analysis over finite sums, leaving the programmer to simulate this behaviour through the use of inheritance hierarchies. However, this can force subclass specific methods to bubble up to the top of the inheritance tree, violating type safety.
