Applicative Functors in Natural Language Semantics

@cite{charlow-2018} @cite{mcbride-paterson-2008}

Three applicative functors — Reader, Set, and Cont — recur across natural language semantics. @cite{charlow-2018} shows they share a common algebraic structure (a type constructor F with ρ :: a → F a and ⊛ :: F(a → b) → F a → F b satisfying four laws), and that this structure is closed under composition.

Applicative	F a	ρ	⊛	Linguistic use
Reader E	E → a	λ_. x	λe. f e (x e)	Assignment-sensitivity
Set	a → Prop	{x}	{f x \| f ∈ m, x ∈ n}	Alternatives/Hamblin
Cont R	(a → R) → R	λκ. κ x	λκ. m(λf. n(λx. κ(f x)))	Scope-taking

Key results

1. Reader satisfies the four applicative functor laws (§3.3)
2. Composed applicatives F ∘ G are applicative (§3.3, all 4 laws)
3. Variable-free semantics (@cite{jacobson-1999}) = Reader Entity (§6)
4. Set applicative satisfies all 4 laws; Hamblin QuestionDen W = Cont Bool W definitionally (both (W → Bool) → Bool)
5. Cont applicative operations = Cont.pure/Cont.bind+Cont.map (§3.3)
6. Typed assignment family Gᵣ for intensional variables (§5)

Reader applicative

The Reader applicative for environment type E:

• F a := E → a
• ρ x := λ_. x (constant function)
• m ⊛ n := λe. m e (n e) (evaluate both at the same environment)

This is the foundation of assignment-sensitive composition (@cite{charlow-2018} §3.1–3.2). The four applicative functor laws hold definitionally.

def Semantics.Composition.Applicative.readerPure {E A : Type} (x : A) : E → A

ρ: lift a value into the Reader space (pure/return).

Equations

• Semantics.Composition.Applicative.readerPure x x✝ = x

def Semantics.Composition.Applicative.readerAp {E A B : Type} (f : E → A → B) (x : E → A) : E → B

⊛: compose two environment-dependent meanings (<*>/ap).

Equations

• Semantics.Composition.Applicative.readerAp f x e = f e (x e)

theorem Semantics.Composition.Applicative.reader_homomorphism {E A B : Type} (f : A → B) (x : A) : readerAp (readerPure f) (readerPure x) = readerPure (f x)

theorem Semantics.Composition.Applicative.reader_identity {E A : Type} (v : E → A) : readerAp (readerPure id) v = v

theorem Semantics.Composition.Applicative.reader_interchange {E A B : Type} (u : E → A → B) (y : A) : readerAp u (readerPure y) = readerAp (readerPure fun (f : A → B) => f y) u

theorem Semantics.Composition.Applicative.reader_composition {E A B C : Type} (u : E → B → C) (v : E → A → B) (w : E → A) : readerAp (readerAp (readerAp (readerPure Function.comp) u) v) w = readerAp u (readerAp v w)

Composed applicative functors

@cite{charlow-2018} §3.3, Fig 5: Given two applicative type constructors F and G, their composition F ∘ G is applicative. For Reader E₁ ∘ Reader E₂:

ρ_{F∘G}(x) = λe₁ λe₂. x
(m ⊛_{F∘G} n)(e₁)(e₂) = m e₁ e₂ (n e₁ e₂)

This closure property guarantees modularity: any two applicative-based analyses can be combined without additional machinery. Examples:

• G ∘ S: assignment-dependent sets of alternatives
• S ∘ G: alternative assignment-dependent meanings
• G ∘ G: doubly assignment-dependent meanings (§5, paycheck/reconstruction)

def Semantics.Composition.Applicative.composedPure {E₁ E₂ A : Type} (x : A) : E₁ → E₂ → A

Composed ρ for Reader E₁ ∘ Reader E₂.

Equations

• Semantics.Composition.Applicative.composedPure x x✝¹ x✝ = x

def Semantics.Composition.Applicative.composedAp {E₁ E₂ A B : Type} (f : E₁ → E₂ → A → B) (x : E₁ → E₂ → A) : E₁ → E₂ → B

Composed ⊛ for Reader E₁ ∘ Reader E₂.

Equations

