20.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. In particular, this type is 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.

inductive type

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

The disjoint union of types α and β, ordinarily written α ⊕ β.

An element of α ⊕ β is either an a : α wrapped in Sum.inl or a b : β wrapped in Sum.inr. α ⊕ β is not equivalent to the set-theoretic union of α and β because its values include an indication of which of the two types was chosen. The union of a singleton set with itself contains one element, while Unit ⊕ Unit contains distinct values inl () and inr ().

Constructors

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

Left injection into the sum type α ⊕ β.

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

Right injection into the sum type α ⊕ β.

inductive type

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

The disjoint union of arbitrary sorts α β, or α ⊕' β.

It differs from α ⊕ β in that it allows α and β to have arbitrary sorts Sort u and Sort v, instead of restricting them to Type u and Type v. This means that it can be used in situations where one side is a proposition, like True ⊕' Nat. However, the resulting universe level constraints are often more difficult to solve than those that result from Sum.

Constructors

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

Left injection into the sum type α ⊕' β.

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

Right injection into the sum type α ⊕' β.

20.14.1. Syntax🔗

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

syntaxSum Types

term ::= ...
    | The disjoint union of types `α` and `β`, ordinarily written `α ⊕ β`.

An element of `α ⊕ β` is either an `a : α` wrapped in `Sum.inl` or a `b : β` wrapped in `Sum.inr`.
`α ⊕ β` is not equivalent to the set-theoretic union of `α` and `β` because its values include an
indication of which of the two types was chosen. The union of a singleton set with itself contains
one element, while `Unit ⊕ Unit` contains distinct values `inl ()` and `inr ()`.
term ⊕ term

α ⊕ β is notation for Sum α β.

syntaxPotentially-Propositional Sum Types

term ::= ...
    | The disjoint union of arbitrary sorts `α` `β`, or `α ⊕' β`.

It differs from `α ⊕ β` in that it allows `α` and `β` to have arbitrary sorts `Sort u` and `Sort v`,
instead of restricting them to `Type u` and `Type v`. This means that it can be used in situations
where one side is a proposition, like `True ⊕' Nat`. However, the resulting universe level
constraints are often more difficult to solve than those that result from `Sum`.
term ⊕' term

α ⊕' β is notation for PSum α β.

20.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.

20.14.2.1. Case Distinction

def

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

Checks whether a sum is the left injection inl.

def

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

Checks whether a sum is the right injection inr.

20.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 : β → γ) : α ⊕ β → γ
Sum.elim.{u_1, u_2, u_3} {α : Type u_1}
  {β : Type u_2} {γ : Sort u_3}
  (f : α → γ) (g : β → γ) : α ⊕ β → γ

Case analysis for sums that applies the appropriate function f or g after checking which constructor is present.

def

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

Retrieves the contents from a sum known to be inl.

def

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

Checks whether a sum is the left injection inl and, if so, retrieves its contents.

def

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

Retrieves the contents from a sum known to be inr.

def

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

Checks whether a sum is the right injection inr and, if so, retrieves its contents.

20.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 : β → β') :
  α ⊕ β → α' ⊕ β'
Sum.map.{u_1, u_2, u_3, u_4}
  {α : Type u_1} {α' : Type u_2}
  {β : Type u_3} {β' : Type u_4}
  (f : α → α') (g : β → β') :
  α ⊕ β → α' ⊕ β'

Transforms a sum according to functions on each type.

This function maps α ⊕ β to α' ⊕ β', sending α to α' and β to β'.

def

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

Swaps the factors of a sum type.

The constructor Sum.inl is replaced with Sum.inr, and vice versa.

20.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 : term`have` is used to declare local hypotheses and opaque local definitions. It has the same syntax as `let`, and it is equivalent to `let +nondep`, creating a *nondependent* let expression.have 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 ``` The *anaphoric let* `let := v` defines a variable called `this`.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 instance of type class
  Inhabited (Nat ⊕ String)

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.panic! "Cant' find it"

failed to synthesize instance of type class
  Inhabited (Nat ⊕ String)

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.

The desired instance can be made available to instance synthesis using Lean.Parser.Term.have : term`have` is used to declare local hypotheses and opaque local definitions. It has the same syntax as `let`, and it is equivalent to `let +nondep`, creating a *nondependent* let expression.have:

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

Live ↪

def

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

If the left type in a sum is inhabited then the sum is inhabited.

This is not an instance to avoid non-canonical instances when both the left and right types are inhabited.

def

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

If the right type in a sum is inhabited then the sum is inhabited.

This is not an instance to avoid non-canonical instances when both the left and right types are inhabited.

def

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

If the left type in a sum is inhabited then the sum is inhabited.

This is not an instance to avoid non-canonical instances when both the left and right types are inhabited.

def

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

If the right type in a sum is inhabited then the sum is inhabited.

This is not an instance to avoid non-canonical instances when both the left and right types are inhabited.