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.