• Semantics.Composition.Applicative.composedAp f x e₁ e₂ = f e₁ e₂ (x e₁ e₂)

theorem Semantics.Composition.Applicative.composed_homomorphism {E₁ E₂ A B : Type} (f : A → B) (x : A) : composedAp (composedPure f) (composedPure x) = composedPure (f x)

theorem Semantics.Composition.Applicative.composed_identity {E₁ E₂ A : Type} (v : E₁ → E₂ → A) : composedAp (composedPure id) v = v

theorem Semantics.Composition.Applicative.composed_interchange {E₁ E₂ A B : Type} (u : E₁ → E₂ → A → B) (y : A) : composedAp u (composedPure y) = composedAp (composedPure fun (f : A → B) => f y) u

theorem Semantics.Composition.Applicative.composed_composition {E₁ E₂ A B C : Type} (u : E₁ → E₂ → B → C) (v : E₁ → E₂ → A → B) (w : E₁ → E₂ → A) : composedAp (composedAp (composedAp (composedPure Function.comp) u) v) w = composedAp u (composedAp v w)

The Composition law — the fourth applicative functor law. Previously missing from the linglib formalization.

Variable-free semantics as Reader Entity

@cite{charlow-2018} §6: @cite{jacobson-1999}'s variable-free semantics treats pronouns as identity functions ⟦she⟧ := λx. x (type e → e). The composition apparatus is structurally identical to the assignment- sensitive version — readerPure and readerAp — with Entity as the environment type instead of assignments.

The paper's striking observation: composing the VF applicative with itself (Reader E ∘ Reader E) yields two-pronoun readings where the pronouns resolve independently. Uncurrying the result produces assignment-dependence "organically" (§6).

def Semantics.Composition.Applicative.vfPronoun {E : Type} : E → E

VF pronoun: the identity function ⟦she⟧ := λx. x.

Equations

• Semantics.Composition.Applicative.vfPronoun = id

theorem Semantics.Composition.Applicative.vf_she_left {E : Type} (left : E → Bool) : readerAp (readerPure left) vfPronoun = left

"She left" in VF: ρ(left) ⊛ she = left.

theorem Semantics.Composition.Applicative.vf_she_saw_her_single {E : Type} (saw : E → E → Bool) : readerAp (readerAp (readerPure saw) vfPronoun) vfPronoun = fun (e : E) => saw e e

"She saw her" with a single entity parameter: both pronouns resolve to the same entity, yielding λe. saw e e (reflexive reading).

theorem Semantics.Composition.Applicative.vf_she_saw_her_composed {E : Type} (saw : E → E → Bool) : (composedAp (composedAp (composedPure saw) fun (x e₂ : E) => e₂) fun (e₁ x : E) => e₁) = fun (e₁ e₂ : E) => saw e₂ e₁

"She saw her" with composed applicative (two entity parameters): the two pronouns resolve independently, yielding λx λy. saw y x. Assignment-dependence "springs organically into being" from uncurrying (@cite{charlow-2018} §6).

Set applicative

@cite{charlow-2018} §3.3 eqs (14)–(15): Alternative semantics of the @cite{hamblin-1973b} variety uses an applicative functor for sets:

S a := a → Prop
ρ x := {x}                          = `setPure`
m ⊛ n := {f x | f ∈ m, x ∈ n}      = `setAp`

A Hamblin question denotation (W → Bool) → Bool is definitionally Cont Bool W (both expand to (W → Bool) → Bool), connecting the Set and Cont perspectives.

def Semantics.Composition.Applicative.setPure {A : Type} (x : A) : A → Prop

Set ρ: the singleton set {x}.

Equations

• Semantics.Composition.Applicative.setPure x y = (y = x)

def Semantics.Composition.Applicative.setAp {A B : Type} (m : (A → B) → Prop) (n : A → Prop) : B → Prop

Set ⊛: pointwise function application across sets. {f x | f ∈ m, x ∈ n}

Equations

• Semantics.Composition.Applicative.setAp m n b = ∃ (f : A → B), m f ∧ ∃ (x : A), n x ∧ f x = b

theorem Semantics.Composition.Applicative.set_homomorphism {A B : Type} (f : A → B) (x : A) : setAp (setPure f) (setPure x) = setPure (f x)

