monad

IsMonadAssoc

def IsMonadAssoc (M : Type -> Type) (bnd : (A : Type) -> (B : Type) -> M A -> (A -> M B) -> M B) : Type 1

The monad associativity law for bind: bind (bind m f) g = bind m (fun a => bind (f a) g).

IsMonad

def IsMonad (M : Type -> Type) (ret : (A : Type) -> A -> M A) (bnd : (A : Type) -> (B : Type) -> M A -> (A -> M B) -> M B) : Type 1

The type saying return and bind make M a lawful monad: left identity, right identity and associativity.

kleisli

def kleisli (M : Type -> Type) (bnd : (A : Type) -> (B : Type) -> M A -> (A -> M B) -> M B) (A : Type) (B : Type) (C : Type) (f : A -> M B) (g : B -> M C) (a : A) : M C

Kleisli composition for a monad given by its bind: run f, then feed the result to g.

pureOption

def pureOption (A : Type) (a : A) : Option A

The monadic return for Maybe with an explicit type argument: wraps a value in just.

bindOptionFull

def bindOptionFull (A : Type) (B : Type) (mx : Option A) (f : A -> Option B) : Option B

The monadic bind for Maybe with explicit type arguments: continues with the value, or propagates nothing.

joinOption

def joinOption (A : Type) (mmx : Option (Option A)) : Option A

Flattens a nested Maybe: just (just a) becomes just a, anything else nothing.

bindOptionLeftId

def bindOptionLeftId (A : Type) (B : Type) (a : A) (f : A -> Option B) : bindOptionFull A B (pureOption A a) f ≡ f a

The Maybe monad satisfies left identity: bind (pure a) f = f a.

bindOptionRightId

def bindOptionRightId (A : Type) (mx : Option A) : bindOptionFull A A mx (pureOption A) ≡ mx

The Maybe monad satisfies right identity: bind m pure = m.

bindOptionAssoc

def bindOptionAssoc (A : Type) (B : Type) (C : Type) (mx : Option A) (f : A -> Option B) (g : B -> Option C) : bindOptionFull B C (bindOptionFull A B mx f) g ≡ bindOptionFull A C mx (fun (a : A) => bindOptionFull B C (f a) g)

The Maybe monad’s bind is associative: bind (bind m f) g = bind m (fun a => bind (f a) g).

optionIsMonad

def optionIsMonad : IsMonad Option pureOption bindOptionFull

Maybe with pureMaybe and bindMaybeFull is a lawful monad.

pureList

def pureList (A : Type) (a : A) : List A

The monadic return for List: the singleton list.

bindList

def bindList (A : Type) (B : Type) (xs : List A) (f : A -> List B) : List B

The monadic bind for List (flatMap): applies f to each element and concatenates the results.

joinList

def joinList (A : Type) (xss : List (List A)) : List A

Flattens a list of lists by concatenation.

bindListLeftId

def bindListLeftId (A : Type) (B : Type) (a : A) (f : A -> List B) : bindList A B (pureList A a) f ≡ f a

The List monad satisfies left identity: bind [a] f = f a.

bindListRightId

def bindListRightId (A : Type) (xs : List A) : bindList A A xs (pureList A) ≡ xs

The List monad satisfies right identity: bind xs pure = xs.

bindListAppend

def bindListAppend (A : Type) (B : Type) (xs : List A) (ys : List A) (f : A -> List B) : bindList A B (append xs ys) f ≡ append (bindList A B xs f) (bindList A B ys f)

Binding distributes over append: bind (xs ++ ys) f = bind xs f ++ bind ys f.

listAssoc

def listAssoc (A : Type) (B : Type) (C : Type) (xs : List A) (f : A -> List B) (g : B -> List C) : bindList B C (bindList A B xs f) g ≡ bindList A C xs (fun (a : A) => bindList B C (f a) g)

The List monad’s bind is associative: bind (bind xs f) g = bind xs (fun a => bind (f a) g).

listIsMonad

