Skip to content

Denotational Semantics of Compositional Effects

QVR layers monadic and applicative effects over the residuated category universe through two parallel typeclass towers (monads and arrows) and a class-driven schema-lifting system. This page assigns denotations to these constructs and proves that they conservatively extend the bare deduction fragment of Weighted Deduction Fragment.

1. Setting

We work in the V-enriched semantic universe of Setting and Notation. For an effect-typed parser we fix:

  • A residuated category universe \(\mathcal{C}\) realized as a finite set \(\llbracket \mathrm{Cat} \rrbracket\). The carrier is built by the FreeResiduated(generators, depth, ops) object class: starting from a finite alphabet of atomic categories, it freely closes the carrier under the constructors ops (which include the residuation slashes \(/\) and \(\backslash\), the monoidal product \(\otimes\), and the diamond modality \(\diamondsuit\)) up to a finite depth bound, yielding a finite-set object whose elements are the well-formed category expressions of bounded complexity.
  • A finite list of declared effects \(T_1, \dots, T_n\), each registered against one or more typeclass ABCs: Functor, Applicative, Monad, Alternative, MonadPlus, Traversable, ArrowApply, or ArrowLoop.

The effect-typed category universe is

\[ \widehat{\mathcal{C}} \;=\; \mathcal{C} \times \mathrm{EffectStack}_{\le d}(T_1, \dots, T_n), \]

where \(\mathrm{EffectStack}_{\le d}\) is the set of finite stacks of effects of length at most \(d\) (the effect_depth parameter of chart_fold). Each chart cell at span \((i, j)\) is indexed by an element of \(\widehat{\mathcal{C}}\).

2. Typeclass denotations

Each typeclass \(\mathfrak{C}\) in quivers.monadic.typeclasses is modeled by a panproto theory \(\mathrm{Th}\mathfrak{C}\) in quivers.monadic.theories; class extension corresponds to theory inclusion via \(\mathrm{colimit}\). The sorts and operations of each theory are:

\(\mathrm{Th}\mathfrak{C}\) Sorts Operations Equations
\(\mathrm{ThFunctor}\) \(\mathrm{Carrier}\), \(\mathrm{Hom}\) \(\mathrm{fmap\_obj}\), \(\mathrm{fmap}\) identity, composition
\(\mathrm{ThApplicative}\) (extends Functor) \(\mathrm{pure}\), \(\mathrm{apply}\) identity, homomorphism, interchange, composition
\(\mathrm{ThMonad}\) (extends Applicative) \(\mathrm{join}\) left/right unit, associativity
\(\mathrm{ThAlternative}\) (extends Applicative) \(\mathrm{empty}\), \(\mathrm{alt}\) identity, associativity
\(\mathrm{ThMonadPlus}\) (extends Monad + Alternative) (none new) left zero
\(\mathrm{ThTraversable}\) (extends Functor + Foldable) \(\mathrm{traverse}\) naturality, identity, composition

An effect instance \(T\) that registers against \(\mathfrak{C}\) corresponds to a panproto theory morphism \(\mathrm{Th}\mathfrak{C} \to \mathrm{ThQVR}\) whose vertex map sends \(\mathrm{Carrier}\) to the runtime carrier sort of the residuated universe and whose operation map realizes the class operations as morphisms of \(\mathcal{V}\text{-}\mathbf{Rel}\) / \(\mathbf{Stoch}\) / \(\mathbf{Kern}\).

3. Effect-typed schema denotations

A SchemaDecl whose domain or codomain mentions an ObjectEffectApply node \(T(X)\) is parametric in its free pattern variables. For each choice of instantiation \(X, Y \in \mathcal{C}\) the schema denotes a morphism

\[ \llbracket r \rrbracket_{X, Y} \;:\; T(X/Y) \otimes T(Y) \;\to\; T(X) \quad \text{in } \widehat{\mathcal{C}}; \]

the family \(\bigl(\llbracket r \rrbracket_{X, Y}\bigr)_{X, Y}\) is a natural transformation of bifunctors (an applicative-style lifted application). The naturality square is the applicative composition law; it follows from the implementation when \(T\) inhabits \(\mathbf{Applicative}\).

For Monad-typed schemas the denotation is the Kleisli composition:

\[ \llbracket \mathrm{bind}_T \rrbracket_{X, Y} \;:\; T(X) \otimes (X \backslash T(Y)) \;\to\; T(Y), \]

