Option α is the type of values which are either some v for some v:α, or none.
In functional programming, this type is used similarly to nullable types: none represents the absence of a value.
Additionally, partial functions from α to β can be represented by the type α → Option β, where none results when the function is undefined for some input.
Computationally, these partial functions represent the possibility of failure or errors, and they correspond to a program that can terminate early but not throw an informative exception.
Option can also be thought of as being similar to a list that contains at most one element.
From this perspective, iterating over Option consists of carrying out an operation only when a value is present.
The Option API makes frequent use of this perspective.
The function Std.HashMap.get? looks up a specified key a : α inside a HashMap α β:
Std.HashMap.get?.{u, v} {α : Type u} {β : Type v}
[BEq α] [Hashable α]
(m : HashMap α β) (a : α) :
Option β
Because there is no way to know in advance whether the key is actually in the map, the return type is Option β, where none means the key was not in the map, and some b means that the key was found and b is the value retrieved.
The xs[i] syntax, which is used to index into collections when there is an available proof that i is a valid index into xs, has a variant xs[i]? that returns an optional value depending on whether the given index is valid.
If m:HashMap α β and a:α, then m[a]? is equivalent to HashMap.get? m a.
In many programming languages, it is important to remember to check for the null value.
When using Option, the type system requires these checks in the right places: Option α and α are not the same type, and converting from one to the other requires handling the case of none.
This can be done via helpers such as Option.getD, or with pattern matching.
def postalCodes : Std.HashMap Nat String :=
.empty |>.insert 12345 "Schenectady"
#eval postalCodes[12346]?.getD "not found"
"not found"
#eval
match postalCodes[12346]? with
| none => "not found"
| some city => city
"not found"
#eval
if let some city := postalCodes[12345]? then
city
else
"not found"
"Schenectady"
Option.{u} (α : Type u) : Type u
Optional values, which are either some around a value from the underlying type or none.
Option can represent nullable types or computations that might fail. In the codomain of a function
type, it can also represent partiality.
none.{u} {α : Type u} : Option αNo value.
some.{u} {α : Type u} (val : α) : Option α
Some value of type α.
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.
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.
Option.get.{u} {α : Type u} (o : Option α) :
o.isSome = true → α
Extracts the value from an option that can be proven to be some.
Option.getD.{u_1} {α : Type u_1}
(opt : Option α) (dflt : α) : α
Option.getDM.{u_1, u_2}
{m : Type u_1 → Type u_2} {α : Type u_1}
[Monad m] (x : Option α) (y : m α) : m α
Gets the value in an option, monadically computing a default value on none.
This is the monadic analogue of Option.getD.
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.
Option.elim.{u_1, u_2} {α : Type u_1}
{β : Sort u_2} : Option α → β → (α → β) → β
A case analysis function for Option.
Given a value for none and a function to apply to the contents of some, Option.elim checks
which constructor a given Option consists of, and uses the appropriate argument.
Option.elim is an elimination principle for Option. In particular, it is a non-dependent version
of Option.recOn. It can also be seen as a combination of Option.map and Option.getD.
Examples:
(some "hello").elim 0 String.length = 5
none.elim 0 String.length = 0
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 case analysis function for Option.
Given a fallback computation for none and a monadic operation to apply to the contents of some,
Option.elimM checks which constructor a given Option consists of, and uses the appropriate
argument.
Option.elimM can also be seen as a combination of Option.mapM and Option.getDM. It is a
monadic analogue of Option.elim.
Option.liftOrGet.{u_1} {α : Type u_1}
(f : α → α → α) :
Option α → Option α → Option αApplies a function to a two optional values if both are present. Otherwise, if one value is present, it is returned and the function is not used.
The value is some (f a b) if the inputs are some a and some b. Otherwise, the behavior is
equivalent to Option.orElse. If only one input is some x, then the value is some x. If both
are none, then the value is none.
Examples:
Option.liftOrGet (· + ·) none (some 3) = some 3
Option.liftOrGet (· + ·) (some 2) (some 3) = some 5
Option.liftOrGet (· + ·) (some 2) none = some 2
Option.liftOrGet (· + ·) none none = none
Option.merge.{u_1} {α : Type u_1}
(fn : α → α → α) :
Option α → Option α → Option αApplies a function to a two optional values if both are present. Otherwise, if one value is present, it is returned and the function is not used.
The value is some (fn a b) if the inputs are some a and some b. Otherwise, the behavior is
equivalent to Option.orElse: if only one input is some x, then the value is some x, and if
both are none, then the value is none.
Examples:
Option.merge (· + ·) none (some 3) = some 3
Option.merge (· + ·) (some 2) (some 3) = some 5
Option.merge (· + ·) (some 2) none = some 2
Option.merge (· + ·) none none = none
Ordering of optional values typically uses the DecidableEq (Option α), LT (Option α), Min (Option α), and Max (Option α) instances.
Option.min.{u_1} {α : Type u_1} [Min α] :
Option α → Option α → Option α
The minimum of two optional values, with none treated as the least element. This function is
usually accessed through the Min (Option α) instance, rather than directly.
Prior to nightly-2025-02-27, none was treated as the greatest element, so
min none (some x) = min (some x) none = some x.
Examples:
Option.min (some 2) (some 5) = some 2
Option.min (some 5) (some 2) = some 2
Option.min (some 2) none = none
Option.min none (some 5) = none
Option.min none none = none
Option.max.{u_1} {α : Type u_1} [Max α] :
Option α → Option α → Option αThe maximum of two optional values.
This function is usually accessed through the Max (Option α) instance, rather than directly.
Examples:
Option.max (some 2) (some 5) = some 5
Option.max (some 5) (some 2) = some 5
Option.max (some 2) none = some 2
Option.max none (some 5) = some 5
Option.max none none = none
Option.lt.{u_1, u_2} {α : Type u_1}
{β : Type u_2} (r : α → β → Prop) :
Option α → Option β → Prop
Lifts an ordering relation to Option, such that none is the least element.
It can be understood as adding a distinguished least element, represented by none, to both α and
β.
This definition is part of the implementation of the LT (Option α) instance. However, because it
can be used with heterogeneous relations, it is sometimes useful on its own.
Examples:
Option.decidable_eq_none.{u_1} {α : Type u_1}
{o : Option α} : Decidable (o = none)
Equality with 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 the standard instance of
DecidableEq (Option α), which can cause problems. It can be locally bound if needed.
Try to use the Boolean comparisons Option.isNone or Option.isSome instead.
Option.repr.{u_1} {α : Type u_1} [Repr α] :
Option α → Nat → Std.FormatReturns a representation of an optional value that should be able to be parsed as an equivalent optional value.
This function is typically accessed through the Repr (Option α) instance.
Option.format.{u} {α : Type u}
[Std.ToFormat α] : Option α → Std.FormatFormats an optional value, with no expectation that the Lean parser should be able to parse the result.
This function is usually accessed through the ToFormat (Option α) instance.
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.
Option.guard.{u_1} {α : Type u_1} (p : α → Prop)
[DecidablePred p] (a : α) : Option α
Returns none if a value doesn't satisfy a predicate, or the value itself otherwise.
From the perspective of Option as computations that might fail, this function is a run-time
assertion operator in the Option monad.
Examples:
Option.guard (· > 2) 1 = none
Option.guard (· > 2) 5 = some 5
Option.bind.{u_1, u_2} {α : Type u_1}
{β : Type u_2} :
Option α → (α → Option β) → Option β
Sequencing of Option computations.
From the perspective of Option as computations that might fail, this function sequences
potentially-failing computations, failing if either fails. From the perspective of Option as a
collection with at most one element, the function is applied to the element if present, and the
final result is empty if either the initial or the resulting collections are empty.
This function is often accessed via the >>= operator from the Bind (Option α) instance, or
implicitly via do-notation, but it is also idiomatic to call it using generalized field
notation.
Examples:
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 the monadic action f on o's value, if any, and returns the result, or none if there is
no value.
From the perspective of Option as a collection with at most one element, the monadic the function
is applied to the element if present, and the final result is empty if either the initial or the
resulting collections are empty.
Option.sequence.{u, u_1} {m : Type u → Type u_1}
[Monad m] {α : Type u} :
Option (m α) → m (Option α)Converts an optional monadic computation into a monadic computation of an optional value.
Example:
#eval show IO (Option String) from
Option.sequence <| some do
IO.println "hello"
return "world"
hello
some "world"Option.tryCatch.{u_1} {α : Type u_1}
(x : Option α) (handle : Unit → Option α) :
Option α
Recover from failing Option computations with a handler function.
This function is usually accessed through the MonadExceptOf Unit Option instance.
Examples:
Option.tryCatch none (fun () => some "handled") = some "handled"
Option.tryCatch (some "succeeded") (fun () => some "handled") = some "succeeded"
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.
Option.all.{u_1} {α : Type u_1} (p : α → Bool) :
Option α → Bool
Checks whether an optional value either satisfies a Boolean predicate or is none.
Examples:
`(some 33).all (· % 2 == 0) = false
`(some 22).all (· % 2 == 0) = true
`none.all (fun x : Nat => x % 2 == 0) = true
Option.any.{u_1} {α : Type u_1} (p : α → Bool) :
Option α → Bool
Checks whether an optional value is not none and satisfies a Boolean predicate.
Examples:
`(some 33).any (· % 2 == 0) = false
`(some 22).any (· % 2 == 0) = true
`none.any (fun x : Nat => true) = false
Option.filter.{u_1} {α : Type u_1}
(p : α → Bool) : Option α → Option αKeeps an optional value only if it satisfies a Boolean predicate.
If Option is thought of as a collection that contains at most one element, then Option.filter is
analogous to List.filter or Array.filter.
Examples:
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
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 β)
Applies a function in some applicative functor to an optional value, returning none with no
effects if the value is missing.
This is analogous to Option.mapM for monads.
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, returning the result. If the optional value is
none, the function is not called and the result is also none.
From the perspective of Option as a container with at most one element, this is analogous to
List.mapM, returning the result of running the monadic function on all elements of the container.
Option.mapA is the corresponding operation for applicative functors.
Option.attach.{u_1} {α : Type u_1}
(xs : Option α) : Option { x // x ∈ xs }“Attaches” a proof that an optional value, if present, is indeed this value, returning a subtype that expresses this fact.
This function is primarily used to allow definitions by well-founded recursion that use iteration
operators (such as Option.map) to prove that an optional value drawn from a parameter is smaller
than the parameter. This allows the well-founded recursion mechanism to prove that the function
terminates.
Option.attachWith.{u_1} {α : Type u_1}
(xs : Option α) (P : α → Prop)
(H : ∀ (x : α), x ∈ xs → P x) :
Option { x // P x }“Attaches” a proof that some predicate holds for an optional value, if present, returning a subtype that expresses this fact.
This function is primarily used to implement Option.attach, which allows definitions by
well-founded recursion that use iteration operators (such as Option.map) to prove that an optional
value drawn from a parameter is smaller than the parameter. This allows the well-founded recursion
mechanism to prove that the function terminates.
Option.unattach.{u_1} {α : Type u_1}
{p : α → Prop} (o : Option { x // p x }) :
Option α
Remove an attached proof that the value in an Option is indeed that value.
This function is usually inserted automatically by Lean, rather than explicitly in code. It is introduced as an intermediate step during the elaboration of definitions by well-founded recursion.
If this function is encountered in a proof state, the right approach is usually the tactic
simp [Option.unattach, -Option.map_subtype].
It is a synonym for Option.map Subtype.val.
Option.choice.{u_1} (α : Type u_1) : Option α
Option.pbind.{u_1, u_2} {α : Type u_1}
{β : Type u_2} (o : Option α)
(f : (a : α) → a ∈ o → Option β) : Option β
Given an optional value and a function that can be applied when the value is some, returns the
result of applying the function if this is possible.
The function f is partial because it is only defined for the values a : α such a ∈ o, which
is equivalent to o = some a. This restriction allows the function to use the fact that it can only
be called when o is not none: it can relate its argument to the optional value o. Its runtime
behavior is equivalent to that of Option.bind.
Examples:
def attach (v : Option α) : Option { y : α // y ∈ v } :=
v.pbind fun x h => some ⟨x, h⟩
#reduce attach (some 3)
some ⟨3, ⋯⟩#reduce attach none
noneOption.pelim.{u_1, u_2} {α : Type u_1}
{β : Sort u_2} (o : Option α) (b : β)
(f : (a : α) → a ∈ o → β) : β
Given an optional value and a function that can be applied when the value is some, returns the
result of applying the function if this is possible, or a fallback value otherwise.
The function f is partial because it is only defined for the values a : α such a ∈ o, which
is equivalent to o = some a. This restriction allows the function to use the fact that it can only
be called when o is not none: it can relate its argument to the optional value o. Its runtime
behavior is equivalent to that of Option.elim.
Examples:
def attach (v : Option α) : Option { y : α // y ∈ v } :=
v.pelim none fun x h => some ⟨x, h⟩
#reduce attach (some 3)
some ⟨3, ⋯⟩#reduce attach none
noneOption.pmap.{u_1, u_2} {α : Type u_1}
{β : Type u_2} {p : α → Prop}
(f : (a : α) → p a → β) (o : Option α) :
(∀ (a : α), a ∈ o → p a) → Option β
Given a function from the elements of α that satisfy p to β and a proof that an optional value
satisfies p if it's present, applies the function to the value.
Examples:
def attach (v : Option α) : Option { y : α // y ∈ v } :=
v.pmap (fun a (h : a ∈ v) => ⟨_, h⟩) (fun _ h => h)
#reduce attach (some 3)
some ⟨3, ⋯⟩#reduce attach none
none