def listIsMonad : IsMonad List pureList bindList

List with pureList and bindList is a lawful monad.

kleisliOptionLeftId

def kleisliOptionLeftId (A : Type) (B : Type) (f : A -> Option B) (a : A) : kleisliOption A A B (pureOption A) f a ≡ f a

Pure is a left identity for Kleisli composition in Maybe.

kleisliOptionRightId

def kleisliOptionRightId (A : Type) (B : Type) (f : A -> Option B) (a : A) : kleisliOption A B B f (pureOption B) a ≡ f a

Pure is a right identity for Kleisli composition in Maybe.

kleisliOptionAssoc

def kleisliOptionAssoc (A : Type) (B : Type) (C : Type) (D : Type) (f : A -> Option B) (g : B -> Option C) (h : C -> Option D) (a : A) : kleisliOption A C D (fun (x : A) => kleisliOption A B C f g x) h a ≡ kleisliOption A B D f (fun (b : B) => kleisliOption B C D g h b) a

Kleisli composition in Maybe is associative: (f >=> g) >=> h = f >=> (g >=> h).

kleisliListLeftId

def kleisliListLeftId (A : Type) (B : Type) (f : A -> List B) (a : A) : kleisliList A A B (pureList A) f a ≡ f a

Pure is a left identity for Kleisli composition in List.

kleisliListRightId

def kleisliListRightId (A : Type) (B : Type) (f : A -> List B) (a : A) : kleisliList A B B f (pureList B) a ≡ f a

Pure is a right identity for Kleisli composition in List.

joinOptionNone

def joinOptionNone (A : Type) : joinOption A (none : Option (Option A)) ≡ (none : Option A)

Joining nothing gives nothing.

joinOptionSomeNone

def joinOptionSomeNone (A : Type) : joinOption A (some (none : Option A)) ≡ (none : Option A)

Joining just nothing gives nothing.

joinOptionSomeSome

def joinOptionSomeSome (A : Type) (a : A) : joinOption A (some (some a)) ≡ some a

Joining just (just a) gives just a.

joinOptionPure

def joinOptionPure (A : Type) (mx : Option A) : joinOption A (pureOption (Option A) mx) ≡ mx

Join after pure is the identity on Maybe: join (pure m) = m.

joinOptionFmapPureSome

def joinOptionFmapPureSome (A : Type) (x : A) : joinOption A (some (pureOption A x)) ≡ some x

Join after mapping pure is the identity, just case: join (just (pure x)) = just x.

joinListNil

def joinListNil (A : Type) : joinList A (nil : List (List A)) ≡ (nil : List A)

Flattening the empty list of lists gives the empty list.

joinListSingleton

def joinListSingleton (A : Type) (xs : List A) : joinList A (cons xs nil) ≡ xs

Flattening a one-element list of lists gives that element.

joinListConsNil

def joinListConsNil (A : Type) (xss : List (List A)) : joinList A (cons nil xss) ≡ joinList A xss

Flattening skips a leading empty list: join ([] :: xss) = join xss.

mapViaBind

def mapViaBind (A : Type) (B : Type) (f : A -> B) (mx : Option A) : Option B

The functor map for Maybe expressed through bind and pure.

mapViaBindNone

def mapViaBindNone (A : Type) (B : Type) (f : A -> B) : mapViaBind A B f (none : Option A) ≡ (none : Option B)

Mapping via bind over nothing gives nothing.

mapViaBindSome

def mapViaBindSome (A : Type) (B : Type) (f : A -> B) (x : A) : mapViaBind A B f (some x) ≡ some (f x)

Mapping via bind over just x gives just (f x).

guardOption

def guardOption (b : Bool) : Option Unit

Guard for Maybe: just unit when the condition is true, nothing otherwise.

filterOption

def filterOption (A : Type) (p : A -> Bool) (mx : Option A) : Option A

Keeps the contained value only when it satisfies the Boolean predicate p, otherwise gives nothing.