a morphism in the Kleisli category \(\mathrm{Kl}(T)\) realizing the canonical bind. The two presentations agree via the kleisli / arrow_monad bridges.

4. Joint type-and-effect dispatch

A chart parser over a residuated universe \(\mathcal{C}\) with declared effects \(\bar T = (T_1, \dots, T_n)\) has cells

\[ \mathrm{Chart}[i, j] \;\in\; \mathcal{V}^{|\widehat{\mathcal{C}}|} \]
a \(\mathcal{V}\)-valued vector indexed by effect-typed categories. Schema firings populate cells according to four rules:
  1. Base firing. A schema \(r : \pi_1 \otimes \pi_2 \to \pi\) fires between cells \(\mathrm{Chart}[i, k]\) and \(\mathrm{Chart}[k, j]\) at the type coordinate when the effect-stack coordinates of both cells are empty (or when the schema has been auto-lifted to admit the cells' effect prefix; see rule 2).
  2. Lift firing. When child cells carry effect prefixes \(\bar{S}_1, \bar{S}_2\) that the schema's domain doesn't, the class-driven lifts of class_directed_lifts emit a schema whose domain wraps the base premises in the appropriate effect prefixes. The denotation of this lifted firing is exactly the natural-transformation composition of §3 above.
  3. Handler firing. When a cell holds a \(T(\alpha)\) distribution and a \(\mathrm{Handler}_{T \to S}\) is registered (a panproto theory morphism \(\mathrm{Th}T \to \mathrm{Th}S\)), applying the handler produces a fresh cell at \(S(\alpha)\). In the special case \(S = \mathrm{Identity}\), the handler eliminates the effect entirely.
  4. Commutation firing. When a \(\mathrm{DistributiveLaw}(T, U)\) is registered, the \(\mathrm{swap}_{T,U}\) schema realizes the natural transformation \(T \circ U \Rightarrow U \circ T\) on cells whose effect-stack ends with \(T \cdot U\).

The four firings compose freely; the chart's CKY enumeration computes the inside score over the joint search space.

4a. Inference rules for effect-typed firing

The four firings are inference rules in the proof system of the chart. Let \(\sigma : \mathrm{Var}(r) \to \mathcal{C}\) range over substitutions of the schema's free pattern variables and let \(\bar S \cdot \bar T\) denote effect-stack concatenation. We write \(\mathrm{Chart}[i, j] \ni (\alpha; \bar T)\) for "the cell at span \((i, j)\) holds an entry at type \(\alpha \in \mathcal{C}\) stacked under effect prefix \(\bar T \in \mathrm{EffectStack}_{\le d}\)".

\[ \frac{r : \pi_1 \otimes \pi_2 \to \pi \in \mathrm{Rules} \qquad \mathrm{Chart}[i, k] \ni (\sigma\pi_1; \varepsilon) \qquad \mathrm{Chart}[k, j] \ni (\sigma\pi_2; \varepsilon)} {\mathrm{Chart}[i, j] \ni (\sigma\pi; \varepsilon)}\ \textsc{Base} \]
\[ \frac{r : \pi_1 \otimes \pi_2 \to \pi \in \mathrm{Rules} \qquad T \in \mathbf{Applicative} \qquad \mathrm{Chart}[i, k] \ni (\sigma\pi_1; \bar S \cdot T) \qquad \mathrm{Chart}[k, j] \ni (\sigma\pi_2; \bar S \cdot T)} {\mathrm{Chart}[i, j] \ni (\sigma\pi; \bar S \cdot T)}\ \textsc{Lift}_T \]
\[ \frac{H : \mathrm{Th}T \to \mathrm{Th}S \in \mathrm{Handlers} \qquad S \neq \mathrm{Identity} \qquad \mathrm{Chart}[i, j] \ni (\alpha; \bar S \cdot T)} {\mathrm{Chart}[i, j] \ni (\alpha; \bar S \cdot S)}\ \textsc{Handle}_{T \to S} \]
\[ \frac{H : \mathrm{Th}T \to \mathrm{Th}\,\mathrm{Identity} \in \mathrm{Handlers} \qquad \mathrm{Chart}[i, j] \ni (\alpha; \bar S \cdot T)} {\mathrm{Chart}[i, j] \ni (\alpha; \bar S)}\ \textsc{Eliminate}_T \]
\[ \frac{\mathrm{swap}_{T, U} : T \circ U \Rightarrow U \circ T \in \mathrm{DistributiveLaws} \qquad \mathrm{Chart}[i, j] \ni (\alpha; \bar S \cdot T \cdot U)} {\mathrm{Chart}[i, j] \ni (\alpha; \bar S \cdot U \cdot T)}\ \textsc{Swap}_{T \mid U} \]

In \(\textsc{Base}\) and \(\textsc{Lift}_T\) the substitution \(\sigma\) is fixed by the cells' type coordinates (which must match \(\pi_1\) and \(\pi_2\) structurally); we elide its construction. \(\textsc{Lift}_T\) requires only that \(T\) inhabit \(\mathbf{Applicative}\); every \(\mathbf{Monad}\) extends \(\mathbf{Applicative}\), so the rule covers monadic effects as a special case. \(\textsc{Handle}_{T \to S}\) and \(\textsc{Eliminate}_T\) are syntactic variants of the same handler firing, separated so each rule has a single conclusion shape.

The denotation of every derivation built from these four rules is the corresponding composite natural transformation in \(\widehat{\mathcal{C}}\); Theorem Lifting Adequacy below identifies the chart's inside score with that composite.

5. Adequacy of effect lifting

Theorem (Lifting Adequacy). Let \(r\) be a base SchemaDecl and \(T\) an effect instance registered against the typeclasses \(\mathfrak{C}_1, \dots, \mathfrak{C}_k\). Then for every cell configuration over \(\widehat{\mathcal{C}}\) that admits a derivation under the lifted schemas \(\mathrm{class\_directed\_lifts}(r, T)\), the chart parser's inside score equals the categorical denotation of the composite natural transformation through \(\mathrm{Th}\mathfrak{C}_1, \dots, \mathrm{Th}\mathfrak{C}_k\) in the appropriate enriched category.

Proof sketch. By induction on the typeclass tower:

  • For \(\mathfrak{C} = \mathbf{Applicative}\), the lifted schema is the applicative composition law; the chart firing realizes the natural transformation \(T(\pi_1) \otimes T(\pi_2) \Rightarrow T(\pi)\) obtained by postcomposing the base \(r\) with \(T\)'s apply. The applicative laws (identity, homomorphism, interchange, composition) imply that successive applicative lifts compose to the same denotation irrespective of bracketing; the chart's left-associative scheduling is thus one valid realization among many equivalent choices.
  • For \(\mathfrak{C} = \mathbf{Monad}\), the bind-lift is the Kleisli composition of the base schema; the monad laws imply \(\mathrm{join} \circ \mathrm{fmap}(\mathrm{join}) = \mathrm{join} \circ \mathrm{join}\), so iterated bind-lifts compose to the iterated Kleisli of the base rule.
  • For \(\mathfrak{C} = \mathbf{Alternative}\), the alt-lift realizes \(T \otimes T \Rightarrow T\) via \(T\)'s alt; the alternative laws give the equational theory of the resulting non-deterministic derivation tree.

The chart algorithm (CKY) is the standard inside-score recurrence and is sound for arbitrary \(\mathcal{V}\)-algebra-valued semirings (see Weighted Deduction Fragment §7). \(\square\)

6. Free-monad denotation

For an effect signature \(\Sigma = \{\mathrm{op}_1 : P_1 \to R_1, \dots, \mathrm{op}_m : P_m \to R_m\}\), the free monad \(\mathrm{FreeMonad}(\Sigma)\) has the denotation of the finitely-branched signature trees over \(\Sigma\):

\[ \llbracket \mathrm{FreeMonad}(\Sigma)(A) \rrbracket \;=\; \coprod_{n \ge 0} \mathrm{Tree}_{\Sigma, n}(A), \]

where \(\mathrm{Tree}_{\Sigma, n}(A)\) is the set of \(\Sigma\)-shaped trees of depth \(\le n\) whose leaves are values in \(A\). The runtime realization truncates at the depth parameter of the enclosing deduction { … } block to keep the carrier finite.

A handler \(H : \Sigma \to S\) is a panproto theory morphism \(\mathrm{Th}\Sigma \to \mathrm{Th}S\); the denotation of \(H.\mathrm{run} : \mathrm{FreeMonad}(\Sigma)(A) \to S(A)\) is the universal map of free monads (the fold over the operation tree that interprets each internal node through the corresponding clause of \(H\)).

7. Bridges and conservativity

The kleisli and arrow_monad bridges of quivers.monadic.bridges realize the canonical theory morphisms:

\[ \mathrm{kleisli} \;:\; \mathrm{ThMonad} \;\to\; \mathrm{ThArrowApply}, \qquad \mathrm{arrow\_monad} \;:\; \mathrm{ThArrowApply} \;\to\; \mathrm{ThMonad} \]

These functions implement the ArrowApply/Monad constructions described by Hughes (2000). In Quivers, \(\mathrm{arrow\_monad} \circ \mathrm{kleisli} \;\cong\; \mathrm{id}_{\mathrm{ThMonad}}\) and \(\mathrm{kleisli} \circ \mathrm{arrow\_monad} \;\cong\; \mathrm{id}_{\mathrm{ThArrowApply}}\) are naturally isomorphic (not equal) via the canonical \(1 \otimes A \cong A\) unitor that absorbs the ArrowMonad(a)(A) = a(1, A) boxing. Consequently the arrow-side and monad-side presentations of any effect agree on denotation up to the canonical isomorphism. When the underlying monad is also a monad-fix, admitting a least-fixed-point operator, the chart_fold runtime's loop_arr construction agrees denotationally with the Kleisli-iteration of the binary step; for monads without mfix, the arrow-side trace is the well-defined realization and the Kleisli side is undefined.

Conservativity. When the declared effects list \(\bar T\) is empty, the joint type-and-effect dispatch of §4 collapses to the classical residuated-grammar dispatch of Weighted Deduction Fragment §6, and the inside score is the standard Lambek / CCG / multimodal-TLG chart-parser denotation. The effects framework is thus a strict extension over the bare grammar fragment.

8. QIEC rows and lexical handlers

QIEC is the explicitly typed account of effects every computation of a module is checked under, the elaborated program included. An applied interface \(E[\bar a]\) describes an operation family, while a lexical instance \(i:E[\bar a]\) supplies the identity that appears in a row. This distinction means that two state cells with the same value type need not collapse into one capability. A row has the schematic form \(\{i_1,\ldots,i_n\mid\rho\;\mathsf{lacks}\;j_1,\ldots,j_m\}\); its tail supports effect polymorphism, and its lacks set records negative constraints needed by row extension and handler elimination.

The reference evaluator gives QIEC computations a deep, lexical handler semantics. Resuming a captured continuation reinstalls the matched handler, while an effect performed by the clause body is offered to outer handlers. Dispatch compares the lexical instance, applied interface, and operation. Thus an unrelated instance of the same interface cannot be intercepted by accident. Dynamic grade checks enforce the declared number of resumptions, and multi-shot resumptions extend their trace address with a branch path.

This row bridge unifies the source contracts of state, abort, random choice, scoring, nondeterministic choice, and weighted accumulation. A handler's clauses are authored in the source or remain process-local attachments. Pyro, NumPyro, PyMC, Edward2, Turing, Gen, WebPPL, and Church lower the same typed computation graph through corresponding implementations of the stable-ID runtime ABI. Conformance tests exercise these implementations in the target runtimes against the reference machine at clamped points, but do not prove them equivalent; each dispatches by stable instance and operation identifiers rather than by interface names. Stan lowers a computation with an empty closed effect row, an empty static telescope, and a scalar result as a user-defined function, conditionals, calls, and recursion included; BUGS and JAGS refuse every call. The static targets issue precise capability diagnostics for the rest. Establishing a backend-level adequacy proof between each generated runtime and the reference evaluator remains a live possibility. The QIEC developer note gives the executable boundary.

The effect handlers of quivers.effects are lexical handlers of this calculus. A MonadicProgram runs on the reference machine as the kernel computation program_kernel encodes it to: each host step is an instance of the prelude's Compute interface performed on the environment of every value bound so far, each draw is the canonical Random.sample request on the program's random instance, and each site's density is a Score.add the answering handler emits on the program's score instance. A handler on the with stack installs a lexical handler of one of those instances; the run nests them in a fixed order, the score accumulator outermost, then every score transformer, then the scoring draw and the run's observations, then every handler of random in stack order, then the parameter store and the param handlers layered over it, then the host steps. Two consequences follow. An inner handler of random sees a site's request before any outer one and sees the outer answer flow back through its resumption, so a trace inside a clamp records the clamped value. A site's density is emitted outward by whichever handler answered it, so every score transformer reaches every site, and a trace reads each site's density from what reached the accumulator under the site's provenance, which the kernel carries on every derived request as the site's static identity and dynamic address.

References