either

Either.bind

def bind {E : Type} {A : Type} {B : Type} (e : Either E A) (f : A -> Either E B) : Either E B

The result of f on a right value; a left value stays (the chaining of the Monad (Either E) instance).

Either.join

def join {E : Type} {A : Type} (e : Either E (Either E A)) : Either E A

A nested right flattened.

Either.apply

def apply {E : Type} {A : Type} {B : Type} (ef : Either E (A -> B)) (ea : Either E A) : Either E B

A function in a right applied to a value in a right; the first left otherwise.

Either.orElse

def orElse {E : Type} {A : Type} (e : Either E A) (recover : E -> Either E A) : Either E A

A left value handed to recover; a right value stays.

Either.traverse

def traverse {E : Type} {A : Type} {B : Type} (f : A -> Either E B) (xs : List A) : Either E (List B)

f on every element, the results in a right; the first left otherwise.

Either.sequence

def sequence {E : Type} {A : Type} (xs : List (Either E A)) : Either E (List A)

The values of a list of rights; the first left otherwise.

Either.partition

def partition {A : Type} {B : Type} (xs : List (Either A B)) : List A * List B

The left values and the right values of a list, each in order.

Either.lefts

def lefts {A : Type} {B : Type} (xs : List (Either A B)) : List A

The left values of a list, in order.

Either.rights

def rights {A : Type} {B : Type} (xs : List (Either A B)) : List B

The right values of a list, in order.

Either.toOption

def toOption {A : Type} {B : Type} (e : Either A B) : Option B

The right value, if there is one.

Either.ofOption

def ofOption {A : Type} {B : Type} (missing : A) (o : Option B) : Either A B

A present value as a right, an absent one as left missing.

Either.merge

def merge {A : Type} (e : Either A A) : A

The value, whichever side it is on.

Either.bimapIdentity

def bimapIdentity {A : Type} {B : Type} (e : Either A B) : bimap (fun (a : A) => a) (fun (b : B) => b) e = e

Mapping both sides with identities changes nothing.

Either.bimapCompose

def bimapCompose {A : Type} {B : Type} {C : Type} {D : Type} {E : Type} {F : Type} (f : A -> C) (f2 : C -> E) (g : B -> D) (g2 : D -> F) (e : Either A B) : bimap f2 g2 (bimap f g e) = bimap (fun (a : A) => f2 (f a)) (fun (b : B) => g2 (g b)) e

Mapping both sides twice is mapping with the compositions.

Either.bimapSplits

def bimapSplits {A : Type} {B : Type} {C : Type} {D : Type} (f : A -> C) (g : B -> D) (e : Either A B) : bimap f g e = mapRight g (mapLeft f e)

Mapping both sides is mapping the left, then the right.

Either.swapSidesTwice

def swapSidesTwice {A : Type} {B : Type} (e : Either A B) : swapSides (swapSides e) = e

Swapping twice gives the value back.

Either.foldBimap

def foldBimap {A : Type} {B : Type} {C : Type} {D : Type} {E : Type} (f : A -> C) (g : B -> D) (h : C -> E) (k : D -> E) (e : Either A B) : fold h k (bimap f g e) = fold (fun (a : A) => h (f a)) (fun (b : B) => k (g b)) e

Folding after mapping is folding with the compositions.

Either.bindRight

def bindRight {E : Type} {A : Type} {B : Type} (a : A) (f : A -> Either E B) : bind (right a) f = f a

Chaining a right into f is f of its value.

Either.bindIntoRight

def bindIntoRight {E : Type} {A : Type} (e : Either E A) : bind e (fun (a : A) => right a) = e

Chaining into right changes nothing.

Either.bindAssociative

def bindAssociative {E : Type} {A : Type} {B : Type} {C : Type} (e : Either E A) (f : A -> Either E B) (g : B -> Either E C) : bind (bind e f) g = bind e (fun (a : A) => bind (f a) g)

Chaining is associative.