mapViaBindList

def mapViaBindList (A : Type) (B : Type) (f : A -> B) (xs : List A) : List B

The functor map for List expressed through bind and pure.

mapViaBindListNil

def mapViaBindListNil (A : Type) (B : Type) (f : A -> B) : mapViaBindList A B f (nil : List A) ≡ (nil : List B)

Mapping via bind over the empty list gives the empty list.

mapViaBindListCons

def mapViaBindListCons (A : Type) (B : Type) (f : A -> B) (x : A) (xs : List A) : mapViaBindList A B f (cons x xs) ≡ cons (f x) (mapViaBindList A B f xs)

Mapping via bind over a cons list maps the head and recurses: map f (x :: xs) = f x :: map f xs.

filterViaBind

def filterViaBind (A : Type) (p : A -> Bool) (xs : List A) : List A

Filters a list by the Boolean predicate p, expressed through bind.

optionBindMapNone

def optionBindMapNone (A : Type) (B : Type) (f : A -> B) : bindOptionFull A B (none : Option A) (fun (a : A) => pureOption B (f a)) ≡ (none : Option B)

Binding nothing with pure ∘ f gives nothing.

optionBindMapSome

def optionBindMapSome (A : Type) (B : Type) (f : A -> B) (x : A) : bindOptionFull A B (some x) (fun (a : A) => pureOption B (f a)) ≡ some (f x)

Binding just x with pure ∘ f gives just (f x).

optionBindFmapNone

def optionBindFmapNone (A : Type) (B : Type) (C : Type) (f : A -> B) (g : B -> Option C) : bindOptionFull B C (none : Option B) g ≡ (none : Option C)

Binding nothing with any continuation gives nothing.

optionBindFmapSome

def optionBindFmapSome (A : Type) (B : Type) (C : Type) (f : A -> B) (g : B -> Option C) (x : A) : bindOptionFull B C (some (f x)) g ≡ g (f x)

Binding just (f x) with g gives g (f x).

optionPureNatWitness

def optionPureNatWitness (A : Type) (B : Type) (f : A -> B) (a : A) : some (f a) ≡ pureOption B (f a)

just (f a) is pure (f a), the computation behind naturality of pure for Maybe.

optionJoinNatNone

def optionJoinNatNone (A : Type) (B : Type) (f : A -> B) : joinOption B (none : Option (Option B)) ≡ (none : Option B)

Joining nothing gives nothing (a case of naturality of join for Maybe).

optionJoinNatSomeNone

def optionJoinNatSomeNone (A : Type) (B : Type) (f : A -> B) : joinOption B (some (none : Option B)) ≡ (none : Option B)

Joining just nothing gives nothing (a case of naturality of join for Maybe).

optionJoinNatSomeSome

def optionJoinNatSomeSome (A : Type) (B : Type) (f : A -> B) (x : A) : joinOption B (some (some (f x))) ≡ some (f x)

Joining just (just (f x)) gives just (f x) (a case of naturality of join for Maybe).

strengthOption

def strengthOption (A : Type) (B : Type) (p : (a : A) × Option B) : Option ((a : A) × B)

The strength of Maybe: moves a pair whose second component is a Maybe inside the Maybe.

strengthList

def strengthList (A : Type) (B : Type) (a : A) (xs : List B) : List ((a2 : A) × B)

The strength of List: pairs a fixed value a with every element of the list.

strengthListNil

def strengthListNil (A : Type) (B : Type) (a : A) : strengthList A B a (nil : List B) ≡ (nil : List ((a2 : A) × B))

The strength of List on the empty list is the empty list.

liftM2Option

def liftM2Option (A : Type) (B : Type) (C : Type) (f : A -> B -> C) (mx : Option A) (my : Option B) : Option C

Lifts a binary function to Maybe: applies f when both arguments are present.

liftM2List

def liftM2List (A : Type) (B : Type) (C : Type) (f : A -> B -> C) (xs : List A) (ys : List B) : List C

