10.1. Optional Values🔗

Planned Content

Describe Option, including the default coercions and its API.

Tracked at issue #110

🔗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