Laws for well behaved monadic failure operation

class LawfulAppend (α : Type u) [EmptyCollection α] [Append α] : Prop

Typeclass for instances where ∅ is an identity for ++.

• empty_append (x : α) : ∅ ++ x = x
• append_empty (x : α) : x ++ ∅ = x
• append_assoc (x y z : α) : x ++ (y ++ z) = x ++ y ++ z

instance LawfulAppend.instLawfulMonadWriterT {M : Type u → Type v} {ω : Type u} [Monad M] [EmptyCollection ω] [Append ω] [LawfulAppend ω] [LawfulMonad M] : LawfulMonad (WriterT ω M)

instance LawfulAppend.instList (α : Type u) : LawfulAppend (List α)

@[simp]

theorem WriterT.run_mk {m : Type u → Type v} [Monad m] {α ω : Type u} [LawfulMonad m] (x : m (α × ω)) : (WriterT.mk x).run = x

@[simp]

theorem WriterT.run_tell {m : Type u → Type v} [Monad m] {ω : Type u} (w : ω) : (tell w).run = pure (PUnit.unit, w)

@[simp]

theorem WriterT.run_monadLift {m : Type u → Type v} [Monad m] {ω α : Type u} [Monoid ω] (x : m α) : (monadLift x).run = (fun (x : α) => (x, 1)) <$> x

theorem WriterT.liftM_def {m : Type u → Type v} [Monad m] {ω α : Type u} [Monoid ω] (x : m α) : liftM x = WriterT.mk ((fun (x : α) => (x, 1)) <$> x)

theorem WriterT.monadLift_def {m : Type u → Type v} [Monad m] {ω α : Type u} [Monoid ω] (x : m α) : MonadLift.monadLift x = WriterT.mk ((fun (x : α) => (x, 1)) <$> x)

theorem WriterT.bind_def {m : Type u → Type v} [Monad m] {ω α β : Type u} [Monoid ω] (x : WriterT ω m α) (f : α → WriterT ω m β) : x >>= f = WriterT.mk do let x ← x.run match x with | (a, w₁) => (Prod.map id fun (x : ω) => w₁ * x) <$> f a

@[simp]

theorem WriterT.run_pure {m : Type u → Type v} [Monad m] {ω α : Type u} [Monoid ω] [LawfulMonad m] (x : α) : (pure x).run = pure (x, 1)

@[simp]

theorem WriterT.run_bind {m : Type u → Type v} [Monad m] {ω α β : Type u} [Monoid ω] [LawfulMonad m] (x : WriterT ω m α) (f : α → WriterT ω m β) : (x >>= f).run = do let x ← x.run match x with | (a, w₁) => (Prod.map id fun (x : ω) => w₁ * x) <$> (f a).run

@[simp]

theorem WriterT.run_seqLeft {m : Type u → Type v} [Monad m] {ω : Type u} [Monoid ω] {α β : Type u} (x : WriterT ω m α) (y : WriterT ω m β) : (x *> y).run = do let z ← x.run (Prod.map id fun (x : ω) => z.snd * x) <$> y.run

@[simp]

theorem WriterT.run_map {m : Type u → Type v} [Monad m] {ω α β : Type u} [Monoid ω] (x : WriterT ω m α) (f : α → β) : (f <$> x).run = Prod.map f id <$> x.run

@[simp]

theorem WriterT.run_monadLift' {m : Type u → Type v} [Monad m] {ω α : Type u} [EmptyCollection ω] (x : m α) : (monadLift x).run = (fun (x : α) => (x, ∅)) <$> x

theorem WriterT.liftM_def' {m : Type u → Type v} [Monad m] {ω α : Type u} [EmptyCollection ω] (x : m α) : liftM x = WriterT.mk ((fun (x : α) => (x, ∅)) <$> x)

theorem WriterT.monadLift_def' {m : Type u → Type v} [Monad m] {ω α : Type u} [EmptyCollection ω] (x : m α) : MonadLift.monadLift x = WriterT.mk ((fun (x : α) => (x, ∅)) <$> x)

