12.12. Optional Values🔗

inductive type

Option.{u} (α : Type u) : Type u

Option α is the type of values which are either some a for some a : α, or none. In functional programming languages, this type is used to represent the possibility of failure, or sometimes nullability.

For example, the function HashMap.get? : HashMap α β → α → Option β looks up a specified key a : α inside the map. Because we do not know in advance whether the key is actually in the map, the return type is Option β, where none means the value was not in the map, and some b means that the value was found and b is the value retrieved.

The xs[i] syntax, which is used to index into collections, has a variant xs[i]? that returns an optional value depending on whether the given index is valid. For example, if m : HashMap α β and a : α, then m[a]? is equivalent to HashMap.get? m a.

To extract a value from an Option α, we use pattern matching:

def map (f : α → β) (x : Option α) : Option β :=
  match x with
  | some a => some (f a)
  | none => none

We can also use if let to pattern match on Option and get the value in the branch:

def map (f : α → β) (x : Option α) : Option β :=
  if let some a := x then
    some (f a)
  else
    none

Constructors

none.{u} {α : Type u} : Option α

No value.

some.{u} {α : Type u} (val : α) : Option α

Some value of type α.

12.12.1. Coercions

There is a coercion from α to Option α that wraps a value in some. This allows Option to be used in a style similar to nullable types in other languages, where values that are missing are indicated by none and values that are present are not specially marked.

Coercions and Option

In getAlpha, a line of input is read. If the line consists only of letters (after removing whitespace from the beginning and end of it), then it is returned; otherwise, the function returns none.

def getAlpha : IO (Option String) := do
  let line := (← (← IO.getStdin).getLine).trim
  if line.length > 0 && line.all Char.isAlpha then
    return line
  else
    return none

In the successful case, there is no explicit some wrapped around line. The some is automatically inserted by the coercion.

12.12.2. API Reference

12.12.2.1. Extracting Values

def

Option.get.{u} {α : Type u} (o : Option α)
    : o.isSome = true → α

Extracts the value a from an option that is known to be some a for some a.

def

Option.get!.{u} {α : Type u} [Inhabited α]
    : Option α → α

def

Option.getD.{u_1} {α : Type u_1}
    (opt : Option α) (dflt : α) : α

Get with default. If opt : Option α and dflt : α, then opt.getD dflt returns a if opt = some a and dflt otherwise.

This function is @[macro_inline], so dflt will not be evaluated unless opt turns out to be none.

def

Option.getDM.{u_1, u_2}
    {m : Type u_1 → Type u_2} {α : Type u_1}
    [Monad m] (x : Option α) (y : m α) : m α

A monadic analogue of Option.getD.

def

Option.getM.{u_1, u_2} {m : Type u_1 → Type u_2}
    {α : Type u_1} [Alternative m]
    : Option α → m α

Lifts an optional value to any Alternative, sending none to failure.

def

Option.elim.{u_1, u_2} {α : Type u_1}
    {β : Sort u_2} : Option α → β → (α → β) → β

An elimination principle for Option. It is a nondependent version of Option.recOn.

def

Option.elimM.{u_1, u_2}
    {m : Type u_1 → Type u_2} {α β : Type u_1}
    [Monad m] (x : m (Option α)) (y : m β)
    (z : α → m β) : m β

A monadic analogue of Option.elim.

def

Option.liftOrGet.{u_1} {α : Type u_1}
    (f : α → α → α)
    : Option α → Option α → Option α

Two arguments failsafe function. Returns f a b if the inputs are some a and some b, and "does nothing" otherwise.

def

Option.merge.{u_1} {α : Type u_1}
    (fn : α → α → α)
    : Option α → Option α → Option α

Take a pair of options and if they are both some, apply the given fn to produce an output. Otherwise act like orElse.

12.12.2.2. Properties and Comparisons

def

Option.isNone.{u_1} {α : Type u_1}
    : Option α → Bool

Returns true on none and false on some x.

def

Option.isSome.{u_1} {α : Type u_1}
    : Option α → Bool

Returns true on some x and false on none.

def

Option.isEqSome.{u_1} {α : Type u_1} [BEq α]
    : Option α → α → Bool

x?.isEqSome y is equivalent to x? == some y, but avoids an allocation.

def

Option.min.{u_1} {α : Type u_1} [Min α]
    : Option α → Option α → Option α

The minimum of two optional values.

def

Option.max.{u_1} {α : Type u_1} [Max α]
    : Option α → Option α → Option α

The maximum of two optional values.

def

Option.lt.{u_1, u_2} {α : Type u_1}
    {β : Type u_2} (r : α → β → Prop)
    : Option α → Option β → Prop

def

Option.decidable_eq_none.{u_1} {α : Type u_1}
    {o : Option α} : Decidable (o = none)

o = none is decidable even if the wrapped type does not have decidable equality. This is not an instance because it is not definitionally equal to instance : DecidableEq Option. Try to use o.isNone or o.isSome instead.

12.12.2.3. Conversion

def

Option.toArray.{u_1} {α : Type u_1}
    : Option α → Array α

Cast of Option to Array. Returns #[a] if the input is some a, and #[] if it is none.

def

Option.toList.{u_1} {α : Type u_1}
    : Option α → List α

Cast of Option to List. Returns [a] if the input is some a, and [] if it is none.

def

Option.repr.{u_1} {α : Type u_1} [Repr α]
    : Option α → Nat → Std.Format

def

Option.format.{u} {α : Type u} [Std.ToFormat α]
    : Option α → Std.Format

12.12.2.4. Control

Option can be thought of as describing a computation that may fail to return a value. The Monad Option instance, along with Alternative Option, is based on this understanding. Returning none can also be thought of as throwing an exception that contains no interesting information, which is captured in the MonadExcept Unit Option instance.

