Writer monads for side-issue meaning

A computation of the writer monad Writer ω yields a value and logs output in ω. Giorgolo and Asudeh model conventional implicature this way, in Shan's monadic program: the value of an expression is its at-issue content, the log collects the side-issue propositions of its parts, pure logs nothing and bind appends the logs. Forgetting the log is a monad morphism to Id, and bind only extends the log, so content flows from the at-issue dimension into the side-issue one and never back.

Main definitions

• Writer.val, Writer.log: the value and the log of a computation.
• WriterT.instLawfulMonadList: the monad laws for list logs, over any lawful monad.

Main results

• Writer.val_pure, Writer.val_bind: forgetting the log is a monad morphism.
• Writer.log_prefix_bind: the log of m is a prefix of the log of m >>= f.

Implementation notes

• Mathlib's two Monad instances on Writer ω, for [Monoid ω] and for [EmptyCollection ω] [Append ω], are both WriterT.monad empty append; the projection lemmas are stated for that monad, as mathlib states WriterT.run_bind, and apply under either.
• Mathlib proves the monad laws for monoid logs only, and lists are not a monoid there.
• Giorgolo and Asudeh take the log to be a monoid of propositions and fix it to sets under union. They require the arrows to be isotone in the log for the preorder x ≤ y ↔ ∃ z, x * z = y, which is x ∣ y in mathlib. The consumers here log lists, the free monoid, on which this preorder is the prefix order.

References

• [GA12]
• [Sha01]

instance WriterT.instLawfulMonadList {M : Type u → Type v} {P : Type u} [Monad M] [LawfulMonad M] : LawfulMonad (WriterT (List P) M)

A writer monad with list logs is lawful over any lawful monad.

def Writer.mk {ω A : Type u} (a : A) (w : ω) : Writer ω A

Writer.mk a w is the computation with value a and log w.

Equations

• Writer.mk a w = WriterT.mk (a, w)

def Writer.val {ω A : Type u} (m : Writer ω A) : A

The value of a computation is the first component of its run.

Equations

• m.val = (WriterT.run m).fst

def Writer.log {ω A : Type u} (m : Writer ω A) : ω

The log of a computation is the second component of its run.

Equations

• m.log = (WriterT.run m).snd

theorem Writer.ext {ω A : Type u} {m₁ m₂ : Writer ω A} (hv : m₁.val = m₂.val) (hl : m₁.log = m₂.log) : m₁ = m₂

theorem Writer.ext_iff {ω A : Type u} {m₁ m₂ : Writer ω A} : m₁ = m₂ ↔ m₁.val = m₂.val ∧ m₁.log = m₂.log

@[simp]

theorem Writer.val_mk {ω A : Type u} (a : A) (w : ω) : (Writer.mk a w).val = a

@[simp]

theorem Writer.log_mk {ω A : Type u} (a : A) (w : ω) : (Writer.mk a w).log = w

@[simp]

theorem Writer.val_tell {ω : Type u} (w : ω) : (tell w).val = PUnit.unit

@[simp]

theorem Writer.log_tell {ω : Type u} (w : ω) : (tell w).log = w

@[simp]

theorem Writer.val_pure {ω A : Type u} (empty : ω) (append : ω → ω → ω) (a : A) : (pure a).val = a

@[simp]

theorem Writer.log_pure {ω A : Type u} (empty : ω) (append : ω → ω → ω) (a : A) : (pure a).log = empty

@[simp]

theorem Writer.val_bind {ω A B : Type u} (empty : ω) (append : ω → ω → ω) (m : Writer ω A) (f : A → Writer ω B) : (m >>= f).val = (f m.val).val

The value of m >>= f is the value of f at the value of m, so the log of m never reaches it.

@[simp]

theorem Writer.log_bind {ω A B : Type u} (empty : ω) (append : ω → ω → ω) (m : Writer ω A) (f : A → Writer ω B) : (m >>= f).log = append m.log (f m.val).log

@[simp]

theorem Writer.val_map {ω A B : Type u} (empty : ω) (append : ω → ω → ω) (f : A → B) (m : Writer ω A) : (f <$> m).val = f m.val

@[simp]

theorem Writer.log_map {ω A B : Type u} (empty : ω) (append : ω → ω → ω) (f : A → B) (m : Writer ω A) : (f <$> m).log = m.log

@[simp]

theorem Writer.val_seq {ω A B : Type u} (empty : ω) (append : ω → ω → ω) (f : Writer ω (A → B)) (m : Writer ω A) : (f <*> m).val = f.val m.val

@[simp]

theorem Writer.log_seq {ω A B : Type u} (empty : ω) (append : ω → ω → ω) (f : Writer ω (A → B)) (m : Writer ω A) : (f <*> m).log = append f.log m.log

theorem Writer.log_prefix_bind {A B P : Type u} (m : Writer (List P) A) (f : A → Writer (List P) B) : m.log <+: (m >>= f).log

The log of m >>= f extends the log of m, so composition is isotone for the prefix order on list logs.