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