MAYBE TYPE

The type (also called ) is the disjoint union of the unit type and a given type . It represents computations that may fail or return no value () or succeed with a value ().

Formation

def Maybe (A : U) : U := + 𝟏 A

Constructors

has two constructors: (the failure case) and (the success case).

def nothing (A : U) : Maybe A := inl 𝟏 A ★
def just (A : U) (a : A) : Maybe A := inr 𝟏 A a

Eliminators

The induction principle for is derived from the induction principle of the disjoint union .

def maybe-ind (A : U) (P: Maybe A → U)
    (n: P (nothing A)) (j: Π (x: A), P (just A x))
  : Π (a: Maybe A), P a
 := +-ind 𝟏 A P (ind₁ (λ (_ : 𝟏), P (nothing A)) n) j

Non-dependent versions:

def maybe-rec (A P: U) (n: P) (j: A → P) : Maybe A → P
 := maybe-ind A (λ (_ : Maybe A), P) n j

Theorems

Standard computational rules follow from the corresponding rules of .

(See $+$-β rules in the Either section for the computational behavior.)