14.14. Sum Types🔗

Sum types represent a choice between two types: an element of the sum is an element of one of the other types, paired with an indication of which type it came from. Sums are also known as disjoint unions, discriminated unions, or tagged unions. The constructors of a sum are also called injections; mathematically, they can be considered as injective functions from each summand to the sum.

There are two varieties of the sum type:

Sum is polymorphic over all Type universes, and is never a proposition.
PSum is allows the summands to be propositions or types. Unlike Or, the PSum of two propositions is still a type, and non-propositional code can check which injection was used to construct a given value.

Manually-written Lean code almost always uses only Sum, while PSum is used as part of the implementation of proof automation. This is because it imposes problematic constraints that universe level unification cannot solve.

inductive type

Sum.{u, v} (α : Type u) (β : Type v) :
  Type (max u v)

Sum α β, or α ⊕ β, is the disjoint union of types α and β. An element of α ⊕ β is either of the form .inl a where a : α, or .inr b where b : β.

Constructors

inl.{u, v} {α : Type u} {β : Type v} (val : α) : α ⊕ β

Left injection into the sum type α ⊕ β. If a : α then .inl a : α ⊕ β.

inr.{u, v} {α : Type u} {β : Type v} (val : β) : α ⊕ β

Right injection into the sum type α ⊕ β. If b : β then .inr b : α ⊕ β.

inductive type

PSum.{u, v} (α : Sort u) (β : Sort v) :
  Sort (max (max 1 u) v)

PSum α β, or α ⊕' β, is the disjoint union of types α and β. It differs from α ⊕ β in that it allows α and β to have arbitrary sorts Sort u and Sort v, instead of restricting to Type u and Type v. This means that it can be used in situations where one side is a proposition, like True ⊕' Nat.

The reason this is not the default is that this type lives in the universe Sort (max 1 u v), which can cause problems for universe level unification, because the equation max 1 u v = ?u + 1 has no solution in level arithmetic. PSum is usually only used in automation that constructs sums of arbitrary types.

Constructors

inl.{u, v} {α : Sort u} {β : Sort v} (val : α) : α ⊕' β

Left injection into the sum type α ⊕' β. If a : α then .inl a : α ⊕' β.

inr.{u, v} {α : Sort u} {β : Sort v} (val : β) : α ⊕' β

Right injection into the sum type α ⊕' β. If b : β then .inr b : α ⊕' β.

14.14.1. Syntax🔗

The names Sum and PSum are rarely written explicitly. Most code uses the corresponding infix operators.

syntaxSum Types

term ::= ...
    | `Sum α β`, or `α ⊕ β`, is the disjoint union of types `α` and `β`.
An element of `α ⊕ β` is either of the form `.inl a` where `a : α`,
or `.inr b` where `b : β`.
term ⊕ term

α ⊕ β is notation for Sum α β.

syntaxPotentially-Propositional Sum Types

term ::= ...
    | `PSum α β`, or `α ⊕' β`, is the disjoint union of types `α` and `β`.
It differs from `α ⊕ β` in that it allows `α` and `β` to have arbitrary sorts
`Sort u` and `Sort v`, instead of restricting to `Type u` and `Type v`. This means
that it can be used in situations where one side is a proposition, like `True ⊕' Nat`.

The reason this is not the default is that this type lives in the universe `Sort (max 1 u v)`,
which can cause problems for universe level unification,
because the equation `max 1 u v = ?u + 1` has no solution in level arithmetic.
`PSum` is usually only used in automation that constructs sums of arbitrary types.
term ⊕' term

α ⊕' β is notation for PSum α β.

14.14.2. API Reference🔗

Sum types are primarily used with pattern matching rather than explicit function calls from an API. As such, their primary API is the constructors inl and inr.

14.14.2.1. Case Distinction

def

Sum.isLeft.{u_1, u_2} {α : Type u_1}
  {β : Type u_2} : α ⊕ β → Bool

Check if a sum is inl.

def

Sum.isRight.{u_1, u_2} {α : Type u_1}
  {β : Type u_2} : α ⊕ β → Bool

Check if a sum is inr.

14.14.2.2. Extracting Values

def

Sum.elim.{u_1, u_2, u_3} {α : Type u_1}
  {β : Type u_2} {γ : Sort u_3} (f : α → γ)
  (g : β → γ) : α ⊕ β → γ

Define a function on α ⊕ β by giving separate definitions on α and β.

def