Homomorphism: {f} ⊛ {x} = {f x}.

theorem Semantics.Composition.Applicative.set_identity {A : Type} (v : A → Prop) : setAp (setPure id) v = v

Identity: {id} ⊛ v = v.

theorem Semantics.Composition.Applicative.set_interchange {A B : Type} (u : (A → B) → Prop) (y : A) : setAp u (setPure y) = setAp (setPure fun (f : A → B) => f y) u

Interchange: u ⊛ {y} = {(fun f => f y)} ⊛ u.

theorem Semantics.Composition.Applicative.set_composition {A B C : Type} (u : (B → C) → Prop) (v : (A → B) → Prop) (w : A → Prop) : setAp (setAp (setAp (setPure Function.comp) u) v) w = setAp u (setAp v w)

Composition: {∘} ⊛ u ⊛ v ⊛ w = u ⊛ (v ⊛ w).

Continuation applicative

@cite{charlow-2018} §3.3 eqs (16)–(17): scope-taking expressions use the continuation applicative Cᵣ a := (a → r) → r. The operations are definitionally Cont.pure and the derived <*> from Core/Continuation.lean.

theorem Semantics.Composition.Applicative.cont_pure_eq {R A : Type} (x : A) : (fun (κ : A → R) => κ x) = Core.Continuation.Cont.pure x

Eq (16): ρ x := λκ. κ x = Cont.pure.

theorem Semantics.Composition.Applicative.cont_ap_eq {R A B : Type} (m : Core.Continuation.Cont R (A → B)) (n : Core.Continuation.Cont R A) : (fun (κ : B → R) => m fun (f : A → B) => n fun (x : A) => κ (f x)) = m.bind fun (f : A → B) => Core.Continuation.Cont.map f n

Eq (17): m ⊛ n := λκ. m(λf. n(λx. κ(f x))) = Cont <*>.

Typed assignment family Gᵣ

@cite{charlow-2018} §5.1: type-homogeneous assignments gᵣ := ℕ → r avoid consistency problems of a single polymorphic assignment type. Each type r gets its own assignment type:

• gₑ: maps indices to individuals
• g_{gₑ→e}: maps indices to individual concepts (intensions)

The composed applicative Gₑ ∘ G_{gₑ→e} handles paycheck pronouns without monadic join (§5.2): the paycheck pronoun reads an intension from the intension-assignment and evaluates it at the entity-assignment.

@[reducible, inline]

abbrev Semantics.Composition.Applicative.TypedAssignment (r : Type) : Type

Type-homogeneous assignment: maps indices to values of type r. Specializes to Core.Assignment E when r = E.

Equations

• Semantics.Composition.Applicative.TypedAssignment r = (Nat → r)

theorem Semantics.Composition.Applicative.typed_paycheck {E : Type} (likes : E → E → Bool) (mom : E → E) (bill : E) (j : Nat) (gᵢ : TypedAssignment (TypedAssignment E → E)) (gₑ : TypedAssignment E) (h_intension : gᵢ j = fun (h : TypedAssignment E) => mom (h 0)) (h_bill : gₑ 0 = bill) : composedAp (composedAp (composedPure likes) fun (gᵢ' : TypedAssignment (TypedAssignment E → E)) (gₑ' : TypedAssignment E) => gᵢ' j gₑ') (composedPure bill) gᵢ gₑ = likes (mom bill) bill

Self-contained paycheck derivation via composed Gₑ ∘ G_{gₑ→e}.

The intension-assignment gᵢ maps index j to the intension λh. mom(h 0) (= "his₀ mom"). The entity-assignment gₑ maps index 0 to Bill. The paycheck pronoun herⱼ reads from gᵢ and evaluates at gₑ, yielding mom(bill).

theorem Semantics.Composition.Applicative.typed_intension_is_rho_ap_pro {E : Type} (mom : E → E) : (readerAp (readerPure mom) fun (h : TypedAssignment E) => h 0) = fun (h : TypedAssignment E) => mom (h 0)

The intension λh. mom(h 0) is compositionally derived as ρ(mom) ⊛ pro₀ in the inner Gₑ applicative.