Lexical Entry Types

Typed lexical entries for compositional semantics, polymorphic over an effect functor M ([BC24b]): an entry's denotation is an M-computation over its denotation domain. Scope-takers live at M = Cont R, CI items at M = Writer P. The default M := Id recovers the pure [HK98] case, so every existing call site reads unchanged; effectful lexicons supply an explicit M.

• LexEntry E W (M := Id) — a typed denotation over entity/index types E/W, carried by M
• Lexicon E W (M := Id) — string-keyed lookup of M-effectful entries
• Lexicon.lift — embed a pure lexicon into any effect via pure

structure Semantics.Montague.LexEntry (E W : Type) (M : Type → Type := Id) : Type

A typed lexical entry whose denotation carries the effect M (default Id = pure H&K).

• ty : Intensional.Ty
• denot : M (Intensional.Denot E W self.ty)

def Semantics.Montague.Lexicon (E W : Type) (M : Type → Type := Id) : Type

String-keyed lexicon of M-effectful entries (default Id).

Equations

• Semantics.Montague.Lexicon E W M = (String → Option (Semantics.Montague.LexEntry E W M))

def Semantics.Montague.Lexicon.lift {E W : Type} (M : Type → Type) [Pure M] (lex : Lexicon E W) : Lexicon E W M

Embed a pure lexicon into effect M by pure-lifting every entry.

Equations

• Semantics.Montague.Lexicon.lift M lex w = Option.map (fun (e : Semantics.Montague.LexEntry E W) => { ty := e.ty Id, denot := pure (e.denot Id) }) (lex w)