Bumford and Charlow 2026: effect-driven interpretation

[BC26f] treat pronouns, antecedents, indefinites and quantifiers as computations with effects, and the modes of semantic combination as higher-order operations that lift a basic combinator through the algebra of an effect: maps for functors (chapter 2), structured application for applicatives (chapter 3), join for monads (chapter 4), and co-unit and eject for adjunctions (chapter 5). This file states the modes over Lean's Functor, Applicative and Monad classes and mathlib's adjunctions, and proves the results of chapter 5 about them.

A pronoun reads a referent and an antecedent stores one. Storing is left adjoint to reading, with currying as the hom-equivalence, and the co-unit mode cancels the two effects, so a sentence whose pronouns are bound denotes a pure value. The co-unit mode takes the left adjoint from the left daughter, so an antecedent must precede the pronoun it binds however the scopes are inverted: this is crossover, proved here over the book's type-driven grammar.

Every right adjoint on types distributes over function types, and the eject modes use this. With them the grammar derives, with no new machinery, the bind of the reader transformer, the bind of the monad that any adjunction induces, which for storing and reading is Lean's state monad, and, with indeterminacy in between, the state transformer over sets that dynamic semantics is built on.

Main definitions

• mapL, mapR, structuredApp, joinMode: the map, structured application and join modes
• Output, outputInput: the storing effect W and the adjunction W ⊣ R
• counitMode, eject, ejectL, ejectR: the modes an adjunction adds
• Ty, Eff, Combine: the type-driven grammar of the book's Appendix B

Main results

• joinMode_mapL_ba, joinMode_mapR_fa: join at the map modes is bind
• mapL_ejectR_counitMode: the bind of the monad of any adjunction is a mode of combination
• mapL_ejectR_counitMode_outputInput, mapL_joinMode_mapL_ejectR_counitMode: the state monad and the state transformer come from W ⊣ R
• ejectL_structuredApp_joinMode_mapR: the reader transformer comes from ejection
• Combine.reads: crossover

Implementation notes

The storing effect Output ι α = α × ι is a functor and not mathlib's WriterT, whose functor comes only with a monad over a monoid of logs. A single stored referent cannot be merged with another, which is the book's reason that this W is not a monad (section 5.3.4). The supplement effect, whose log is a monoid, is Composition/Writer.lean.

The modes act on Lean's type constructors; an adjunction is mathlib's Adjunction between the corresponding functors ofTypeFunctor Ω ⊣ ofTypeFunctor Γ, so the unit, co-unit and induced monad are mathlib's. The grammar's Ty has computation types comp f a, which Montague.Ty lacks: that engine runs every node in one effect, where the book's grammar tracks a stack of effects per node. As in Appendix B, a writer is applicative exactly when its datum is t, every applicative effect of the grammar is monadic, and the only adjunction is W i ⊣ R i. Base types are e and t.

The Element is forthcoming; equation, section and appendix locators are to the arXiv version of April 2025.

TODO

• Islands (section 5.4): the book filters the results at an island node by a predicate on their types; the grammar here has no syntax trees.
• The denotations of derivations, the book's interpreter of section 5.5: Combine is a Prop, and the interpreter would be a type-valued version with a denotation for each rule.

References

• [BC26f]
• [BS14]

Modes of combination

A mode of combination takes a basic combinator (∗) : σ → τ → ω and returns one that works when a daughter carries an effect.

def BumfordCharlow2026.fa {α β : Type u} (f : α → β) (x : α) : β

Forward application (>).

Equations

• BumfordCharlow2026.fa f x = f x

def BumfordCharlow2026.ba {α β : Type u} (x : α) (f : α → β) : β

Backward application (<).

Equations

• BumfordCharlow2026.ba x f = f x

def BumfordCharlow2026.mapL {σ τ ω : Type u} {F : Type u → Type v} [Functor F] (star : σ → τ → ω) (e₁ : F σ) (e₂ : τ) : F ω

Map Left F̄ (2.17a): map the combinator over an effectful left daughter.

Equations

• BumfordCharlow2026.mapL star e₁ e₂ = (fun (a : σ) => star a e₂) <$> e₁

def BumfordCharlow2026.mapR {σ τ ω : Type u} {F : Type u → Type v} [Functor F] (star : σ → τ → ω) (e₁ : σ) (e₂ : F τ) : F ω