Lifts a binary function to List: applies f to every pair from the Cartesian product.

sequenceOption

def sequenceOption (A : Type) (xs : List (Option A)) : Option (List A)

Turns a list of Maybes into a Maybe list: just the values if all are present, otherwise nothing.

traverseOption

def traverseOption (A : Type) (B : Type) (f : A -> Option B) (xs : List A) : Option (List B)

Applies a partial function to every element: just the results if all succeed, otherwise nothing.

optionToListPure

def optionToListPure (A : Type) (a : A) : Option.toList A (pureOption A a) ≡ pureList A a

Converting Maybe to List sends pure to pure: maybeToList (pure a) = [a].

optionToListBindNone

def optionToListBindNone (A : Type) (B : Type) (f : A -> Option B) : Option.toList B (bindOptionFull A B (none : Option A) f) ≡ bindList A B (Option.toList A (none : Option A)) (fun (a : A) => Option.toList B (f a))

Converting Maybe to List preserves bind, nothing case.

optionToListBindSome

def optionToListBindSome (A : Type) (B : Type) (a : A) (f : A -> Option B) : Option.toList B (bindOptionFull A B (some a) f) ≡ bindList A B (Option.toList A (some a)) (fun (x : A) => Option.toList B (f x))

Converting Maybe to List preserves bind, just case.

listToOption

def listToOption (A : Type) (xs : List A) : Option A

The head of a list as a Maybe: nothing for the empty list.

orElseOption

def orElseOption (A : Type) (mx : Option A) (my : Option A) : Option A

Left-biased choice for Maybe: the first argument if present, otherwise the second.

orElseOptionNoneL

def orElseOptionNoneL (A : Type) (my : Option A) : orElseOption A (none : Option A) my ≡ my

nothing is a left identity for orElseMaybe.

orElseOptionSomeL

def orElseOptionSomeL (A : Type) (x : A) (my : Option A) : orElseOption A (some x) my ≡ some x

orElseMaybe returns a present left argument: orElse (just x) m = just x.

orElseOptionAssoc

def orElseOptionAssoc (A : Type) (mx : Option A) (my : Option A) (mz : Option A) : orElseOption A (orElseOption A mx my) mz ≡ orElseOption A mx (orElseOption A my mz)

orElseMaybe is associative.

orElseOptionNoneR

def orElseOptionNoneR (A : Type) (mx : Option A) : orElseOption A mx (none : Option A) ≡ mx

nothing is a right identity for orElseMaybe.

apOption

def apOption (A : Type) (B : Type) (mf : Option (A -> B)) (mx : Option A) : Option B

The applicative apply for Maybe: applies a wrapped function to a wrapped value, nothing if either is missing.

apOptionId

def apOptionId (A : Type) (mx : Option A) : apOption A A (some (fun (a : A) => a)) mx ≡ mx

The Maybe applicative satisfies the identity law: cong (just id) m = m.

voidOption

def voidOption (A : Type) (mx : Option A) : Option Unit

Discards the contained value, keeping only whether it is present.

whenOption

def whenOption (b : Bool) : Option Unit

just unit when the condition is true, nothing otherwise.

unlessOption

def unlessOption (b : Bool) : Option Unit

just unit when the condition is false, nothing otherwise.

safeHead

def safeHead : List Nat -> Option Nat

The head of a list of naturals, or nothing for the empty list.

safePred

def safePred : Nat -> Option Nat

The predecessor of a natural number, or nothing for zero.

kleisli_head_pred

def kleisli_head_pred (xs : List Nat) : Option Nat

Example Kleisli composite in Maybe: the predecessor of the head of a list, if both exist.

kleisliOptionPureLeft

def kleisliOptionPureLeft (f : Nat -> Option Nat) (n : Nat) : kleisliOption Nat Nat Nat (pureOption Nat) f n ≡ f n

Pure is a left identity for Kleisli composition in Maybe (on Nat).

kleisliOptionPureRight

