Basic control operations

Extends the theory on functors, applicatives and monads.

def zipWithM {F : Type u → Type v} [Applicative F] {α₁ α₂ φ : Type u} (f : α₁ → α₂ → F φ) : List α₁ → List α₂ → F (List φ)

A generalization of List.zipWith which combines list elements with an Applicative.

Equations

• zipWithM f (x_2 :: xs) (y :: ys) = (fun (x1 : φ) (x2 : List φ) => x1 :: x2) <$> f x_2 y <*> zipWithM f xs ys
• zipWithM f x✝¹ x✝ = pure []

def zipWithM' {α β γ : Type u} {F : Type u → Type v} [Applicative F] (f : α → β → F γ) : List α → List β → F PUnit

Like zipWithM but evaluates the result as it traverses the lists using *>.

Equations

• zipWithM' f (x_2 :: xs) (y :: ys) = f x_2 y *> zipWithM' f xs ys
• zipWithM' f [] x✝ = pure PUnit.unit
• zipWithM' f x✝ [] = pure PUnit.unit

@[simp]

theorem pure_id'_seq {α : Type u} {F : Type u → Type v} [Applicative F] [LawfulApplicative F] (x : F α) : (pure fun (x : α) => x) <*> x = x

theorem seq_map_assoc {α β γ : Type u} {F : Type u → Type v} [Applicative F] [LawfulApplicative F] (x : F (α → β)) (f : γ → α) (y : F γ) : x <*> f <$> y = (fun (x : α → β) => x ∘ f) <$> x <*> y

theorem map_seq {α β γ : Type u} {F : Type u → Type v} [Applicative F] [LawfulApplicative F] (f : β → γ) (x : F (α → β)) (y : F α) : f <$> (x <*> y) = (fun (x : α → β) => f ∘ x) <$> x <*> y

theorem seq_bind_eq {α β γ : Type u} {m : Type u → Type v} [Monad m] [LawfulMonad m] (x : m α) {g : β → m γ} {f : α → β} : f <$> x >>= g = x >>= g ∘ f

theorem fish_pure {m : Type u → Type v} [Monad m] [LawfulMonad m] {α : Type u_1} {β : Type u} (f : α → m β) : f >=> pure = f

theorem fish_pipe {m : Type u → Type v} [Monad m] [LawfulMonad m] {α β : Type u} (f : α → m β) : pure >=> f = f

theorem fish_assoc {m : Type u → Type v} [Monad m] [LawfulMonad m] {α : Type u_1} {β γ φ : Type u} (f : α → m β) (g : β → m γ) (h : γ → m φ) : (f >=> g) >=> h = f >=> g >=> h

def List.mapAccumRM {α : Type u} {β' γ' : Type v} {m' : Type v → Type w} [Monad m'] (f : α → β' → m' (β' × γ')) : β' → List α → m' (β' × List γ')

Takes a value β and List α and accumulates pairs according to a monadic function f. Accumulation occurs from the right (i.e., starting from the tail of the list).

Equations

