Algebraic effects in Montague semantics

To start, we'll define our computation types as values of a function \(\mathcal{F}_l(v)\), where \(l\) is a parameter consisting of a list of types of the form \(p_i ⤚ a_i\). \(\mathcal{F}_l(v)\) is defined as follows, where \(\epsilon\) is the empty list, and \(o\) is an arbitrary type. (Thus, fixing \(v\), computation types act like equivalence classes of simple types that are agnostic about what \(o\) is).

\[\begin{align*} \mathcal{F}_{\epsilon}(v) &= v\\ \mathcal{F}_{p ⤚ a, l}(v) &= (p \rightarrow (a \rightarrow \mathcal{F}_l(v)) \rightarrow o) \rightarrow o \end{align*}\]

Thus any computation whose type is derived from the parameter \(\epsilon\) is trivial; it just returns a value. To see what a computation whose type is derived from a complex parameter looks like, let's consider the parameter \((e \rightarrow t) \rightarrow t ⤚ e, (e \rightarrow t) \rightarrow t ⤚ e\). Any such computation is a λ-term of the following type.

\[\begin{align*} &\mathcal{F}_{(e \rightarrow t) \rightarrow t ⤚ e, (e \rightarrow t) \rightarrow t ⤚ e}(v)\\ =\ \ &(((e \rightarrow t) \rightarrow t ) \rightarrow (e \rightarrow \mathcal{F}_{(e \rightarrow t) \rightarrow t ⤚ e}(v)) \rightarrow o) \rightarrow o\\ =\ \ &(((e \rightarrow t) \rightarrow t ) \rightarrow (e \rightarrow (((e \rightarrow t) \rightarrow t ) \rightarrow (e \rightarrow \mathcal{F}_\epsilon(v) \rightarrow o^\prime) \rightarrow o^\prime) \rightarrow o) \rightarrow o\\ =\ \ &(((e \rightarrow t) \rightarrow t ) \rightarrow (e \rightarrow (((e \rightarrow t) \rightarrow t ) \rightarrow (e \rightarrow v \rightarrow o^\prime) \rightarrow o^\prime) \rightarrow o) \rightarrow o \end{align*}\]

If we set \(v\) to the type \(t\) of truth values, a term of this type might be the following one. (As will become evident, this term represents the meaning of the sentence every dog chased every cat.)

\[\lambda h.h (\lambda k.\forall x.\textbf{dog} x \rightarrow k x) (\lambda y, h^\prime.h^\prime (\lambda k.\forall x.\textbf{cat} x \rightarrow k x) (\lambda z.\textbf{chase} z y))\]

Such a format for representing computations may look reminiscent of the system presented in §1, but with two crucially new conventions. First, operations are now represented by λ-abstracted variables. The choice of variable name \(h\) is meant to suggest that operations act as functions on their handlers; indeed, interpreting an operation in terms of a handler, from this perspective, is just a matter of passing the handler to the operation (encoded as a λ-abstraction). Second, the parameters of computation types now explicitly represent how many times particular operations are invoked, and in what order. The computation type \(\mathcal{F}_{(e \rightarrow t) \rightarrow t ⤚ e, (e \rightarrow t) \rightarrow t ⤚ e}(t)\), for instance, is the type of a computation which invokes the \(\mathtt{scope}\) operation twice before returning a value of type \(t\).

Thus there is a somwhat indirect relationship between the parameter \(l\) of a computation type \(\mathcal{F}_l(v)\) and an algebraic signature: the parameter describes the operations invoked in a computation (in the order in which they are invoked) and, hence, the operations contained in the smallest algebraic signature with which the computation is compatible. The parameter \(\epsilon\) indicates that no operations are invoked; such a computation (which merely returns a value) is thus compatible with any algebraic signature. Meanwhile, the parameter \(p_1 ⤚ a_1, \ldots, p_n ⤚ a_n\) indicates that operations with those types are invoked (in that order); such a computation is compatible with any algebraic signature, as long as it contains operations with the types \(p_1 ⤚ a_1, \ldots, p_n ⤚ a_n\).

In Haskell, we may encode \(\mathcal{F}_l(v)\) as a generalized algebraic data type.

-- | The data type of effectful computations.
data F l v where
  Pure :: v -> F '[] v
  Impure :: (forall o . (p -> (a -> F l v) -> o) -> o) -> F (p >-- a ': l) v

We have two constructors: Pure, for trivial (i.e., pure) computations that return values, and Impure, for those which invoke an operation before continuing with the rest of the computation. Note that we invoke explicit quantification over the type \(o\) to encode the GADT, rather than simply allow it to be arbitrary, as above. Type-quantificationais a necessary feature of the Haskell implementation, since the GADT would otherwise hide the type \(o\), forcing on it an existential interpretation.

Given our encoding of computations with algebraic effects into the simply typed λ-calculus, we ought to provide a way of composing them analogous to what we had in §1. Fortunately, the relevant compositional scheme is straightforward: just as algebraic effects normally give rise to monads, our encoding gives rise to graded monads.

Graded monads generalize monads in order to associate with each computation type an effect that parameterizes it with fine-grained information about the nature of the relevant side effect. Concretely, a graded monad is a family of functors \(G : \mathcal{E} \rightarrow \mathcal{T} \rightarrow \mathcal{T}\), parameterized by a monoid \(\mathcal{E}\) of effects. Then given some \(e \in \mathcal{E}\), \(G_e\) is an endofunctor on the category \(\mathcal{T}\) of types. Associated with each graded monad are two operators, \((\cdot)^\eta\) and \(\bind\), having the following type-signatures (where \(\mathtt{0}\) and \(+\) are, respectively, the identity and associative operation of the monoid \(\mathcal{E}\)).

\[\begin{align*} (\cdot)^\eta &: v \rightarrow G_\mathtt{0}(v)\\ (\bind) &: G_e(v) \rightarrow (v \rightarrow G_f(w)) \rightarrow G_{e+f}(w) \end{align*}\]

These operators are required to satisfy the graded monad laws, which are identical in form to the laws for ordinary monads, modulo the manipulation of effects.⁶

In our case, the relevant graded monad consists of the function \(\mathcal{F} : {\mathcal{T}_⤚}^* \rightarrow \mathcal{T} \rightarrow \mathcal{T}\), whose effects are given by \({\mathcal{T}_⤚}^*\), the free monoid (i.e., of lists) over \(\mathcal{T}_⤚ = \{p ⤚ a \divd p, a \in \mathcal{T}\}\). Given any effect \(l \in {\mathcal{T}_⤚}^*\), \(\mathcal{F}_l\) is indeed a functor, as witnessed by the following definition of \(\mathtt{map}_{\mathcal{F}_l}\).

\[\begin{align*} \mathtt{map}_{\mathcal{F}_l} &: (v \rightarrow w) \rightarrow \mathcal{F}_l(v) \rightarrow \mathcal{F}_l(w)\\ \mathtt{map}_{\mathcal{F}_\epsilon} f v &= f v\tag{injection}\\ \mathtt{map}_{\mathcal{F}_{p ⤚ a, l}} f m &= \lambda h.m (\lambda p, k.h p (\lambda a.\mathtt{map}_{\mathcal{F}_l} f (k a)))\tag{operation} \end{align*}\]

(Accordingly, we may write the following Functor instance in Haskell.)

-- | For any effect l, F l is a /Functor/.
instance Functor (F l) where
  fmap f (Pure v) = Pure $ f v
  fmap f (Impure m) = Impure $ \h -> m $ \p k -> h p (\a -> fmap f $ k a)

The fact that \(\mathcal{F}\) is a graded monad is exhibited, first, by the following definition of \((\cdot)^\eta\),

\[\begin{align*} (\cdot)^\eta &: v \rightarrow \mathcal{F}_\epsilon(v)\\ v^\eta &= v \end{align*}\]

and second, by the following definition of \(\bind\).

\[\begin{align*} (\bind) &: \mathcal{F}_{l_1}(v) \rightarrow (v \rightarrow \mathcal{F}_{l_2}(w)) \rightarrow \mathcal{F}_{l_1, l_2}(w)\\ v \bind k &= k v\tag{injection}\\ m \bind k &= \lambda h.m (\lambda p, k^\prime.h p (\lambda a.k^\prime a \bind k))\tag{operation} \end{align*}\]

In Haskell, we may write the corresponding instance for the Effect class of [Orchard and Petricek, 2014] for graded monads. (:++), which provides the associative operation of the relevant monoid, is concatenation on type-level lists.

-- | Computations with algebraic effects form a graded monad.
instance Effect F where
  type Unit F = '[] -- The monoidal unit.
  type Plus F l1 l2 = l1 :++ l2 -- The monoidal associative operation.

  return :: v -> F '[] v
  return v  = Pure v

  (>>=) :: F l1 v -> (v -> F l2 w) -> F (l1 :++ l2) w
  Pure v >>= k = k v -- (injection)
  Impure m >>= k = Impure $ \h -> m $ \p k' -> h p (\a -> k' a >>= k) -- (operation)

At this point, it is useful to define the operations that will be the basis of the linguistic example presented §3. We can understand operations associated with the type \(p ⤚ a\) as simply typed λ-terms with the following type (where \(v\) is an arbitrary value type and \(l\) may be any effect).

\[p \rightarrow (a \rightarrow \mathcal{F}_l(v)) \rightarrow \mathcal{F}_{p ⤚ a, l}(v)\]

-- | The type of an operation taking parameter p and a-many arguments.
type Operation p a = forall l v . p -> (a -> F l v) -> F (p >-- a ': l) v

Any given operation will therefore be rendered as a λ-term with the following shape.

\[\begin{align*} \mathtt{op}_{p ⤚ a} &: p \rightarrow (a \rightarrow \mathcal{F}_l(v)) \rightarrow \mathcal{F}_{p ⤚ a, l}(v)\\ \mathtt{op}_{p ⤚ a}(p; k) &= \lambda h.h p k \end{align*}\]

-- | Operations take a parameter, p, and a-many arguments. Handlers then use the
-- parameter to choose which arguments they will further handle.
op :: Operation p a
op p k = Impure $ \h -> h p k

Given a parameter \(p\) and a continuation \(k\) (associated with arity \(a\)), the operation builds a new computation, i.e., element of an algebra whose signature is compatible with the effect \(p ⤚ a, l\). Any given operation is associated with a computation that simply invokes the operation on some parameter and returns a result. Given an operation associated with the type \(p ⤚ a\), and a parameter \(p\) (of type \(p\)), the corresponding computation is given by the following abbreviation \(\mathtt{comp}_{p ⤚ a}\).

\[\begin{align*} \mathtt{comp}_{p ⤚ a} &: p \rightarrow \mathcal{F}_{p ⤚ a}(a)\\ \mathtt{comp}_{p ⤚ a} p &= \mathtt{op}_{p ⤚ a}(p; \lambda a.a) \end{align*}\]

-- | The type of a computation consisting of a single operation.
type Computation p a = p -> F '[p >-- a] a

-- | Computations (of one operation) just perform the operation and return the
-- result.
comp :: Computation p a
comp p = op p return

That is, the computation invokes the operation and continues with the return of the graded monad. Any operation may then be recovered from its associated computation by binding it to the relevant continuation, i.e., as

\[\mathtt{op}_{p ⤚ a}(p; k) = \mathtt{comp}_{p ⤚ a} p \bind k\]

For the linguistic example we consider in §3, we will deal specifically with the operations associated with state (§2.3.1) and quantification (§2.3.2).

In total we have three operations, \(\mathtt{get}_{\star ⤚ \gamma}\), \(\mathtt{put}_{\gamma ⤚ \star}\), and \(\mathtt{scope}_{(e \rightarrow t) \rightarrow t ⤚ e}\); what we need now is a way to handle them. Recall from §1 that handlers have the following shape,

\[\banana{(\mathtt{op}_i : M_i)_{i \in I}, \eta : N}\]

where \((\mathtt{op}_i : M_i)_{i \in I}\) is some collection of operations in one algebra, associated with the terms which interpret them in another. (Recall that \(\eta : N\) means that the handler interprets pure values \(v\) as \(N v\).) In this subsection, I will outline a general procedure for translating arbitrary handlers with this shape into the simply typed λ-calculus in a way compatible with the given encoding of operations and computations. In particular, any given handler will be encoded as a function of type \(\mathcal{F}_{l_{in}}(v_{in}) \rightarrow \mathcal{F}_{l_{out}}(v_{out})\) that takes a computation to handle as its input in order to produce an interpretation for that computation in the new algebra as its output.

It helps to show the encoding of a handler by first representing it as a tuple holding its individual interpreters. Thus we will start by representing an arbitrary handler, as given above, in terms of the following tuple.

\[\langle M_1, \ldots, M_{|I|}, N\rangle\]

The tuple provides a kind of middleman while we build the λ-term corresponding to the handler. To encode the handler, we'll need the ability to retrieve the components of this tuple when the encoding requires them. Thus we'll require the following function, \(\mathtt{retrieve}\).

\[\begin{align*} \mathtt{retrieve} &: m_1 \times \ldots \times m_{|I|} \times n \rightarrow o\ \ (\text{where}\ o \in \{m_1, \ldots, m_{|I|}, n\})\\ \mathtt{retrieve} \langle\ldots O \ldots\rangle &= O \end{align*}\]

This scheme can be implemented in Haskell in terms of the following class.

-- | The class of handlers whose individual interpreters may be retrieved.
class Retrievable interpreter handler where
  retrieve :: handler -> interpreter

The tuple corresponding to a handler has two types of components: those interpreting operations, and one final one interpreting values. In both cases, we wish to interpret the source (operation or value) in some target algebra, i.e., one whose signature is compatible with some predetermined effect \(l\). Thus we have the following types for the interpreters which are the components of such a tuple.

-- | A type for operation interpreters.
type InterpretOp p a l v = p -> (a -> F l v) -> F l v

-- | A type for value interpreters.
type InterpretVal l v1 v2 = v1 -> F l v2

For our case, we will require a handler that interprets computations from the {\(\mathtt{get}_{\star ⤚ \gamma}\), \(\mathtt{put}_{\gamma ⤚ \star}\), \(\mathtt{scope}_{(e \rightarrow t) \rightarrow t ⤚ e}\)}-algebra as simpler computations that invoke exactly one \(\mathtt{get}_{\star ⤚ \gamma}\) and exactly one \(\mathtt{put}_{\gamma ⤚ \star}\); that is, computations whose types are parameterized by the effect \(\star ⤚ \gamma, \gamma ⤚ \star\), and which thus have the following shape (where \(g^\prime\) is some environment and \(v\) is some value, both possibly depending on the input \(g\) in some way).

\[\begin{align*} &\mathtt{get}_{\star ⤚ \gamma}(\star; \lambda g.\mathtt{put}_{\gamma ⤚ \star}(g^\prime; \lambda\star, v))\\ =\ \ &\lambda h.h \star (\lambda g, h^\prime.h^\prime g^\prime (\lambda\star.v)) \end{align*}\]

Such simpler computations are "fully interpreted", insofar as they correspond exactly to computations in the State monad. In particular, the above λ-term may be viewed as an alternative notation for the following Stateful program.

\[\lambda g.\langle v, g^\prime\rangle\]

Accordingly, we will interpret values by simply returning them in (our encoding of) the State monad; that is, using the following interpreter.

\[\begin{align*} \mathtt{interpretStVal} &: v \rightarrow \mathcal{F}_{\star ⤚ \gamma, \gamma ⤚ \star}(v)\\ \mathtt{interpretStVal} &= \lambda v.\mathtt{get}_{\star ⤚ \gamma}(\star; \lambda g.\mathtt{put}_{\gamma ⤚ \star}(g; \lambda\star.v))\\ &= \lambda v, h.h \star (\lambda g, h^\prime.h^\prime g (\lambda\star.v)) \end{align*}\]

type InterpretStVal v = InterpretVal '[() >-- [Entity], [Entity] >-- ()] v v

-- | Interpret a value.
interpretStVal :: InterpretStVal v
interpretStVal = \v -> get () (\g -> put g (\() -> return v))

That is, the interpreter for values yields a computation corresponding to the following program, given a value \(v\).

\[\lambda g.\langle v, g\rangle\]

Analogously, the interpreters for operations have the following types.

type InterpretStOp p a v = InterpretOp p a '[() >-- [Entity], [Entity] >-- ()] v

type InterpretStGet v = InterpretStOp () [Entity] v
type InterpretStPut v = InterpretStOp [Entity] () v
type InterpretStScope = InterpretStOp Quantifier Entity Bool

An interpreter for \(\mathtt{get}_{\star ⤚ \gamma}\), for instance, will be of type \(\star \rightarrow (\gamma \rightarrow \mathcal{F}_{\star ⤚ \gamma, \gamma ⤚ \star}(v)) \rightarrow \mathcal{F}_{\star ⤚ \gamma, \gamma ⤚ \star}(v)\). In particular, we may interpret it as follows.

\[\begin{align*} \mathtt{interpretStGet} &: \star \rightarrow (\gamma \rightarrow \mathcal{F}_{\star ⤚ \gamma, \gamma ⤚ \star}(v)) \rightarrow \mathcal{F}_{\star ⤚ \gamma, \gamma ⤚ \star}(v)\\ \mathtt{interpretStGet} &= \lambda\star, k.\mathtt{get}_{\star ⤚ \gamma}(\star; \lambda g.k g (\lambda\star, k^\prime.k^\prime g))\\ (\ &= \lambda\star, k, h.h \star (\lambda g.k g (\lambda\star, k^\prime.k^\prime g))\ \ ) \end{align*}\]

-- | Interpret a 'get' occurrence.
interpretStGet :: InterpretGet v
interpretStGet = \() k -> get () (\g -> case k g of
                                          Impure m -> m $ \() k' -> k' g)

Thus we interpret a \(\mathtt{get}_{\star ⤚ \gamma}\) by building a computation of type \(\mathcal{F}_{\star ⤚ \gamma, \gamma ⤚ \star}(v)\) that feeds its (interpreted) continuation of type \(\gamma \rightarrow \mathcal{F}_{\star ⤚ \gamma, \gamma ⤚ \star}(v)\) the first gotten environment of the computation, after which it, again, feeds this environment to the outer \(\mathtt{get}_{\star ⤚ \gamma}\) of the result.

The interpretation of \(\mathtt{put}_{\gamma ⤚ \star}\) is analagous.

\[\begin{align*} \mathtt{interpretStPut} &: \gamma \rightarrow (\star \rightarrow \mathcal{F}_{\star ⤚ \gamma, \gamma ⤚ \star}(v)) \rightarrow \mathcal{F}_{\star ⤚ \gamma, \gamma ⤚ \star}(v)\\ \mathtt{interpretStPut} &= \lambda g, k.\mathtt{get}_{\star ⤚ \gamma}(\star; \lambda g^\prime.k \star (\lambda\star, k^\prime.k^\prime g))\\ (\ &= \lambda g, k, h.h \star (\lambda g^\prime.k \star (\lambda\star, k^\prime.k^\prime g))\ \ ) \end{align*}\]

-- | Interpret a 'put' occurrence.
interpretStPut :: InterpretPut v
interpretStPut = \g k -> get () (\g' -> case k () of
                                          Impure m -> m $ \() k' -> k' g)

In this case, the \(\mathtt{put}_{\gamma ⤚ \star}\) occurrence is interpreted by plugging its (interpreted) continuation with \(\star\) and then feeding the environment it puts to the outer \(\mathtt{get}_{\star ⤚ \gamma}\) of the result. Doing so ensures that \(\mathtt{put}_{\gamma ⤚ \star}\) has the required effect on the resulting computation; i.e., that of dictating its input.

Finally, we have the following interpretation for \(\mathtt{scope}_{(e \rightarrow t) \rightarrow t ⤚ e}\).

\[\begin{align*} \mathtt{interpretStScope} &: ((e \rightarrow t) \rightarrow t) \rightarrow (e \rightarrow \mathcal{F}_{\star ⤚ \gamma, \gamma ⤚ \star}(t)) \rightarrow \mathcal{F}_{\star ⤚ \gamma, \gamma ⤚ \star}(t)\\ \mathtt{interpretStScope} &= \lambda q, k.\mathtt{get}_{\star ⤚ \gamma}(\star; \lambda g.\mathtt{put}_{\gamma ⤚ \star}(g; \lambda\star.q (\lambda x.k x (\lambda\star, k^\prime.k^\prime g (\lambda g^\prime, k^{\prime\prime}.k^{\prime\prime} \star)))))\\ (\ &= \lambda q, k, h.h \star (\lambda g, h^\prime.h^\prime g (\lambda\star.q (\lambda x.k x (\lambda\star, k^\prime.k^\prime g (\lambda g^\prime, k^{\prime\prime}.k^{\prime\prime} \star)))))\ \ ) \end{align*}\]

-- | Interpret a 'scope' occurrence.
interpretStScope :: InterpretScope
interpretStScope = \q k ->
                 get () (\g ->
                 put g (\() ->
                 return (q $ \x -> case k x of
                                     Impure m -> m $ \_ k' ->
                                       case k' g of
                                         Impure m' -> m' $ \_ k'' ->
                                           case k'' () of
                                             Pure a -> a)))

Thus, in order to interpret an occurrence of \(\mathtt{scope}_{(e \rightarrow t) \rightarrow t ⤚ e}\), we must essentially push the \((e \rightarrow t) \rightarrow t\) -type quantifier meaning down past the \(\mathtt{get}_{\star ⤚ \gamma}\) and \(\mathtt{put}_{\gamma ⤚ \star}\) of the resulting computation so that it may gain access to a continuation of type \(e \rightarrow t\). The implication of using such an interpreter for \(\mathtt{scope}_{(e \rightarrow t) \rightarrow t ⤚ e}\) effects is that quantifier meanings may only be handled inside computations whose value type is \(t\), i.e., at sentence boundaries. An immediate consequence of pushing quantifier meanings down past \(\mathtt{get}_{\star ⤚ \gamma}\) and \(\mathtt{put}_{\gamma ⤚ \star}\) (a maneuver which has been forced upon us by the types!) is that dynamic effects incurred within the quantifier's scope are lost outside of it. In other words, allowing quantifier meanings access to a scope of the right type forces a situation in which they may be live candidates for anaphora inside of their scope, but not outside of it. We have thus derived (from their types!) that quantifier meanings are internally dynamic, but externally static, with respect to anaphora. This situation does not hold for ordinary anaphora, i.e., to individual-denoting expressions, whose side effects are captured in the resulting State-monadic algebra, rendering them dynamic.⁷

We may now construct the tuple determining our handler as follows.

\[\begin{align*} \mathtt{getPutScopeHandler} = \langle&\mathtt{interpretStGet},\\ &\mathtt{interpretStPut},\\ &\mathtt{interpretStScope},\\ &\mathtt{interpretStVal}\rangle \end{align*}\]

-- | The type of handlers for computations possibly featuring 'get', 'put', and
-- 'scope'.
type GetPutScopeHandler
  = (InterpretGet Bool,
      (InterpretPut Bool,
        (InterpretScope,
          InterpretStVal Bool)))

-- | A handler for computations possibly featuring 'get', 'put', and 'scope'.
getPutScopeHandler :: GetPutScopeHandler
getPutScopeHandler = (interpretStGet,
                       (interpretStPut,
                         (interpretStScope,
                           interpretStVal)))

In order to correctly retrieve an interpreter from a handler, we must define the following instances of the Retrievable class in Haskell (there are eleven total!).⁸

-- | When a handler has only one component.
instance Retrievable interpreter interpreter where
  retrieve = id

-- | Access the first component of a handler.
instance Retrievable interpreter (interpreter, handler) where
  retrieve = fst

-- | Look past the first component to retrieve an interpreter from inside the
-- second component.
instance Retrievable (InterpretStVal v) handler
      => Retrievable (InterpretStVal v) (InterpretGet v, handler) where
  retrieve = retrieve . snd

-- | Look past the first component to retrieve a handler from inside the
-- second component.
instance Retrievable (InterpretStVal v) handler
      => Retrievable (InterpretStVal v) (InterpretPut v, handler) where
  retrieve = retrieve . snd

-- | Look past the first component to retrieve a handler from inside the
-- second component.
instance Retrievable (InterpretStVal v) handler
      => Retrievable (InterpretStVal v) (InterpretScope, handler) where
  retrieve = retrieve . snd

-- | Look past the first component to retrieve a handler from inside the
-- second component.
instance Retrievable (InterpretGet v) handler
      => Retrievable (InterpretGet v) (InterpretPut v, handler) where
  retrieve = retrieve . snd

-- | Look past the first component to retrieve a handler from inside the
-- second component.
instance Retrievable (InterpretGet v) handler
      => Retrievable (InterpretGet v) (InterpretScope, handler) where
  retrieve = retrieve . snd

-- | Look past the first component to retrieve a handler from inside the
-- second component.
instance Retrievable (InterpretPut v) handler
      => Retrievable (InterpretPut v) (InterpretGet v, handler) where
  retrieve = retrieve . snd

-- | Look past the first component to retrieve a handler from inside the
-- second component.
instance Retrievable (InterpretPut v) handler
      => Retrievable (InterpretPut v) (InterpretScope, handler) where
  retrieve = retrieve . snd

-- | Look past the first component to retrieve a handler from inside the
-- second component.
instance Retrievable InterpretScope handler
      => Retrievable InterpretScope (InterpretGet v, handler) where
  retrieve = retrieve . snd

-- | Look past the first component to retrieve a handler from inside the
-- second component.
instance Retrievable InterpretScope handler
      => Retrievable InterpretScope (InterpretPut v, handler) where
  retrieve = retrieve . snd

With these components, defining a handler for our effects is straightforward. In particular, we may define the following partial function, \(\mathtt{handle}\), from tuples to λ-terms.

\[\begin{align*} \mathtt{handle} &: m_1 \times \ldots \times m_{|I|} \times n \rightarrow \mathcal{F}_{l_{in}}(v_{in}) \rightarrow \mathcal{F}_{l_{out}}(v_{out}) \end{align*}\]

As in §1, the semantics of effect handling is defined by an injection case and an operation case. These correspond to the following two definitions of \(\mathtt{handle}\), depending on whether the computation it handles invokes operations or merely returns a value. (Note that we're ignoring the case in which a handler passes over an operation it doesn't handle, since it is currently irrelevant for our purposes.)

\[\begin{align*} \mathtt{handle} h v &= \mathtt{retrieve} h v\tag{injection}\\ \mathtt{handle} h m &= m (\lambda p, k.\mathtt{retrieve} h p (\lambda a.\mathtt{handle} h (k a)))\tag{operation} \end{align*}\]

In Haskell, we may define a corresponding Handleable class, along with the two relevant instances for injections and operations (note that we invoke type applications, along with the ScopedTypeVariables language extension, to fix the right type for \(\mathtt{retrieve}\) when handling an operation).

-- | The class of handleable effects. Handle a computation associated with the
-- list of effects l1 and value type v1 to turn it into a computation associated
-- with the list of effects l2 and value type v2, in a way that depends on the
-- given handler.
class Handleable handler l1 l2 v1 v2 where
  handle :: handler -> F l1 v1 -> F l2 v2

-- | Handle a value.
instance Retrievable (InterpretStVal v) handler
      => Handleable handler '[] '[() >-- [Entity], [Entity] >-- ()] v v where
  handle handler (Pure v) = retrieve handler v

-- | Handle an operation.
instance (Retrievable (InterpretStOp p a v) handler,
          Handleable handler l '[() >-- [Entity], [Entity] >-- ()] v v)
      => Handleable handler (p >-- a ': l)
         '[() >-- [Entity], [Entity] >-- ()] v v where
  handle handler (Impure m)
    = m $ \p k -> retrieve @(InterpretStOp p a v) handler
                  p (\a -> handle handler (k a))

At the end of the day, we may define the handler for our fragment as a family of λ-terms indexed by the set \(\{\star ⤚ \gamma, \gamma ⤚ \star, (e \rightarrow t) \rightarrow t ⤚ e\}^*\), i.e., of effects built up only from the types associated with our three operations. Given an effect \(l\) from this set, we may define our handler as follows.

\[\begin{align*} \mathtt{handleSentence}_l &: \mathcal{F}_l(t) \rightarrow \mathcal{F}_{\star ⤚ \gamma, \gamma ⤚ \star}(t)\\ \mathtt{handleSentence}_l &= \mathtt{handle}\ \mathtt{getPutScopeHandler} \end{align*}\]

-- | Handle a sentence with effects, using a 'GetPutScopeHandler'.
handleSentence :: Handleable GetPutScopeHandler l
                  '[() >-- [Entity], [Entity] >-- ()] Bool Bool
               => F l Bool -> F '[() >-- [Entity], [Entity] >-- ()] Bool
handleSentence = handle getPutScopeHandler

Note that, because the handler handles quantifier meanings, it is only applicable at computations with return values of type \(t\). That said, any given effect from the set above will determine a handler. As an example, let's take the case of a computation with one \(\mathtt{scope}_{(e \rightarrow t) \rightarrow t ⤚ e}\), i.e., whose effect is just the singleton \((e \rightarrow t) \rightarrow t ⤚ e\).

\[\begin{align*} &\mathtt{handleSentence}_{(e \rightarrow t) \rightarrow t ⤚ e} : \mathcal{F}_{(e \rightarrow t) \rightarrow t ⤚ e}(t) \rightarrow \mathcal{F}_{\star ⤚ \gamma, \gamma ⤚ \star}(t)\\ &\mathtt{handleSentence}_{(e \rightarrow t) \rightarrow t ⤚ e} m\\ =\ \ &\mathtt{handle}\ \mathtt{getPutScopeHandler}\ m\\ =\ \ &m (\lambda q, k.\mathtt{retrieve}\ \mathtt{getPutScopeHandler}\ q\ (\lambda x.\mathtt{handle}\ \mathtt{getPutScopeHandler}\ (k x)))\\ =\ \ &m (\lambda q, k.\mathtt{retrieve}\ \mathtt{getPutScopeHandler}\ q\ (\lambda x.\mathtt{retrieve}\ \mathtt{getPutScopeHandler}\ (k x)))\\ =\ \ &m (\lambda q, k.\mathtt{retrieve}\ \mathtt{getPutScopeHandler}\ q\ (\lambda x.\mathtt{interpretStVal}\ (k x)))\\ =\ \ &m (\lambda q, k.\mathtt{interpretStScope}\ q\ (\lambda x.\mathtt{interpretStVal}\ (k x)))\\ =\ \ &m (\lambda q, k, h.h \star (\lambda g, h^\prime.h^\prime g (\lambda\star.q (\lambda x.\mathtt{interpretStVal}\ (k x) (\lambda\star, k^\prime.k^\prime g (\lambda g^\prime, k^{\prime\prime}.k^{\prime\prime} \star))))))\\ =\ \ &m (\lambda q, k, h.h \star (\lambda g, h^\prime.h^\prime g (\lambda\star.q (\lambda x.k x))))\\ =\ \ &m (\lambda q, k.\mathtt{get}_{\star ⤚ \gamma}(\star; \lambda g.\mathtt{put}_{\gamma ⤚ \star}(g; \lambda\star.q (\lambda x.k x)))) \end{align*}\]

Note that, in this case, the type of \(m\) is

\[\begin{align*} &(((e \rightarrow t) \rightarrow t) \rightarrow (e \rightarrow \mathcal{F}_\epsilon(t)) \rightarrow \mathcal{F}_{\star ⤚ \gamma, \gamma ⤚ \star}(t)) \rightarrow \mathcal{F}_{\star ⤚ \gamma, \gamma ⤚ \star}(t)\\ =\ \ &(((e \rightarrow t) \rightarrow t) \rightarrow (e \rightarrow t) \rightarrow \mathcal{F}_{\star ⤚ \gamma, \gamma ⤚ \star}(t)) \rightarrow \mathcal{F}_{\star ⤚ \gamma, \gamma ⤚ \star}(t) \end{align*}\]

so that the result type \(o\) is fixed to \(\mathcal{F}_{\star ⤚ \gamma, \gamma ⤚ \star}(t)\).

Let's first introduce a lexicon of English, complete with denotations as simply typed λ-terms. To analyze anaphora, we'll use the \(\mathtt{sel}\) function of [de Groote, 2006], which retrieves an individual from the environment (and is thus of type \(\gamma \rightarrow e\)).

\[\begin{align*} \mathtt{every} &: (e \rightarrow t) \rightarrow \mathcal{F}_{(e \rightarrow t) \rightarrow t ⤚ e}(e)\\ \mathtt{every} &= \lambda p.\mathtt{scope}^\prime_{(e \rightarrow t) \rightarrow t ⤚ e} (\lambda k.\forall x : p x\ \rightarrow\ k x)\\ &= \lambda p, h.h\ (\lambda k.\forall x : p x\ \rightarrow\ k x)\ (\lambda y.y)\\[3mm] \mathtt{herself} &: \mathcal{F}_{\star ⤚ \gamma}(e)\\ \mathtt{herself} &= \mathtt{get}_{\star ⤚ \gamma}(\star; \lambda g.\mathtt{sel} g)\\ &= \lambda h.h \star (\lambda g.\mathtt{sel} g)\\[3mm] (\cdot)^\triangleright &: \mathcal{F}_l e \rightarrow \mathcal{F}_{l, \star ⤚ \gamma, \gamma ⤚ \star}(e)\tag{bind}\\ m^\triangleright &= m \bind \lambda x.\mathtt{get}_{\star ⤚ \gamma}(\star; \lambda g.\mathtt{put}_{\gamma ⤚ \star}(\append{x}{g}; \lambda\star.x))\\ &= m \bind \lambda x, h.h \star (\lambda g, h^\prime.h^\prime (\append{x}{g}) (\lambda\star.x))\\[3mm] \mathtt{postdoc} &: e \rightarrow t\\ \mathtt{postdoc} &= \textbf{pd}\\[3mm] \mathtt{cited} &: \mathcal{F}_\epsilon(e \rightarrow e \rightarrow t)\\ \mathtt{cited} &= \textbf{cite}^\eta\\[3mm] \mathtt{ashley} &: \mathcal{F}_\epsilon(e)\\ \mathtt{ashley} &= \textbf{a}^\eta \end{align*}\]

Additionally, we'll need versions of forward and backward Functional Application, which we present in terms of \(\mathtt{map}_{\mathcal{F}_l}\) and an operator \(\mu\) (called 'join'). This presentation is necessary for Haskell to infer the correct type for the application combinators and is equivalent to the presentation in terms of \(\bind\) and \((\cdot)^\eta\).

\[\begin{align*} \mu &: \mathcal{F}_{l_1}(\mathcal{F}_{l_2}(v)) \rightarrow \mathcal{F}_{l_1,l_2}(v)\tag{join}\\ \mu m &= m \bind \lambda n.n \end{align*}\]

-- | Graded monadic 'join'.
join :: F l1 (F l2 v) -> F (l1 :++ l2) v
join m = m >>= id

\[\begin{align*} (\triangleright) &: \mathcal{F}_{l_1}(v \rightarrow w) \rightarrow \mathcal{F}_{l_2}(v) \rightarrow \mathcal{F}_{l_1, l_2}(w)\tag{forward application}\\ m \triangleright n &= \mu\ (\mathtt{map}_{\mathcal{F}_{l_1}} (\lambda f.\mathtt{map}_{\mathcal{F}_{l_2}} (\lambda x.f x)\ n)\ m)\\[3mm] (\triangleleft) &: \mathcal{F}_{l_1}(v) \rightarrow \mathcal{F}_{l_2}(v \rightarrow w) \rightarrow \mathcal{F}_{l_1, l_2}(w)\tag{backward application}\\ m \triangleleft n &= \mu\ (\mathtt{map}_{\mathcal{F}_{l_1}} (\lambda x.\mathtt{map}_{\mathcal{F}_{l_2}} (\lambda f.f x)\ n)\ m) \end{align*}\]

-- | Forward application
(|>) :: F l1 (v -> w) -> F l2 v -> F (l1 :++ l2) w
m |> n = join $ fmap (\f -> fmap (\x -> f x) n) m

-- | Backward application
(<|) :: F l1 v -> F l2 (v -> w) -> F (l1 :++ l2) w
m <| n = join $ fmap (\x -> fmap (\f -> f x) n) m

Let's first look at example 1.

\[\begin{align*} &(\mathtt{every} \mathtt{postdoc})^\triangleright \triangleleft (\mathtt{cited} \triangleright \mathtt{herself})\\ =\ \ &(\mathtt{scope}^\prime_{(e \rightarrow t) \rightarrow t ⤚ e} (\lambda k.\forall x : \textbf{pd} x\ \rightarrow\ k x))^\triangleright \triangleleft (\mathtt{cited} \triangleright \mathtt{herself})\\ =\ \ &(\mathtt{scope}^\prime_{(e \rightarrow t) \rightarrow t ⤚ e} (\lambda k.\forall x : \textbf{pd} x\ \rightarrow k x))^\triangleright \triangleleft \mathtt{get}_{\star ⤚ \gamma}(\star; \lambda g.\textbf{cite} (\mathtt{sel} g))\\ =\ \ &\mathtt{scope}_{(e \rightarrow t) \rightarrow t ⤚ e} (\lambda k.\forall x : \textbf{pd} x\ \rightarrow k x)\\ &\hspace{1cm}(\lambda y.\mathtt{get}_{\star ⤚ \gamma}(\star; \lambda g.\mathtt{put}_{\gamma ⤚ \star}(\append{y}{g}; \lambda\star.\mathtt{get}_{\star ⤚ \gamma}(\star; \lambda g^\prime.\textbf{cite} (\mathtt{sel} g^\prime) y)))) \end{align*}\]

As we can see by inspecting the operations present in the resulting λ-term, the semantic type of 1 is \(\mathcal{F}_{(e \rightarrow t) \rightarrow t ⤚ e, \star ⤚ \gamma, \gamma ⤚ \star, \star ⤚ \gamma}\ \ (t)\). Its side effects are, in order, to invoke a quantifier meaning, read the environment, update the environment with the variable bound by the quantifier, and, finally, to read the environment again to do anaphora.

Example 2 composes in a similar way.

\[\begin{align*} &\mathtt{ashley}^\triangleright \triangleleft (\mathtt{cited} \triangleright \mathtt{herself})\\ =\ \ &\mathtt{ashley}^\triangleright \triangleleft \mathtt{get}_{\star ⤚ \gamma}(\star; \lambda g.\textbf{cite} (\mathtt{sel} g))\\ =\ \ &\mathtt{get}_{\star ⤚ \gamma}(\star; \lambda g.\mathtt{put}_{\gamma ⤚ \star}(\append{\textbf{a}}{g}; \lambda\star.\mathtt{get}_{\star ⤚ \gamma}(\star; \lambda g^\prime.\textbf{cite} (\mathtt{sel} g^\prime) \textbf{a}))) \end{align*}\]

In this case, the resulting type is simpler — \(\mathcal{F}_{\star ⤚ \gamma, \gamma ⤚ \star, \star ⤚ \gamma}\ (t)\) — as there is no quantifier. The environment is read, updated with \(\textbf{a}\), and then read again for anaphora.

Of course these "meanings" are not enough; we need to handle them! Doing so will produce ordinary State-monadic meanings, which we may associate with truth conditions. Fortunately, both sentences are of the right value type (\(t\)) to be handled. In the case of example 1, we wish to derive the following.

\[\mathtt{handleSentence}_{(e \rightarrow t) \rightarrow t ⤚ e, \star ⤚ \gamma, \gamma ⤚ \star, \star ⤚ \gamma}\ \ ((\mathtt{every} \mathtt{postdoc})^\triangleright \triangleleft (\mathtt{cited} \triangleright \mathtt{herself}))\]

There is not enough space here to show how the handler is computed, as well as provide the relevant β-reductions, so I'll leave that as an (extremely tedious) exercise for the reader. The simplified meaning which results, however, is the following one.

\[\mathtt{get}_{\star ⤚ \gamma}(\star; \lambda g.\mathtt{put}_{\gamma ⤚ \star}(g; \lambda\star.\forall x.\textbf{pd} x \rightarrow \textbf{cite} (\mathtt{sel} (\append{x}{g})) x))\]

This meaning is equivalent to the State monadic program \(\lambda g.\langle\forall x.\textbf{pd} x \rightarrow \textbf{cite} (\mathtt{sel} (\append{x}{g})) x, g\rangle\); as required, it is externally static.

Likewise, we wish to derive the following interpreted meaning for example 2.

\[\mathtt{handleSentence}_{\star ⤚ \gamma, \gamma ⤚ \star, \star ⤚ \gamma}\ \ (\mathtt{ashley}^\triangleright \triangleleft (\mathtt{cited} \triangleright \mathtt{herself}))\]

In this case, the simplified meaning which results is the following.

\[\mathtt{get}_{\star ⤚ \gamma}(\star; \lambda g.\mathtt{put}_{\gamma ⤚ \star}(\append{\textbf{a}}{g}; \lambda\star.\textbf{cite} (\mathtt{sel} (\append{\textbf{a}}{g})) \textbf{a}))\]

This meaning is equivalent to the State-monadic program \(\lambda g.\langle\textbf{cite} (\mathtt{sel} (\append{\textbf{a}}{g})) \textbf{a}, \append{\textbf{a}}{g}\rangle\); it is thus externally dynamic, in contrast to the meaning of example 1.