def kleisliOptionPureRight (f : Nat -> Option Nat) (n : Nat) : kleisliOption Nat Nat Nat f (pureOption Nat) n ≡ f n

Pure is a right identity for Kleisli composition in Maybe (on Nat).

duplicateList

def duplicateList (n : Nat) : List Nat

The two-element list [n, n].

succList

def succList (n : Nat) : List Nat

The singleton list [n + 1].

kleisli_dup_succ

def kleisli_dup_succ (n : Nat) : List Nat

Example Kleisli composite in List: duplicate n, then take each successor, giving [n + 1, n + 1].

joinMapNone

def joinMapNone (A : Type) (B : Type) (f : A -> Option B) : joinOption B (mapViaBind A (Option B) f (none : Option A)) ≡ bindOptionFull A B (none : Option A) f

Bind is join after map for Maybe, nothing case.

joinMapSome

def joinMapSome (A : Type) (B : Type) (f : A -> Option B) (a : A) : joinOption B (mapViaBind A (Option B) f (some a)) ≡ bindOptionFull A B (some a) f

Bind is join after map for Maybe, just case.

joinMapNil

def joinMapNil (A : Type) (B : Type) (f : A -> List B) : joinList B (mapViaBindList A (List B) f (nil : List A)) ≡ bindList A B (nil : List A) f

Bind is join after map for List, empty-list case.

joinMapSingleton

def joinMapSingleton (A : Type) (B : Type) (f : A -> List B) (a : A) : joinList B (mapViaBindList A (List B) f (cons a (nil : List A))) ≡ append (f a) (nil : List B)

Join after map on a singleton list [a] gives f a ++ [].

mapViaBindIdNone

def mapViaBindIdNone (A : Type) : mapViaBind A A (fun (x : A) => x) (none : Option A) ≡ (none : Option A)

Mapping the identity via bind over nothing gives nothing.

mapViaBindIdSome

def mapViaBindIdSome (A : Type) (a : A) : mapViaBind A A (fun (x : A) => x) (some a) ≡ some a

Mapping the identity via bind over just a gives just a.

mapViaBindCompNone

def mapViaBindCompNone (A B C : Type) (f : B -> C) (g : A -> B) : mapViaBind B C f (mapViaBind A B g (none : Option A)) ≡ mapViaBind A C (fun (x : A) => f (g x)) (none : Option A)

Mapping via bind respects composition, nothing case.

mapViaBindCompSome

def mapViaBindCompSome (A B C : Type) (f : B -> C) (g : A -> B) (a : A) : mapViaBind B C f (mapViaBind A B g (some a)) ≡ mapViaBind A C (fun (x : A) => f (g x)) (some a)

Mapping via bind respects composition, just case.

filterOptionFalse

def filterOptionFalse (A : Type) (mx : Option A) : filterOption A (fun (_ : A) => false) mx ≡ (none : Option A)

Filtering with the always-false predicate gives nothing.

filterOptionTrueSome

def filterOptionTrueSome (A : Type) (x : A) : filterOption A (fun (_ : A) => true) (some x) ≡ some x

Filtering just x with the always-true predicate keeps it.

guardBindTrueF

def guardBindTrueF (B : Type) (f : Unit -> Option B) : bindOptionFull Unit B (guardOption true) f ≡ f unit

Binding a true guard continues: bind (guard true) f = f unit.

guardBindFalseF

def guardBindFalseF (B : Type) (f : Unit -> Option B) : bindOptionFull Unit B (guardOption false) f ≡ (none : Option B)

Binding a false guard fails: bind (guard false) f = nothing.

triple_pred

def triple_pred (n : Nat) : Option Nat

Example bind chain: the predecessor taken three times, nothing if n < 3.

quadruplicate

def quadruplicate (n : Nat) : List Nat

Example bind chain: duplicating twice gives four copies of n.

double_succ_list

def double_succ_list (n : Nat) : List Nat

Example bind chain: the successor taken twice, as a singleton list [n + 2].