def

Option.guard.{u_1} {α : Type u_1} (p : α → Prop)
    [DecidablePred p] (a : α) : Option α

guard p a returns some a if p a holds, otherwise none.

def

Option.bind.{u_1, u_2} {α : Type u_1}
    {β : Type u_2}
    : Option α → (α → Option β) → Option β

def

Option.bindM.{u_1, u_2, u_3}
    {m : Type u_1 → Type u_2} {α : Type u_3}
    {β : Type u_1} [Monad m]
    (f : α → m (Option β)) (o : Option α)
    : m (Option β)

Runs f on o's value, if any, and returns its result, or else returns none.

def

Option.join.{u_1} {α : Type u_1}
    (x : Option (Option α)) : Option α

Flatten an Option of Option, a specialization of joinM.

def

Option.sequence.{u, u_1} {m : Type u → Type u_1}
    [Monad m] {α : Type u}
    : Option (m α) → m (Option α)

If you maybe have a monadic computation in a [Monad m] which produces a term of type α, then there is a naturally associated way to always perform a computation in m which maybe produces a result.

def

Option.tryCatch.{u_1} {α : Type u_1}
    (x : Option α) (handle : Unit → Option α)
    : Option α

def

Option.or.{u_1} {α : Type u_1}
    : Option α → Option α → Option α

If the first argument is some a, returns some a, otherwise returns the second argument. This is similar to <|>/orElse, but it is strict in the second argument.

def

Option.orElse.{u_1} {α : Type u_1}
    : Option α → (Unit → Option α) → Option α

Implementation of OrElse's <|> syntax for Option. If the first argument is some a, returns some a, otherwise evaluates and returns the second argument. See also or for a version that is strict in the second argument.

12.12.2.5. Iteration

Option can be thought of as a collection that contains at most one value. From this perspective, iteration operators can be understood as performing some operation on the contained value, if present, or doing nothing if not.

def

Option.all.{u_1} {α : Type u_1} (p : α → Bool)
    : Option α → Bool

Checks that an optional value satisfies a predicate p or is none.

def

Option.any.{u_1} {α : Type u_1} (p : α → Bool)
    : Option α → Bool

Checks that an optional value is not none and the value satisfies a predicate p.

def

Option.filter.{u_1} {α : Type u_1}
    (p : α → Bool) : Option α → Option α

Keeps an optional value only if it satisfies the predicate p.

def

Option.forM.{u_1, u_2, u_3}
    {m : Type u_1 → Type u_2} {α : Type u_3}
    [Pure m]
    : Option α → (α → m PUnit) → m PUnit

Map a monadic function which returns Unit over an Option.

def

Option.map.{u_1, u_2} {α : Type u_1}
    {β : Type u_2} (f : α → β)
    : Option α → Option β

Map a function over an Option by applying the function to the contained value if present.

def

Option.mapA.{u_1, u_2, u_3}
    {m : Type u_1 → Type u_2} [Applicative m]
    {α : Type u_3} {β : Type u_1} (f : α → m β)
    : Option α → m (Option β)

Like Option.mapM but for applicative functors.

def

Option.mapM.{u_1, u_2, u_3}
    {m : Type u_1 → Type u_2} {α : Type u_3}
    {β : Type u_1} [Monad m] (f : α → m β)
    (o : Option α) : m (Option β)

Runs a monadic function f on an optional value. If the optional value is none the function is not called.

12.12.2.6. Recursion Helpers

def

Option.attach.{u_1} {α : Type u_1}
    (xs : Option α) : Option { x // x ∈ xs }

"Attach" the proof that the element of xs, if present, is in xs to produce a new option with the same elements but in the type {x // x ∈ xs}.

def

Option.attachWith.{u_1} {α : Type u_1}
    (xs : Option α) (P : α → Prop)
    (H : ∀ (x : α), x ∈ xs → P x)
    : Option { x // P x }

"Attach" a proof P x that holds for the element of o, if present, to produce a new option with the same element but in the type {x // P x}.

def

Option.unattach.{u_1} {α : Type u_1}
    {p : α → Prop} (o : Option { x // p x })
    : Option α

A synonym for l.map (·.val). Mostly this should not be needed by users. It is introduced as an intermediate step by lemmas such as map_subtype, and is ideally subsequently simplified away by unattach_attach.

If not, usually the right approach is simp [Option.unattach, -Option.map_subtype] to unfold.

12.12.2.7. Reasoning

def

Option.choice.{u_1} (α : Type u_1) : Option α

An arbitrary some a with a : α if α is nonempty, and otherwise none.

def

Option.pbind.{u_1, u_2} {α : Type u_1}
    {β : Type u_2} (x : Option α)
    : ((a : α) → a ∈ x → Option β) → Option β

Partial bind. If for some x : Option α, f : Π (a : α), a ∈ x → Option β is a partial function defined on a : α giving an Option β, where some a = x, then pbind x f h is essentially the same as bind x f but is defined only when all x = some a, using the proof to apply f.

def

Option.pelim.{u_1, u_2} {α : Type u_1}
    {β : Sort u_2} (o : Option α) (b : β)
    (f : (a : α) → a ∈ o → β) : β

Partial elimination. If o : Option α and f : (a : α) → a ∈ o → β, then o.pelim b f is the same as o.elim b f but f is passed the proof that a ∈ o.

def

Option.pmap.{u_1, u_2} {α : Type u_1}
    {β : Type u_2} {p : α → Prop}
    (f : (a : α) → p a → β) (x : Option α)
    : (∀ (a : α), a ∈ x → p a) → Option β

Partial map. If f : Π a, p a → β is a partial function defined on a : α satisfying p, then pmap f x h is essentially the same as map f x but is defined only when all members of x satisfy p, using the proof to apply f.