Map Right F̃ (2.17b): map the combinator over an effectful right daughter.

Equations

• BumfordCharlow2026.mapR star e₁ e₂ = (fun (b : τ) => star e₁ b) <$> e₂

theorem BumfordCharlow2026.mapR_fa {α β : Type u} {F : Type u → Type v} [Functor F] (f : α → β) (x : F α) : mapR fa f x = f <$> x

F̃(>) and F̄(<) are the functor's map (2.18).

theorem BumfordCharlow2026.mapL_ba {α β : Type u} {F : Type u → Type v} [Functor F] (x : F α) (f : α → β) : mapL ba x f = f <$> x

theorem BumfordCharlow2026.mapR_mapR_fa {α β : Type u} {F : Type u → Type v} [Functor F] {G : Type u → Type u} [Functor G] (f : α → β) (x : F (G α)) : mapR (mapR fa) f x = (f <$> Functor.Comp.mk x).run

F̃(F̃ >) is the map of the composite functor (2.24): functors compose.

def BumfordCharlow2026.structuredApp {σ τ ω : Type u} {F : Type u → Type v} [Applicative F] (star : σ → τ → ω) (e₁ : F σ) (e₂ : F τ) : F ω

Structured Application A (3.10): combine two daughters carrying the same applicative effect, merging the effects.

Equations

• BumfordCharlow2026.structuredApp star e₁ e₂ = pure star <*> e₁ <*> e₂

theorem BumfordCharlow2026.structuredApp_fa {α β : Type u} {F : Type u → Type v} [Applicative F] [LawfulApplicative F] (f : F (α → β)) (x : F α) : structuredApp fa f x = f <*> x

Structured application at forward application is the applicative's <*>.

def BumfordCharlow2026.joinMode {σ τ ω : Type u} {M : Type u → Type u} [Monad M] (star : σ → τ → M (M ω)) (e₁ : σ) (e₂ : τ) : M ω

Join J (4.22): flatten the doubled effect a combinator returns, J(∗) E₁ E₂ := μ(E₁ ∗ E₂).

Equations

• BumfordCharlow2026.joinMode star e₁ e₂ = joinM (star e₁ e₂)

theorem BumfordCharlow2026.joinMode_mapL_ba {α β : Type u} {M : Type u → Type u} [Monad M] [LawfulMonad M] (m : M α) (k : α → M β) : joinMode (mapL ba) m k = m >>= k

J(F̄ <) is bind (after (4.22)).

theorem BumfordCharlow2026.joinMode_mapR_fa {α β : Type u} {M : Type u → Type u} [Monad M] [LawfulMonad M] (k : α → M β) (m : M α) : joinMode (mapR fa) k m = m >>= k

J(F̃ >) is bind with its arguments flipped, the book's (=>>) (after (4.22)).

Storing and reading

A pronoun reads a referent from its context, R α = ι → α (5.1a), and an antecedent stores its referent alongside its value, W α = α × ι (5.1b). Functions out of W α are functions into R β by currying (5.3), which makes W left adjoint to R.

def BumfordCharlow2026.Output (ι α : Type u) : Type u

The storing effect W: a value paired with a stored datum.

Equations

• BumfordCharlow2026.Output ι α = (α × ι)

def BumfordCharlow2026.Output.map {ι α β : Type u} (f : α → β) (p : Output ι α) : Output ι β

Map the value, keeping the stored datum.

Equations

• BumfordCharlow2026.Output.map f p = (f p.1, p.2)

@[instance_reducible]

instance BumfordCharlow2026.Output.functor {ι : Type u} : Functor (Output ι)

Equations

• BumfordCharlow2026.Output.functor = { map := fun {α β : Type ?u.1} => BumfordCharlow2026.Output.map }

instance BumfordCharlow2026.Output.lawfulFunctor {ι : Type u} : LawfulFunctor (Output ι)

def BumfordCharlow2026.store {ι : Type u} (x : ι) : Output ι ι

The antecedent operator ⊲ (5.1b): an entity stores itself.

Equations

• BumfordCharlow2026.store x = (x, x)

def BumfordCharlow2026.pronoun {ι : Type u} : ReaderM ι ι

The pronoun (5.1a): read the referent.

Equations

• BumfordCharlow2026.pronoun i = i

