Writer Monad for Compositional Side-Effects

@cite{giorgolo-asudeh-2012} @cite{shan-2001}

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

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 @cite{potts-2005}'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 PostSuppositional.lean for the same pattern applied to dynamic GQs.

structure Semantics.Composition.WriterMonad.Writer (P : Type u_1) (A : Type u_2) : Type (max u_1 u_2)

The Writer monad: a value paired with an accumulated log.

In @cite{giorgolo-asudeh-2012}'s notation, Writer P A is M(A), where the second component is a collection of logged items of type P, represented as a List for computability.

• val : A

  The at-issue value

• log : List P

  Accumulated side-effect log

theorem Semantics.Composition.WriterMonad.Writer.ext {P : Type u_1} {A : Type u_2} {m₁ m₂ : Writer P A} (hv : m₁.val = m₂.val) (hl : m₁.log = m₂.log) : m₁ = m₂

theorem Semantics.Composition.WriterMonad.Writer.ext_iff {P : Type u_1} {A : Type u_2} {m₁ m₂ : Writer P A} : m₁ = m₂ ↔ m₁.val = m₂.val ∧ m₁.log = m₂.log

def Semantics.Composition.WriterMonad.Writer.pure {P : Type u_1} {A : Type u_2} (a : A) : Writer P A

η (unit): lift a pure value with an empty log.

Ordinary lexical items are η-lifted: ⟦john⟧ = η(j), ⟦likes⟧ = η(λyλx.like(x,y))

Equations

• Semantics.Composition.WriterMonad.Writer.pure a = { val := a, log := [] }

def Semantics.Composition.WriterMonad.Writer.bind {P : Type u_1} {A : Type u_2} {B : Type u_3} (m : Writer P A) (f : A → Writer P B) : Writer P B

⋆ (bind): sequence computations, combining logs.

⟨x, P⟩ ⋆ f = ⟨π₁(f x), P ++ π₂(f x)⟩

The function f receives only the value x, not the log P. This enforces @cite{potts-2005}'s restriction: side-issue content (in the log) is invisible to subsequent at-issue computation.

Equations

• m.bind f = { val := (f m.val).val, log := m.log ++ (f m.val).log }

def Semantics.Composition.WriterMonad.Writer.map {P : Type u_1} {A : Type u_2} {B : Type u_3} (f : A → B) (m : Writer P A) : Writer P B

map: apply a function to the value, preserving the log.

Equations

• Semantics.Composition.WriterMonad.Writer.map f m = { val := f m.val, log := m.log }

def Semantics.Composition.WriterMonad.Writer.tell {P : Type u_1} (p : P) : Writer P Unit

tell (write): log a single item.

Used by CI-contributing expressions to add propositions to the side-issue dimension. In @cite{giorgolo-asudeh-2012}: write(t) = ⟨⊥, {t}⟩

Equations

• Semantics.Composition.WriterMonad.Writer.tell p = { val := (), log := [p] }

def Semantics.Composition.WriterMonad.Writer.app {P : Type u_1} {A : Type u_2} {B : Type u_3} (mf : Writer P (A → B)) (mx : Writer P A) : Writer P B

Monadic application (⊸-elimination in Glue).

A(f)(x) = f ⋆ λg. x ⋆ λy. η(g y)

Both function and argument may carry side-effects; all side-effects are combined in the result.

Equations

• mf.app mx = mf.bind fun (f : A → B) => mx.bind fun (x : A) => Semantics.Composition.WriterMonad.Writer.pure (f x)

@[simp]

theorem Semantics.Composition.WriterMonad.Writer.pure_val {P : Type u_1} {A : Type u_2} (a : A) : (pure a).val = a

@[simp]

theorem Semantics.Composition.WriterMonad.Writer.pure_log {P : Type u_1} {A : Type u_2} (a : A) : (pure a).log = []

@[simp]

theorem Semantics.Composition.WriterMonad.Writer.bind_val {P : Type u_1} {A : Type u_2} {B : Type u_3} (m : Writer P A) (f : A → Writer P B) : (m.bind f).val = (f m.val).val

@[simp]

theorem Semantics.Composition.WriterMonad.Writer.bind_log {P : Type u_1} {A : Type u_2} {B : Type u_3} (m : Writer P A) (f : A → Writer P B) : (m.bind f).log = m.log ++ (f m.val).log

@[simp]

theorem Semantics.Composition.WriterMonad.Writer.tell_val {P : Type u_1} (p : P) : (tell p).val = ()

@[simp]

theorem Semantics.Composition.WriterMonad.Writer.tell_log {P : Type u_1} (p : P) : (tell p).log = [p]

@[simp]

theorem Semantics.Composition.WriterMonad.Writer.map_val {P : Type u_1} {A : Type u_2} {B : Type u_3} (f : A → B) (m : Writer P A) : (map f m).val = f m.val

@[simp]

theorem Semantics.Composition.WriterMonad.Writer.map_log {P : Type u_1} {A : Type u_2} {B : Type u_3} (f : A → B) (m : Writer P A) : (map f m).log = m.log

theorem Semantics.Composition.WriterMonad.Writer.bind_pure_left {P : Type u_1} {A : Type u_2} {B : Type u_3} (a : A) (f : A → Writer P B) : (pure a).bind f = f a

Left identity: η(a) ⋆ f = f a

theorem Semantics.Composition.WriterMonad.Writer.bind_pure_right {P : Type u_1} {A : Type u_2} (m : Writer P A) : m.bind pure = m

Right identity: m ⋆ η = m

theorem Semantics.Composition.WriterMonad.Writer.bind_assoc {P : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} (m : Writer P A) (f : A → Writer P B) (g : B → Writer P C) : (m.bind f).bind g = m.bind fun (a : A) => (f a).bind g

Associativity: (m ⋆ f) ⋆ g = m ⋆ (λa. f a ⋆ g)

theorem Semantics.Composition.WriterMonad.Writer.log_grows {P : Type u_1} {A : Type u_2} {B : Type u_3} (m : Writer P A) (f : A → Writer P B) : ∃ (suffix : List P), (m.bind f).log = m.log ++ suffix

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

theorem Semantics.Composition.WriterMonad.Writer.tell_persists {P : Type u_1} {A : Type u_2} {B : Type u_3} (m : Writer P A) (f : A → Writer P B) (p : P) (h : p ∈ m.log) : p ∈ (m.bind f).log

Side-effects are permanent: once logged, a proposition stays in the log.