Extends the theory on functors, applicatives and monads.

theorem Functor.map_map {α : Type u} {β : Type u} {γ : Type u} {f : Type u → Type v} [Functor f] [LawfulFunctor f] (m : α → β) (g : β → γ) (x : f α) : g <$> m <$> x = (g ∘ m) <$> x

def zipWithM {F : Type u → Type v} [Applicative F] {α₁ : Type u} {α₂ : Type u} {φ : 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) = Seq.seq ((fun (x : φ) (x_1 : List φ) => x :: x_1) <$> f x_2 y) fun (x : Unit) => zipWithM f xs ys
• zipWithM f x✝ x = pure []

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

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

Equations

• zipWithM' f (x_2 :: xs) (y :: ys) = SeqRight.seqRight (f x_2 y) fun (x : Unit) => 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 α) : (Seq.seq (pure fun (x : α) => x) fun (x_1 : Unit) => x) = x

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

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

theorem map_bind {α : Type u} {β : Type u} {γ : Type u} {m : Type u → Type v} [Monad m] [LawfulMonad m] (x : m α) {g : α → m β} {f : β → γ} : f <$> (x >>= g) = do let a ← x f <$> g a

theorem seq_bind_eq {α : Type u} {β : Type u} {γ : 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} {β : Type u} (f : α → m β) : pure >=> f = f

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

def List.mapAccumRM {α : Type u} {β' : Type v} {γ' : 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

• One or more equations did not get rendered due to their size.
• List.mapAccumRM f x [] = pure (x, [])

def List.mapAccumLM {α : Type u} {β' : Type v} {γ' : 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

• One or more equations did not get rendered due to their size.
• List.mapAccumLM f x [] = pure (x, [])

theorem joinM_map_map {m : Type u → Type u} [Monad m] [LawfulMonad m] {α : Type u} {β : 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 = HOrElse.hOrElse (Functor.mapConst true x) fun (x : Unit) => 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 = HOrElse.hOrElse (Functor.mapConst () x) fun (x : Unit) => 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 = HOrElse.hOrElse (some <$> x) fun (x : Unit) => 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.bind x✝ x = match x✝, x with | Sum.inl x, x_1 => Sum.inl x | Sum.inr x, f => f x

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

Equations

• Sum.instMonadSum = Monad.mk

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

class CommApplicative (m : Type u → Type v) [Applicative m] extends LawfulApplicative : 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 β), (SeqLeft.seqLeft x fun (x : Unit) => y) = Seq.seq (Function.const β <$> x) fun (x : Unit) => y
• seqRight_eq : ∀ {α β : Type u} (x : m α) (y : m β), (SeqRight.seqRight x fun (x : Unit) => y) = Seq.seq (Function.const α id <$> x) fun (x : Unit) => y
• pure_seq : ∀ {α β : Type u} (g : α → β) (x : m α), (Seq.seq (pure g) fun (x_1 : Unit) => x) = g <$> x
• map_pure : ∀ {α β : Type u} (g : α → β) (x : α), g <$> pure x = pure (g x)
• seq_pure : ∀ {α β : Type u} (g : m (α → β)) (x : α), (Seq.seq g fun (x_1 : Unit) => pure x) = (fun (h : α → β) => h x) <$> g
• seq_assoc : ∀ {α β γ : Type u} (x : m α) (g : m (α → β)) (h : m (β → γ)), (Seq.seq h fun (x_1 : Unit) => Seq.seq g fun (x_2 : Unit) => x) = Seq.seq (Seq.seq (Function.comp <$> h) fun (x : Unit) => g) fun (x_1 : Unit) => x
• commutative_prod : ∀ {α β : Type u} (a : m α) (b : m β), (Seq.seq (Prod.mk <$> a) fun (x : Unit) => b) = Seq.seq ((fun (b : β) (a : α) => (a, b)) <$> b) fun (x : Unit) => 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} {β : Type u} {γ : Type u} (a : m α) (b : m β) {f : α → β → γ} : (Seq.seq (f <$> a) fun (x : Unit) => b) = Seq.seq (flip f <$> b) fun (x : Unit) => a