def BumfordCharlow2026.outputInput (ι : Type u) : CategoryTheory.ofTypeFunctor (Output ι) ⊣ CategoryTheory.ofTypeFunctor (ReaderM ι)

Storing is left adjoint to reading (5.3): the hom-equivalence Φ is currying.

Equations

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

theorem BumfordCharlow2026.outputInput_homEquiv_apply {ι α β : Type u} (f : Output ι α ⟶ β) (a : α) (x : ι) : (CategoryTheory.ConcreteCategory.hom (((outputInput ι).homEquiv α β) f)) a x = (CategoryTheory.ConcreteCategory.hom f) (a, x)

theorem BumfordCharlow2026.outputInput_unit_app {ι α : Type u} (a : α) (x : ι) : (CategoryTheory.ConcreteCategory.hom ((outputInput ι).unit.app α)) a x = (a, x)

The unit and co-unit of W ⊣ R (5.4): η a = λx. ⟨a, x⟩ and ε ⟨f, x⟩ = f x.

theorem BumfordCharlow2026.outputInput_counit_app {ι α : Type u} (f : ReaderM ι α) (x : ι) : (CategoryTheory.ConcreteCategory.hom ((outputInput ι).counit.app α)) (f, x) = f x

The co-unit mode

For any adjunction Ω ⊣ Γ, the co-unit mode maps the combinator over both daughters and applies the co-unit to the result.

def BumfordCharlow2026.counitMode {Ω Γ : Type u → Type u} [Functor Ω] [LawfulFunctor Ω] [Functor Γ] [LawfulFunctor Γ] (adj : CategoryTheory.ofTypeFunctor Ω ⊣ CategoryTheory.ofTypeFunctor Γ) {σ τ ω : Type u} (star : σ → τ → ω) (e₁ : Ω σ) (e₂ : Γ τ) : ω

The co-unit mode C (5.8): C(∗) E₁ E₂ := ε((λl. (λr. l ∗ r) • E₂) • E₁). It takes the left adjoint from the left daughter and the right adjoint from the right one.

Equations

• BumfordCharlow2026.counitMode adj star e₁ e₂ = (CategoryTheory.ConcreteCategory.hom (adj.counit.app ω)) ((fun (l : σ) => (fun (r : τ) => star l r) <$> e₂) <$> e₁)

theorem BumfordCharlow2026.counitMode_outputInput {ι σ τ ω : Type u} (star : σ → τ → ω) (p : Output ι σ) (r : ReaderM ι τ) : counitMode (outputInput ι) star p r = star p.1 (r p.2)

Under W ⊣ R the co-unit mode feeds the stored datum to the reader.

def BumfordCharlow2026.eject {α β : Type u} {Ω Γ : Type u → Type u} [Functor Ω] [LawfulFunctor Ω] [Functor Γ] [LawfulFunctor Γ] (adj : CategoryTheory.ofTypeFunctor Ω ⊣ CategoryTheory.ofTypeFunctor Γ) : (α → Γ β) ≃ Γ (α → β)

Eject Υ (5.24): for a right adjoint Γ on types, functions into Γ β are Γ of functions.

Equations

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

theorem BumfordCharlow2026.eject_outputInput {ι α β : Type u} (k : α → ReaderM ι β) : (eject (outputInput ι)) k = fun (i : ι) (a : α) => k a i

For the reader, eject swaps the arguments (5.22).

