option

Option.filter

def filter {A : Type} (test : A -> Bool) (o : Option A) : Option A

The value, if it passes the test.

Option.join

def join {A : Type} (o : Option (Option A)) : Option A

A nested option flattened.

Option.zipWith

def zipWith {A : Type} {B : Type} {C : Type} (f : A -> B -> C) (oa : Option A) (ob : Option B) : Option C

f of both values when both are present.

Option.zip

def zip {A : Type} {B : Type} (oa : Option A) (ob : Option B) : Option (A * B)

Both values as a pair, when both are present.

Option.apply

def apply {A : Type} {B : Type} (of : Option (A -> B)) (oa : Option A) : Option B

A present function applied to a present value.

Option.fold

def fold {A : Type} {B : Type} (absent : B) (f : A -> B) (o : Option A) : B

f of the value, or absent when there is none.

Option.any

def any {A : Type} (test : A -> Bool) (o : Option A) : Bool

Whether there is a value and it passes the test.

Option.all

def all {A : Type} (test : A -> Bool) (o : Option A) : Bool

Whether every value (none, or the one there is) passes the test.

Option.when

def when {A : Type} (condition : Bool) (a : A) : Option A

some a when the condition holds, else none.

Option.mapIdentity

def mapIdentity {A : Type} (o : Option A) : Option.map (fun (a : A) => a) o = o

Mapping the identity changes nothing.

Option.mapCompose

def mapCompose {A : Type} {B : Type} {C : Type} (f : A -> B) (g : B -> C) (o : Option A) : Option.map g (Option.map f o) = Option.map (fun (a : A) => g (f a)) o

Mapping twice is mapping the composition.

Option.bindSome

def bindSome {A : Type} {B : Type} (a : A) (f : A -> Option B) : Option.bind (some a) f = f a

Chaining a present value into f is f of it.

Option.bindIntoSome

def bindIntoSome {A : Type} (o : Option A) : Option.bind o (fun (a : A) => some a) = o

Chaining into some changes nothing.

Option.bindAssociative

def bindAssociative {A : Type} {B : Type} {C : Type} (o : Option A) (f : A -> Option B) (g : B -> Option C) : Option.bind (Option.bind o f) g = Option.bind o (fun (a : A) => Option.bind (f a) g)

Chaining is associative.

Option.joinIsBind

def joinIsBind {A : Type} (o : Option (Option A)) : join o = Option.bind o (fun (inner : Option A) => inner)

Flattening is chaining into the inner option.

Option.orElseAssociative

def orElseAssociative {A : Type} (a : Option A) (b : Option A) (c : Option A) : Option.orElse (Option.orElse a b) c = Option.orElse a (Option.orElse b c)

Taking the first present option is associative.

Option.withDefaultIsFold

def withDefaultIsFold {A : Type} (d : A) (o : Option A) : Option.withDefault d o = fold d (fun (a : A) => a) o

The value or a default is a fold.