Writer Monad for Compositional Side-Effects

[GA12] [Sha01]

The Writer monad ⟨M, η, ⋆⟩ models meaning dimensions that accumulate side-effect information during compositional interpretation:

• M (the functor): maps a type A to paired values A × List P
• η (unit/pure): lifts a value with an empty log
• ⋆ (bind): sequences computations, combining their logs

The carrier is mathlib's Writer (List P) A (= WriterT (List P) Id A), whose Monad instance comes from mathlib's [EmptyCollection ω] [Append ω] instance for WriterT. This file adds the domain-named surface (Writer.mk/val/log/tell), projection simp lemmas, and the LawfulMonad instance for list logs.

This pattern unifies several linglib constructions:

Phenomenon	Value	Log
Conventional implicatures	at-issue content	CI propositions
Post-suppositions	DRS content	cardinality tests
Expressives	denotation	speaker attitude

The Writer monad enforces [Pot05]'s flow restriction structurally: bind's function argument receives only the value, never the log. At-issue content can flow into side-issue computations, but side-issue content cannot leak back into at-issue computation.

See Studies/Charlow2021.lean (PostSupp) for the same pattern applied to dynamic GQs, with the log monoid (Update S, dseq, test ⊤) in place of List P.

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

Construct a Writer computation from a value and a log.

Equations

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

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

The at-issue value of a Writer computation.

Equations

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

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

The accumulated side-effect log of a Writer computation.

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

def Writer.tell {P : Type u} (p : P) : Writer (List P) PUnit

tell (write): log a single item. Used by CI-contributing expressions to add propositions to the side-issue dimension; in [GA12]: write(t) = ⟨⊥, {t}⟩. (PUnit rather than Unit keeps it universe-polymorphic; at Type 0 they coincide.)

Equations

• Writer.tell p = Writer.mk PUnit.unit [p]

Projection lemmas for list logs

@[simp]

theorem Writer.val_pure {P A : Type u} (a : A) : (pure a).val = a

@[simp]

theorem Writer.log_pure {P A : Type u} (a : A) : (pure a).log = []

@[simp]

theorem Writer.val_bind {P A B : Type u} (m : Writer (List P) A) (f : A → Writer (List P) B) : (m >>= f).val = (f m.val).val

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Writer.log_tell {P : Type u} (p : P) : (tell p).log = [p]

Monad laws

The Monad (Writer (List P)) instance is mathlib's [EmptyCollection ω] [Append ω] instance for WriterT; the laws hold because (List P, ++, []) is a monoid.

instance Writer.instLawfulMonadList_linglib {P : Type u} : LawfulMonad (Writer (List P))

Log monotonicity

theorem Writer.log_grows {P A B : Type u} (m : Writer (List P) A) (f : A → Writer (List P) B) : ∃ (suffix : List P), (m >>= f).log = m.log ++ suffix

The log only grows: bind's output log extends the input log.

theorem Writer.tell_persists {P A B : Type u} (m : Writer (List P) A) (f : A → Writer (List P) B) (p : P) (h : p ∈ m.log) : p ∈ (m >>= f).log

Side-effects are permanent: once logged, an item stays in the log.