def BumfordCharlow2026.ejectL {Ω Γ : Type u → Type u} [Functor Ω] [LawfulFunctor Ω] [Functor Γ] [LawfulFunctor Γ] (adj : CategoryTheory.ofTypeFunctor Ω ⊣ CategoryTheory.ofTypeFunctor Γ) {σ σ' τ υ : Type u} (star : Γ (σ → σ') → τ → υ) (e₁ : σ → Γ σ') (e₂ : τ) : υ

Eject Left (5.25a): eject the effect of a left daughter that is a function into a right adjoint.

Equations

• BumfordCharlow2026.ejectL adj star e₁ e₂ = star ((BumfordCharlow2026.eject adj) e₁) e₂

def BumfordCharlow2026.ejectR {Ω Γ : Type u → Type u} [Functor Ω] [LawfulFunctor Ω] [Functor Γ] [LawfulFunctor Γ] (adj : CategoryTheory.ofTypeFunctor Ω ⊣ CategoryTheory.ofTypeFunctor Γ) {σ τ τ' υ : Type u} (star : σ → Γ (τ → τ') → υ) (e₁ : σ) (e₂ : τ → Γ τ') : υ

Eject Right (5.25b).

Equations

• BumfordCharlow2026.ejectR adj star e₁ e₂ = star e₁ ((BumfordCharlow2026.eject adj) e₂)

theorem BumfordCharlow2026.counitMode_ba_eject {α β : Type u} {Ω Γ : Type u → Type u} [Functor Ω] [LawfulFunctor Ω] [Functor Γ] [LawfulFunctor Γ] (adj : CategoryTheory.ofTypeFunctor Ω ⊣ CategoryTheory.ofTypeFunctor Γ) (a : Ω α) (k : α → Γ β) : counitMode adj ba a ((eject adj) k) = (CategoryTheory.ConcreteCategory.hom (adj.counit.app β)) (k <$> a)

theorem BumfordCharlow2026.mapL_ejectR_counitMode {α β : Type u} {Ω Γ : Type u → Type u} [Functor Ω] [LawfulFunctor Ω] [Functor Γ] [LawfulFunctor Γ] (adj : CategoryTheory.ofTypeFunctor Ω ⊣ CategoryTheory.ofTypeFunctor Γ) (m : Γ (Ω α)) (k : α → Γ (Ω β)) : mapL (ejectR adj (counitMode adj ba)) m k = (CategoryTheory.ConcreteCategory.hom (adj.toMonad.μ.app β)) ((CategoryTheory.ConcreteCategory.hom (adj.toMonad.map (TypeCat.ofHom k))) m)

Every adjunction gives rise to a monad through the grammar (section 5.3.4): the mode F̄ ® C < is the bind of the monad Γ Ω the adjunction induces.

Monads from storing and reading

theorem BumfordCharlow2026.mapL_ejectR_counitMode_outputInput {ι α β : Type u} (m : StateM ι α) (k : α → StateM ι β) : mapL (ejectR (outputInput ι) (counitMode (outputInput ι) ba)) m k = m >>= k

The state monad is the monad of W ⊣ R, and its bind is F̄ ® C < (5.37), (5.38).

theorem BumfordCharlow2026.mapL_joinMode_mapL_ejectR_counitMode {ι α β : Type u} {M : Type u → Type u} [Monad M] [LawfulMonad M] (m : StateT ι M α) (k : α → StateT ι M β) : mapL (joinMode (mapL (ejectR (outputInput ι) (counitMode (outputInput ι) ba)))) m k = m >>= k

With a monad in between, F̄ J F̄ ® C < is the bind of the state transformer (5.39); over sets this is the monad of dynamic semantics.

theorem BumfordCharlow2026.ejectL_structuredApp_joinMode_mapR {ι α β : Type u} {M : Type u → Type u} [Monad M] [LawfulMonad M] (m : ReaderT ι M α) (k : α → ReaderT ι M β) : ejectL (outputInput ι) (structuredApp (joinMode (mapR fa))) k m = m >>= k

Ejecting the reader from a function into it, ® A J F̃ > is the bind of the reader transformer (5.28), (5.29).

The type-driven grammar

Appendix B implements the grammar as a function from the types of two daughters to the modes that combine them and the types they yield. Combine l r u says that some mode combines a left daughter of type l with a right daughter of type r into a result of type u.

inductive BumfordCharlow2026.Ty : Type

The types of the grammar.

• e : Ty
• t : Ty
• fn (a b : Ty) : Ty
• comp (f : Eff) (a : Ty) : Ty

  A computation with effect f and value type a.

inductive BumfordCharlow2026.Eff : Type

The effects of the grammar.

• S : Eff

  Indeterminacy.

• R (i : Ty) : Eff

  Reading a datum of type i.

• W (o : Ty) : Eff

  Storing a datum of type o.

• C (r : Ty) : Eff

  Quantifying over contexts with result type r.

def BumfordCharlow2026.Eff.IsApplicative : Eff → Prop

An effect is applicative, and then also monadic, unless it stores something other than a truth value, since only t is a monoid.

Equations

• (BumfordCharlow2026.Eff.W o).IsApplicative = (o = BumfordCharlow2026.Ty.t)
• x✝.IsApplicative = True

def BumfordCharlow2026.Eff.Adjoint : Eff → Eff → Prop

f ⊣ g: storing a datum is left adjoint to reading one of the same type, which is outputInput.

Equations

• (BumfordCharlow2026.Eff.W o).Adjoint (BumfordCharlow2026.Eff.R i) = (o = i)
• x✝¹.Adjoint x✝ = False

def BumfordCharlow2026.Eff.IsRightAdjoint (g : Eff) : Prop

g has a left adjoint.

Equations

• g.IsRightAdjoint = ∃ (f : BumfordCharlow2026.Eff), f.Adjoint g

def BumfordCharlow2026.Eff.IsReader : Eff → Prop

The reading effects.

Equations

• (BumfordCharlow2026.Eff.R i).IsReader = True
• x✝.IsReader = False

theorem BumfordCharlow2026.Eff.not_isReader_of_adjoint {f g : Eff} (h : f.Adjoint g) : ¬f.IsReader

inductive BumfordCharlow2026.Binary : Ty → Ty → Ty → Prop

The binary modes: the basic combinators and the higher-order modes of Figure 10.

• fa {a b : Ty} : Binary (a.fn b) a b
• ba {a b : Ty} : Binary a (a.fn b) b
• pm {a : Ty} : Binary (a.fn Ty.t) (a.fn Ty.t) (a.fn Ty.t)
• mapR {l r u : Ty} {f : Eff} : Combine l r u → Binary l (Ty.comp f r) (Ty.comp f u)
• mapL {l r u : Ty} {f : Eff} : Combine l r u → Binary (Ty.comp f l) r (Ty.comp f u)
• app {l r u : Ty} {f : Eff} : f.IsApplicative → Combine l r u → Binary (Ty.comp f l) (Ty.comp f r) (Ty.comp f u)
• unitR {l l' r u : Ty} {f : Eff} : f.IsApplicative → Combine (l.fn l') r u → Binary ((Ty.comp f l).fn l') r u
• unitL {l r r' u : Ty} {f : Eff} : f.IsApplicative → Combine l (r.fn r') u → Binary l ((Ty.comp f r).fn r') u
• counit {l r u : Ty} {f g : Eff} : f.Adjoint g → Combine l r u → Binary (Ty.comp f l) (Ty.comp g r) u
• ejectR {l r r' u : Ty} {g : Eff} : g.IsRightAdjoint → Combine l (Ty.comp g (r.fn r')) u → Binary l (r.fn (Ty.comp g r')) u
• ejectL {l l' r u : Ty} {g : Eff} : g.IsRightAdjoint → Combine (Ty.comp g (l.fn l')) r u → Binary (l.fn (Ty.comp g l')) r u

inductive BumfordCharlow2026.Combine : Ty → Ty → Ty → Prop

The book's combine: a binary mode, possibly followed by a join or a closure.

• bin {l r u : Ty} : Binary l r u → Combine l r u
• join {l r a : Ty} {f : Eff} : f.IsApplicative → Binary l r (Ty.comp f (Ty.comp f a)) → Combine l r (Ty.comp f a)
• lower {l r a : Ty} : Binary l r (Ty.comp (Eff.C a) a) → Combine l r a

def BumfordCharlow2026.Ty.Reads : Ty → Prop

The type still requests a datum: a reading effect at a strictly positive position.

Equations

• (a.fn b).Reads = b.Reads
• (BumfordCharlow2026.Ty.comp f a).Reads = (f.IsReader ∨ a.Reads)
• x✝.Reads = False

def BumfordCharlow2026.Ty.InputFree : Ty → Prop

No reading effect anywhere in the type.

Equations

• (a.fn b).InputFree = (a.InputFree ∧ b.InputFree)
• (BumfordCharlow2026.Ty.comp f a).InputFree = (¬f.IsReader ∧ a.InputFree)
• x✝.InputFree = True

theorem BumfordCharlow2026.Ty.InputFree.not_reads {a : Ty} : a.InputFree → ¬a.Reads

theorem BumfordCharlow2026.Binary.reads {l r u : Ty} : Binary l r u → l.Reads → r.InputFree → u.Reads

theorem BumfordCharlow2026.Combine.reads {l r u : Ty} : Combine l r u → l.Reads → r.InputFree → u.Reads

Crossover (section 5.2): a left daughter that reads, combined with a right daughter that reads nothing, yields a type that still reads, whatever the modes. Only the co-unit mode removes a reading effect, and it takes the reader from the right daughter.