• List.mapAccumRM f x✝ [] = pure (x✝, [])
• List.mapAccumRM f x✝ (x_2 :: xs) = do let __x ← List.mapAccumRM f x✝ xs match __x with | (a', ys) => do let __x ← f x_2 a' match __x with | (a'', y) => pure (a'', y :: ys)

def List.mapAccumLM {α : Type u} {β' γ' : Type v} {m' : Type v → Type w} [Monad m'] (f : β' → α → m' (β' × γ')) : β' → List α → m' (β' × List γ')

Takes a value β and List α and accumulates pairs according to a monadic function f. Accumulation occurs from the left (i.e., starting from the head of the list).

Equations

• List.mapAccumLM f x✝ [] = pure (x✝, [])
• List.mapAccumLM f x✝ (x_2 :: xs) = do let __x ← f x✝ x_2 match __x with | (a', y) => do let __x ← List.mapAccumLM f a' xs match __x with | (a'', ys) => pure (a'', y :: ys)

theorem joinM_map_map {m : Type u → Type u} [Monad m] [LawfulMonad m] {α β : Type u} (f : α → β) (a : m (m α)) : joinM (Functor.map f <$> a) = f <$> joinM a

theorem joinM_map_joinM {m : Type u → Type u} [Monad m] [LawfulMonad m] {α : Type u} (a : m (m (m α))) : joinM (joinM <$> a) = joinM (joinM a)

@[simp]

theorem joinM_map_pure {m : Type u → Type u} [Monad m] [LawfulMonad m] {α : Type u} (a : m α) : joinM (pure <$> a) = a

@[simp]

theorem joinM_pure {m : Type u → Type u} [Monad m] [LawfulMonad m] {α : Type u} (a : m α) : joinM (pure a) = a

def succeeds {F : Type → Type v} [Alternative F] {α : Type} (x : F α) : F Bool

Returns pure true if the computation succeeds and pure false otherwise.

Equations

• succeeds x = (Functor.mapConst true x <|> pure false)

def tryM {F : Type → Type v} [Alternative F] {α : Type} (x : F α) : F Unit

Attempts to perform the computation, but fails silently if it doesn't succeed.

Equations

• tryM x = (Functor.mapConst () x <|> pure ())

def try? {F : Type → Type v} [Alternative F] {α : Type} (x : F α) : F (Option α)

Attempts to perform the computation, and returns none if it doesn't succeed.

Equations

• try? x = (some <$> x <|> pure none)

@[simp]

theorem guard_true {F : Type → Type v} [Alternative F] {h : Decidable True} : guard True = pure ()

@[simp]

theorem guard_false {F : Type → Type v} [Alternative F] {h : Decidable False} : guard False = failure

def Sum.bind {e : Type v} {α : Type u_1} {β : Type u_2} : e ⊕ α → (α → e ⊕ β) → e ⊕ β

The monadic bind operation for Sum.

Equations

• (Sum.inl x_2).bind x✝ = Sum.inl x_2
• (Sum.inr x_2).bind x✝ = x✝ x_2

@[instance_reducible]

instance Sum.instMonad_mathlib {e : Type v} : Monad (Sum e)

Equations

• One or more equations did not get rendered due to their size.

instance Sum.instLawfulFunctor_mathlib {e : Type v} : LawfulFunctor (Sum e)

instance Sum.instLawfulMonad_mathlib {e : Type v} : LawfulMonad (Sum e)

class CommApplicative (m : Type u → Type v) [Applicative m] extends LawfulApplicative m : Prop

A CommApplicative functor m is a (lawful) applicative functor which behaves identically on α × β and β × α, so computations can occur in either order.

• map_const {α β : Type u} : Functor.mapConst = Functor.map ∘ Function.const β
• id_map {α : Type u} (x : m α) : id <$> x = x
• comp_map {α β γ : Type u} (g : α → β) (h : β → γ) (x : m α) : (h ∘ g) <$> x = h <$> g <$> x
• seqLeft_eq {α β : Type u} (x : m α) (y : m β) : x <* y = Function.const β <$> x <*> y
• seqRight_eq {α β : Type u} (x : m α) (y : m β) : x *> y = Function.const α id <$> x <*> y
• pure_seq {α β : Type u} (g : α → β) (x : m α) : pure g <*> x = g <$> x
• map_pure {α β : Type u} (g : α → β) (x : α) : g <$> pure x = pure (g x)
• seq_pure {α β : Type u} (g : m (α → β)) (x : α) : g <*> pure x = (fun (h : α → β) => h x) <$> g
• seq_assoc {α β γ : Type u} (x : m α) (g : m (α → β)) (h : m (β → γ)) : h <*> (g <*> x) = Function.comp <$> h <*> g <*> x
• commutative_prod {α β : Type u} (a : m α) (b : m β) : Prod.mk <$> a <*> b = (fun (b : β) (a : α) => (a, b)) <$> b <*> a

  Computations performed first on a : α and then on b : β are equal to those performed in the reverse order.

theorem CommApplicative.commutative_map {m : Type u → Type v} [h : Applicative m] [CommApplicative m] {α β γ : Type u} (a : m α) (b : m β) {f : α → β → γ} : f <$> a <*> b = flip f <$> b <*> a