Sum.getLeft.{u_1, u_2} {α : Type u_1}
  {β : Type u_2} (ab : α ⊕ β) :
  ab.isLeft = true → α

Retrieve the contents from a sum known to be inl.

def

Sum.getLeft?.{u_1, u_2} {α : Type u_1}
  {β : Type u_2} : α ⊕ β → Option α

Check if a sum is inl and if so, retrieve its contents.

def

Sum.getRight.{u_1, u_2} {α : Type u_1}
  {β : Type u_2} (ab : α ⊕ β) :
  ab.isRight = true → β

Retrieve the contents from a sum known to be inr.

def

Sum.getRight?.{u_1, u_2} {α : Type u_1}
  {β : Type u_2} : α ⊕ β → Option β

Check if a sum is inr and if so, retrieve its contents.

14.14.2.3. Transformations

def

Sum.map.{u_1, u_2, u_3, u_4} {α : Type u_1}
  {α' : Type u_2} {β : Type u_3} {β' : Type u_4}
  (f : α → α') (g : β → β') : α ⊕ β → α' ⊕ β'

Map α ⊕ β to α' ⊕ β' sending α to α' and β to β'.

def

Sum.swap.{u_1, u_2} {α : Type u_1}
  {β : Type u_2} : α ⊕ β → β ⊕ α

Swap the factors of a sum type

14.14.2.4. Inhabited

The Inhabited definitions for Sum and PSum are not registered as instances. This is because there are two separate ways to construct a default value (via inl or inr), and instance synthesis might result in either choice. The result could be situations where two identically-written terms elaborate differently and are not definitionally equal.

Both types have Nonempty instances, for which proof irrelevance makes the choice of inl or inr not matter. This is enough to enable partial functions. For situations that require an Inhabited instance, such as programs that use panic!, the instance can be explicitly used by adding it to the local context with Lean.Parser.Term.have : termhave or Lean.Parser.Term.let : term`let` is used to declare a local definition. Example: ``` let x := 1 let y := x + 1 x + y ``` Since functions are first class citizens in Lean, you can use `let` to declare local functions too. ``` let double := fun x => 2*x double (double 3) ``` For recursive definitions, you should use `let rec`. You can also perform pattern matching using `let`. For example, assume `p` has type `Nat × Nat`, then you can write ``` let (x, y) := p x + y ```let.

Inhabited Sum Types

In Lean's logic, Lean.Parser.Term.panic : term`panic! msg` formally evaluates to `@Inhabited.default α` if the expected type `α` implements `Inhabited`. At runtime, `msg` and the file position are printed to stderr unless the C function `lean_set_panic_messages(false)` has been executed before. If the C function `lean_set_exit_on_panic(true)` has been executed before, the process is then aborted.panic! is equivalent to the default value specified in its type's Inhabited instance. This means that the type must have such an instance—a Nonempty instance combined with the axiom of choice would render the program non-computable.

Products have the right instance:

example : Nat × String := panic! "Cant' find it"

Sums do not, by default:

example : Nat ⊕ String := failed to synthesize
  Inhabited (Nat ⊕ String)
Additional diagnostic information may be available using the `set_option diagnostics true` command.panic! "Cant' find it"

failed to synthesize
  Inhabited (Nat ⊕ String)
Additional diagnostic information may be available using the `set_option diagnostics true` command.

The desired instance can be made available to instance synthesis using Lean.Parser.Term.have : termhave:

example : Nat ⊕ String :=
  have : Inhabited (Nat ⊕ String) := Sum.inhabitedLeft
  panic! "Cant' find it"

def

Sum.inhabitedLeft.{u, v} {α : Type u}
  {β : Type v} [Inhabited α] : Inhabited (α ⊕ β)

This is not an instance to avoid non-canonical instances.

def

Sum.inhabitedRight.{u, v} {α : Type u}
  {β : Type v} [Inhabited β] : Inhabited (α ⊕ β)

This is not an instance to avoid non-canonical instances.

def

PSum.inhabitedLeft.{u_1, u_2} {α : Sort u_1}
  {β : Sort u_2} [Inhabited α] :
  Inhabited (α ⊕' β)

PSum α β is inhabited if α is inhabited. This is not an instance to avoid non-canonical instances.

def

PSum.inhabitedRight.{u_1, u_2} {α : Sort u_1}
  {β : Sort u_2} [Inhabited β] :
  Inhabited (α ⊕' β)

PSum α β is inhabited if β is inhabited. This is not an instance to avoid non-canonical instances.