Continuation semantics
Table of Contents
1. Overview
Starting with Philippe de Groote's work, a rich literature in formal semantics
has developed which relies on continuation passing to model the
truth-conditional contributions of quantifiers, like some dog and every
linguist. Since de Groote's analysis, most work has focused on what are known
as delimited or composable continuations; in particular, Chris Barker and
Ken Shan's work (e.g., check out their 2014 book, but also Barker 2003 for
something a little shorter). Composable continuations have some fixed result
type, so that the meanings of natural language expressions can be modeled as
functions of type
2. Interpreting via continuations in Haskell
Recall our type family SemType
, which takes grammatical categories of
applicative categorial grammar onto types of the λ-calculus:
type family SemType (c :: Cat) where SemType NP = E SemType N = E :-> T SemType S = T SemType (c1 :\: c2) = SemType c1 :-> SemType c2 SemType (c2 :/: c1) = SemType c1 :-> SemType c2
In terms of this map, we may implement a function interpExpr
, which takes
expressions of English onto λ-terms of continuized types. Rather than map an
expression of category c
directly onto its semantic type, we map it onto a
closed term of type (SemType c :-> T) :-> T
, using continuized functional
application:
interpExpr :: Expr c -> Term Empty ((SemType c :-> T) :-> T) interpExpr (Lex w) = interpWord w interpExpr (AppL e1 e2) = Lam (App (weaken (interpExpr e1)) (Lam (App (weaken (weaken (interpExpr e2))) (Lam (App (Var (Next (Next First))) (App (Var First) (Var (Next First)))))))) interpExpr (AppR e1 e2) = Lam (App (weaken (interpExpr e1)) (Lam (App (weaken (weaken (interpExpr e2))) (Lam (App (Var (Next (Next First))) (App (Var (Next First)) (Var First)))))))
To interpret individual words (though note that we're considering some dog a
word for our purposes - try to think about what difficulties we encounter if
we try to compose every with dog using our current system), we may write a
function interpWord
taking words of some category c
onto closed terms of type
(SemType c :-> T) :-> T
:
interpWord :: Word c -> Term Empty ((SemType c :-> T) :-> T) interpWord (Word "some dog" IsAnNP) = Lam (App (Con Exists) (Lam (App (App (Con And) (App (Con Dog) (Var First))) (App (Var (Next First)) (Var First))))) interpWord (Word "barks" (IsAnNP ::\:: IsAnS)) = Lam (App (Var First) (Con Bark))
Note that for this to be well typed, our constants should have the following types:
data Constant (φ :: Type) where Exists :: Constant ((E :-> T) :-> T) And :: Constant (T :-> (T :-> T)) Dog :: Constant (E :-> T) Bark :: Constant (E :-> T)
Footnotes:
Note that the forward variant just
switches the binders