theorem WriterT.bind_def' {m : Type u → Type v} [Monad m] {ω α β : Type u} [EmptyCollection ω] [Append ω] (x : WriterT ω m α) (f : α → WriterT ω m β) : x >>= f = WriterT.mk do let x ← x.run match x with | (a, w₁) => (Prod.map id fun (x : ω) => w₁ ++ x) <$> f a

@[simp]

theorem WriterT.run_pure' {m : Type u → Type v} [Monad m] {ω α : Type u} [EmptyCollection ω] [Append ω] [LawfulMonad m] (x : α) : (pure x).run = pure (x, ∅)

@[simp]

theorem WriterT.run_bind' {m : Type u → Type v} [Monad m] {ω α β : Type u} [EmptyCollection ω] [Append ω] [LawfulMonad m] (x : WriterT ω m α) (f : α → WriterT ω m β) : (x >>= f).run = do let x ← x.run match x with | (a, w₁) => (Prod.map id fun (x : ω) => w₁ ++ x) <$> (f a).run

@[simp]

theorem WriterT.run_seqLeft' {m : Type u → Type v} [Monad m] {ω : Type u} [Monoid ω] {α β : Type u} (x : WriterT ω m α) (y : WriterT ω m β) : (x *> y).run = do let z ← x.run (Prod.map id fun (x : ω) => z.snd * x) <$> y.run

@[simp]

theorem WriterT.run_map' {m : Type u → Type v} [Monad m] {ω α β : Type u} [EmptyCollection ω] [Append ω] (x : WriterT ω m α) (f : α → β) : (f <$> x).run = Prod.map f id <$> x.run

@[inline]

def WriterT.orElse {m : Type u → Type v} [AlternativeMonad m] {ω α : Type u} (x₁ : WriterT ω m α) (x₂ : Unit → WriterT ω m α) : WriterT ω m α

Equations

• x₁.orElse x₂ = WriterT.mk (x₁.run <|> (x₂ ()).run)

@[inline]

def WriterT.failure {m : Type u → Type v} [AlternativeMonad m] {ω α : Type u} : WriterT ω m α

Equations

• WriterT.failure = WriterT.mk failure

instance WriterT.instAlternativeMonadOfMonoid_toMathlib {m : Type u → Type v} [AlternativeMonad m] {ω : Type u} [Monoid ω] : AlternativeMonad (WriterT ω m)

Equations

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

@[simp]

theorem WriterT.run_failure {m : Type u → Type v} [AlternativeMonad m] {ω : Type u} [Monoid ω] {α : Type u} : failure.run = failure

instance WriterT.instLawfulMonadLiftOfLawfulMonad_toMathlib {m : Type u → Type v} [AlternativeMonad m] {ω : Type u} [Monoid ω] [LawfulMonad m] : LawfulMonadLift m (WriterT ω m)

AddWriterT: Additive Writer Monad Transformer

@[reducible, inline]

abbrev AddWriterT (ω : Type u) (M : Type u → Type v) (α : Type u) : Type v

Writer monad transformer with additive cost accumulation. Defined as WriterT (Multiplicative ω) M, which uses Monoid (Multiplicative ω) (derived from AddMonoid ω) so that tell accumulates via + with identity 0.

The types Multiplicative ω and ω are definitionally equal (Multiplicative is a plain def, not a structure), so no runtime wrapping occurs.

Equations

• AddWriterT ω M = WriterT (Multiplicative ω) M

def AddWriterT.addTell {ω : Type u} {M : Type u → Type v} [Monad M] [AddMonoid ω] (w : ω) : AddWriterT ω M PUnit.{u + 1}

Record an additive cost w in the writer log.

Equations

• AddWriterT.addTell w = tell (Multiplicative.ofAdd w)

@[simp]

theorem AddWriterT.run_addTell {ω : Type u} {M : Type u → Type v} [Monad M] [AddMonoid ω] (w : ω) : WriterT.run (addTell w) = pure (PUnit.unit, Multiplicative.ofAdd w)