Haskell programmers and linguists (particularly semanticists) share many of the same tastes in eseoterica. Continuations, linear logic and category theory each have interesting applications in both domains. A recent paper by Greg Kobele brings to light another connection. Greg shows that Cooper storage — a mechanism introduced in Cooper 1983 for interpreting quantificational noun phrases — can be implemented compositionally by lifting semantic values into a kind of applicative functor.
In this post I'll show how to use some of the ideas from Greg's paper to implement Cooper storage in type safe Haskell. Naturally, this requires using all sorts of fun GHC extensions. Key among these is the type families extension, which makes it easy to write functions from types to types.
The code is available
on github
and builds using stack. Run
stack ghci within the project dir to get an interactive prompt.
I should emphasize that I'm just pulling out one of many ideas in Greg's paper. The following is not a faithful definition-by-definition translation of the paper into Haskell.
I'll give some background on Cooper storage shortly. First let's look at the level of type safety achieved in the Haskell implementation. We can evaluate expressions like the following:
evalExample $ \Denots{ .. } -> retrieve ((some $$ boy) $$ (likes $$ (store (every $$ girl))))
==> True
This expression is a semantic analysis of “Some boy likes every
girl”.
The $$ operator indicates semantic
composition.
The interpretation derived is the one that
allows the boy in question to be different
for each girl. As it happens, the sentence is true under this interpretation in
the model I've defined.
GHC can infer the type of the expression:
:t composeExample $ \Denots{ .. } -> retrieve ((some $$ boy) $$ (likes $$ (store (every $$ girl))))
==> Val (HList 'Nil) (HList 'Nil -> Bool)
This is the type of a boolean semantic value with an empty store.
What happens if we remove the retrieve operation?
:t composeExample $ \Denots{ .. } -> ((some $$ boy) $$ (likes $$ (store (every $$ girl))))
composeExample $ \Denots{ .. } -> ((some $$ boy) $$ (likes $$ (store (every $$ girl))))
:: Val
(HList ('Cons ((E -> Bool) -> Bool) 'Nil))
(HList ('Cons E 'Nil) -> Bool)
As expected, GHCI infers that the semantic value has type (e → t) with one (e → t) → t value in its store.
What if we try to retrieve twice?
:t composeExample $ \Denots{ .. } -> (retrieve (retrieve ((some $$ boy) $$ (likes $$ (store (every $$ girl))))))
<interactive>:1:57: error:
• Couldn't match type ‘'Nil’
with ‘'Cons (TraceOf ((a0 -> Bool) -> c)) (Cooper.TracesOf store)’
Expected type: Val
(HList
('Cons ((E -> Bool) -> Bool) ('Cons ((a0 -> Bool) -> c) store)))
(HList
('Cons E (Cooper.TracesOf ('Cons ((a0 -> Bool) -> c) store)))
-> Bool)
Actual type: Val
(HList (HListConcat 'Nil ('Cons ((E -> Bool) -> Bool) 'Nil)))
(HList
(HListConcat
(Cooper.TracesOf 'Nil)
(Cooper.TracesOf ('Cons ((E -> Bool) -> Bool) 'Nil)))
-> Bool)
• In the first argument of ‘retrieve’, namely
‘((some $$ boy) $$ (likes $$ (store (every $$ girl))))’
In the first argument of ‘retrieve’, namely
‘(retrieve ((some $$ boy) $$ (likes $$ (store (every $$ girl)))))’
In the expression:
(retrieve
(retrieve ((some $$ boy) $$ (likes $$ (store (every $$ girl))))))
Type error! GHC was expecting retrieve to be applied to a semantic value with
an
A store can contain multiple values of different types.
A simple example can be constructed by uselessly putting a type e
value into storage. In the following semantic analysis of “John likes some boy”,
john is put into storage and then immediately retrieved:
evalExample $ \Denots{ .. } -> retrieve (retrieve (store john $$ (likes $$ (store (some $$ boy)))))
===> True
GHC can infer the type of the expression prior to the application of the retrieval operations:
:t composeExample $ \Denots{ .. } -> store john $$ (likes $$ (store (some $$ boy)))
composeExample $ \Denots{ .. } -> store john $$ (likes $$ (store (some $$ boy)))
:: Val
(HList ('Cons E ('Cons ((E -> Bool) -> Bool) 'Nil)))
(HList ('Cons E ('Cons E 'Nil)) -> Bool)
This is a semantic value of type
The connection between store types and parameter types is enforced at the type
level. If, for example, we modify the type of the first parameter to Int, then
the resulting type can't even be constructed:
:t Val (undefined :: (HList ('Cons E ('Cons ((E -> Bool) -> Bool) 'Nil)))) (undefined :: (HList ('Cons E ('Cons E 'Nil)) -> Bool))
===> [no error message]
:t Val (undefined :: (HList ('Cons E ('Cons ((E -> Bool) -> Bool) 'Nil)))) (undefined :: (HList ('Cons Int ('Cons E 'Nil)) -> Bool))
===> Couldn't match type ‘E’ with ‘Int’ [...]
There is also a type-level constraint requiring store to apply only to values
with empty stores. Thus, store (store john) fails to type check.
This section is a brief introduction to generalized quantifiers, and to various mechanisms that have been proposed for interpreting quantificational objects. It's mostly Semantics 101 stuff that linguists will already be familiar with.
Quantificational noun phrases like “every man” or “most dancers” have
the same
syntactic distribution as referential noun
phrases like “John”. In a toy semantics,
referential noun phrases denote individuals and verbs denote
predicates of one or more individuals. Writing e for the type of individuals
and t for the type of truth values, we assign the type e to
referential noun phrases and the type
“John smokes.”
1 iff j smokes
= (λx . 1 iff x smokes)j
t
┌──────┴──────┐
John smokes
j λx . 1 iff x smokes
e e → t
“John” denotes a particular individual (written j in the metalanguage). “Smokes”
denotes the function from individuals to truth values that maps all and only
the individuals who smoke to truth (written 1 in the metalanguage).
Composition is type driven. Since “John” has type e and “smokes” has type
It's easy enough to extend our toy semantics to handle transitive verbs.
There is strong evidence that the verb and its object form a
constituent that excludes the subject. We thus
interpret
“John likes Bill.”
1 iff j likes b
= (λy . 1 iff y likes b)j
t
┌──────────┴──────────┐
│ λy . 1 iff y likes b
│ = (λx . λy . 1 iff y likes x)b
│ e → t
│ ┌─────────┴──────────┐
John likes Bill
j λx . λy . 1 iff y likes x b
e e → e → t e
So far so good. But
what denotation should we assign to a quantificational subject such as “every boy”?
Linguists — who already know the right answer — can easily
forget that the first ideas that spring to mind tend to be very bad ones.
For example, we might suppose that “everyone”
denotes the set of all people, and then define “likes” in such a way
that likes(y)(X) holds for any set X and individual y such that for all x in X,
x likes y. We could extend this bad analysis to expressions
like “someone” by taking the denotation of “someone” to be a proper subset of
the set of people.
Geach (1968) notes that “quantificatious” analyses along these
lines persisted well into the 1950s in informal logic textbooks. Try extending
the analysis to
Richard Montague's seminal 1973 paper “The Proper Treatment of Quantification
in Ordinary English” proposed to treat quantificational noun phrases as
generalized quantifiers.
A generalized quantifier is a predicate of
predicates of individuals.
The generalized quantifier analysis treats
“Everyone likes Bill.”
1 iff ∀x [x likes b]
= 1 iff ∀x [(1 iff x likes b) = 1]
= 1 iff ∀x [(λy . 1 iff y likes b)x = 1]
= (λP . 1 iff ∀x [Px = 1])(λy . 1 iff y likes b)
t
┌──────────┴─────────────────────────┐
│ λy . 1 iff y likes b
│ = (λx . λy . 1 iff y likes x)b
│ e → t
│ ┌─────────┴──────────┐
everyone likes Bill
λP . 1 iff ∀x [Px = 1] λx . λy . 1 iff y likes x b
(e → t) → t e → e → t e
Montague's analysis is appealing because it allows us both to get the right interpretation and to assign an interpretation to each part of the sentence. (Doing one or the other is relatively easy — it's trying to do both at once that usually trips people up.) This is something that we could not achieve within the confines of first-order predicate logic.1
So far, so good. But what if we have a quantificational expression in object position? It no longer seems possible to compose the verb with the object:
“Bill likes everyone.”
???
┌──────────┴──────────────┐
│ ???
│ ┌─────────┴──────────────┐
Bill likes everyone
b λx . λy . 1 iff y likes x λP . 1 iff ∀x [Px = 1]
e e → e → t (e → t) → t
(Montague's system in fact had no problem with “Bill likes everyone”, but it did need some extra machinery to deal with the ambiguity of e.g. “Some student attended every class.” In the interests of concision, I'm going to anachronistically motivate Cooper storage with reference to the simpler case.)
What we really want to do is pass the function
The basic idea behind
Cooper storage is as follows. At the point when “likes” and “everyone” compose, we
insert a type e variable in place of “everyone”, setting aside the
real denotation of “everyone” for later. Once “Bill”
has composed with “likes everyone” — to yield something like
To implement this idea, we'll need a means of composing values containing free
variables in such a way
that these variables may later be bound. One way to do this is to analyze the
denotation of every node as a function of an assignment. An assignment is
a function from variables 𝓪, 𝓫, 𝓬… to individuals. The denotation of everything
we've seen so far is assignment-invariant. For example, the denotation of
“John”, formerly j, is now the constant function
The ⊙ operation now takes the place of function application as the primary
mode of semantic composition. As everything is now parameterized
by assignments, we won't include assignments in types. For example, the
denotation of “John” (
For present purposes we can treat stores as lists of variables paired with assignment-parameterized generalized quantifiers. For every existing type 𝜏, we add a new type ⟨s,𝜏⟩, where s is the type of a store. We add the following composition rules:
If
If
If
(We could use only the last rule and add a bunch of empty stores, but this adds clutter.)
In addition to the preceding rules we have two special rules for storing values and then retrieving them again:
We're now ready to give an analysis of a sentence with a quantificational expression in object position:
“Bill likes every boy.”
⟨⟨⟩, λg . 1 iff ∀x [x is a boy → b likes x]⟩
= ⟨⟨⟩, λg . 1 iff ∀x [x is a boy → (1 iff b likes x) = 1]⟩
= ⟨⟨⟩, λg . 1 iff ∀x [x is a boy → (λx . 1 iff b likes x)x = 1]⟩
= ⟨⟨⟩, λg . (λQ . 1 iff ∀x [x is a boy → Qx = 1])(λx . 1 iff b likes x)⟩
= ⟨⟨⟩, λg . (λg.λQ . 1 iff ∀x [x is a boy → Qx = 1])(g)((λg.λx . 1 iff b likes x)(g))⟩
= ⟨⟨⟩, (λg.λQ . 1 iff ∀x [x is a boy → Qx = 1]) ⊙ (λg.λx . 1 iff b likes x)⟩
= ⟨⟨⟩, (λg.λQ . 1 iff ∀x [x is a boy → Qx = 1]) ⊙ (λg.λx . (λg . 1 iff b likes g(𝓪))(g[𝓪→x]))⟩
t (with empty store)
│
retrieve
│
⟨⟨⟨𝓪, λg.λQ . 1 iff ∀x [x is a boy → Qx = 1]⟩⟩, λg . 1 iff b likes g(𝓪)⟩
⟨s, t⟩
┌───────────────────────────────┴─────────────────────────────┐
Bill ⟨⟨⟨𝓪, λg.λQ . 1 iff ∀x[x is a boy → Qx = 1]⟩⟩, λg.λy . 1 iff y likes g(𝓪)⟩
λg . b ⟨s, e → t⟩
e ┌──────────────────────┴─────────────────────┐
likes ⟨⟨⟨𝓪, (λg.λQ . 1 iff ∀x [x is a boy → Qx = 1])⟩⟩, λg . g(𝓪)⟩
e → e → t ⟨s,e⟩
λg.λx.λy . 1 iff y likes x │
store
│
every boy
λg.λQ . 1 iff ∀x [x is a boy → Qx = 1]⟩
(e → t) → t
Greg notes in his paper that one of the less attractive features of Cooper storage is that it necessitates manipulating expressions containing free variables. One can do this “compositionally” in a rather artificial way using assignments, but it would be preferable to do without this additional machinery.
As things stand, storing a generalized quantifier yields an type e value. Greg's paper describes a system where storing a generalized quantifier yields an e → e value. Rather than waiting until the application of retrieve to add the λ that binds the variable, we introduce the λ at the moment of storage and then percolate the λ up through each step of the semantic composition. It is no longer necessary to pair each item in the store with a variable. For the case where the stored value is a generalized quantifier, store can be defined as follows:
Before digging into the details, it's worth noting that most of what follows is an elaboration of the following two principles:
If A has parameters p1, ..., pm, and B has parameters, q1, ..., qn, then an expression composed of A and B has parameters p1, ...pm, q1, ..., qn.
If A has values s1, ..., sm in its store, and B has values t1, ..., tn in its store, then an expression composed of A and B has values s1, ..., sm, t1, ..., tn in its store.
To begin with, take the case of composing “likes” with its
object
Now let's look at an example where store is applied twice:
We need to compose the value yielded by
which has type
which has type
In general, if
then the composition of ⟨⟨s1…sm⟩, A⟩ and ⟨⟨t1…tn⟩, B⟩ is
We now begin to see the structure of an
applicative functor.
We have a trivial lift operation that lifts values into the
functor: simply pair the value with an empty store.
And the composition operation we've just defined gives us
a means of composing values in the case where
one of the unlifted values is a function that can be
applied to the other. This an operation analogous to
(<*>).
As Greg explains, what we have here doesn't strictly qualify as an applicative
functor because of the restrictions on composition imposed by the types of
the values in the store. It is, however,
a
The retrieve operation is defined as follows:
The basic idea here is that retrieving a value from the store removes that item from the store and also removes the corresponding parameter. We remove the parameter by abstracting over n−1 parameters and then wrapping the argument passed to the stored value with an abstraction over the “missing” parameter.
There are a couple of reasons why stores and lists of parameters can't be modeled using ordinary Haskell lists:
The lists aren't homogenous. Values of different types can be in the store, and parameters can have different types.
The number of parameters must equal the number of items in storage (and we want this constraint to be enforced at the type level).
Might a tuple rather than a list be the
appropriate data structure?
The problem with tuples is that Haskell doesn't allow us to write
code that's parametric over the number of elements in a tuple. We can't, for
example, write a function
that returns the second element of its tuple argument for any
A heterogenous list, or HList, is a data structure that has some of the properties of tuples and some of the properties of ordinary Haskell lists. As with a tuple, the type of an HList determines the type of every member, and each element may have a different type. But as with a list, we can write polymorphic functions that perform such operations as taking the first element of an HList, or concatenating two HLists.
The type of an HList is parameterized by a list of
types.
For example,
the HList
[1::Int, "Foo"] has the type HList [Int, String] (taking some liberties
with Haskell syntax).
There's a minimal implementation of HLists in
HList.hs.3
Let's take a look at the definition of the HList type itself and
a function to concatenate HLists:
data List a = Nil | Cons a (List a)
data HList (l::List *) where
HNil :: HList Nil
HCons :: e -> HList l -> HList ('Cons e l)
type family HListConcat (a::k) (b::k) :: k where
HListConcat 'Nil a = a
HListConcat ('Cons a xs) ys = 'Cons a (HListConcat xs ys)
hListConcat :: HList a -> HList b -> HList (HListConcat a b)
hListConcat HNil xs = xs
hListConcat (HCons a xs) ys = HCons a (hListConcat xs ys)
This code uses the DataKinds extension to lift types to kinds.
By prefixing the constructors for List with ', we can
create lists at the type level. The definition of HList states that an HList
is either HNil — in which case the HList type is parameterized by an empty
type list — or HCons e lHList type is parameterized by
the type list consisting of e followed by l.
Concatenation of HLists is defined both at the type level and the value level.
The value-level definition (hListConcat) should be familiar. The type level
definition makes use of the TypeFamilies extension to define a type-level
function that concatenates lists of types.
The type for hListConcat states that the concatenation of two HLists
parameterized by type lists a and ba ++ b
We'll also
need to be able to split an HList parameterized by a ++ bHLists
with types HList aHList b
class HListSplit (a::List *) (b::List *) where
hListSplit :: HList (HListConcat a b) -> (HList a, HList b)
instance HListSplit 'Nil a where
hListSplit xs = (HNil, xs)
instance HListSplit b c => HListSplit ('Cons a b) c where
hListSplit (HCons x xs) =
(HCons x as, bs)
where (as, bs) = hListSplit xs
We define a type class with three parameters to model semantic composition.
An instance for ComposeWith a b ca and b
can be composed to obtain c. The canonical examples are the instances
ComposeWith (a -> b) a bComposeWith a (a -> b) bComposeWith a b _a, b. This makes
semantic composition deterministic.
class ComposeWith a b c | a b -> c where
composeWith :: a -> b -> c
instance ComposeWith (a -> b) a b where
composeWith = id
instance ComposeWith a (a -> b) b where
composeWith = flip id
We are free to add additional instances of ComposeWith. For example, the
following instance allows composition via predicate modification:
instance ComposeWith (a -> Bool) (a -> Bool) (a -> Bool) where
composeWith p1 p2 x = p1 x && p2 x
We'll also need to define the relation between types and their traces. This can be done in an extensible way using type families:
class HasTrace a where
type TraceOf a :: *
instance HasTrace ((E -> Bool) -> Bool) where
type TraceOf ((E -> Bool) -> Bool) = E
instance HasTrace E where
type TraceOf E = E
As well as mapping types to their traces, we'll also want to map lists of types to lists of the corresponding traces:
class TraceList (a :: List *) where
type TracesOf a :: List *
instance TraceList 'Nil where
type TracesOf 'Nil = 'Nil
instance HasTrace x => TraceList ('Cons x xs) where
type TracesOf ('Cons x xs) = ('Cons (TraceOf x) (TracesOf xs))
The type of semantic values is defined as follows:
data Val s a where
Val
:: TraceList s
=> HList s
-> (HList (TracesOf s) -> b)
-> Val (HList s) ((HList (TracesOf s)) -> b)
The constructor takes two arguments. The first is a store: an HList of values whose types have trace types. The second is a function from an HList of parameters to a value. The type of each parameter is the trace of the type of the corresponding item in the store. The store and the parameter list therefore have the same length.
Stores, and hence parameter lists, may be empty. (I
elided empty stores in the presentation above, but doing so would add
unnecessary complexity to the Haskell
implementation.) We lift a value into Val by wrapping it in a
thunk that ignores its argument
and then pairing this thunk with an empty store:
lift :: a -> Val (HList 'Nil) (HList 'Nil -> a)
lift v = Val HNil (\_ -> v)
The definitions of store and retrieve are fairly transparent:
store
:: HasTrace a
=> Val (HList 'Nil) (HList 'Nil -> a)
-> Val (HList ('Cons a 'Nil)) (HList ('Cons (TraceOf a) 'Nil) -> TraceOf a)
store (Val store a) =
Val (HCons (a HNil) HNil) (\(HCons x _) -> x)
retrieve
:: (TraceList store, ComposeWith s (p -> t) r)
=> Val (HList ('Cons s store)) (HList ('Cons p (TracesOf store)) -> t)
-> Val (HList store) (HList (TracesOf store) -> r)
retrieve (Val store v) =
Val (hListRest store)
(\ps -> composeWith stored (\x -> (v (HCons x ps))))
where
stored = hListFirst storeFinally, we define the composition of Val s a with Val s b:
compose
:: ( ComposeWith f a r
, HListSplit store1 store2
, HListSplit (TracesOf store1) (TracesOf store2)
, TraceList store1, TraceList store2
, TraceList (HListConcat store1 store2)
, HListConcat (TracesOf store1) (TracesOf store2)
~ TracesOf (HListConcat store1 store2)
)
=> Val (HList store1) (HList (TracesOf store1) -> f)
-> Val (HList store2) (HList (TracesOf store2) -> a)
-> Val (HList (HListConcat store1 store2))
(HList (HListConcat (TracesOf store1) (TracesOf store2)) -> r)
compose (Val store1 f1) (Val store2 f2) =
Val (hListConcat store1 store2)
(\ps ->
let
(p1, p2) = hListSplit ps
in
composeWith (f1 p1) (f2 p2)
)
-- ...a type annotation is needed for this to compile, but is elided here...
($$) = compose
infixr 1 $$
Here we have to help GHC's type inferer out in a couple of respects:
We add TraceList (HListConcat store1 store2) in addition to
TraceList store1, TraceList store2. Each constraint entails the other
(I think), but
GHC cannot infer this automatically.
We add
HListConcat (TracesOf store1) (TracesOf store2) ~ TracesOf (HListConcat store1 store2).
This
type equality constraint
informs GHC that applying TracesOf to two lists of types and then
concatenating the results has the same effect as concatenating the two lists
and then applying TracesOf to the result.
In the body of the function,
the store of the resulting semantic value is set to the
concatenation of the stores of the original two values. The list
of parameters is split in two. The first sublist is passed to the first value
and the second to the second. The splitting point
is determined by the types. If, for example, the first value has a single
type e parameter while the second has two type e parameters, then p1 must
contain the first element of ps and p2 must contain the last two elements
of ps.
Sentences with multiple quantificational noun phrases often exhibit scope ambiguities. For example, “Some reviewer likes every paper” can mean either that there is a single reviewer who likes all the papers, or that for every paper, there is at least one reviewer who likes it. To derive both interpretations of such a sentence, we need to be able to retrieve either item from a store containing two items. The order in which the quantifiers are retrieved determines their relative scope.
It would be an interesting exercise to write a generalized version of
retrieve that takes an index into the store as a
type-level parameter. For the purposes of linguistic semantics, it
is only ever necessary to retrieve the third or perhaps the fourth item in a
store.
For the moment I've simply defined
retrieve2,
retrieve3
and
retrieve4
in addition to retrieve.
Another way to go here would be to define a separate set of store-permuting
operations analogous to swap, rot etc. from Forth.
1. The standard FoL paraphrase of
“Everyone likes Bill” is
2. An earlier version of this post referred to parameterized applicative functors. Greg Kobele informs me that the accepted term is now graded.
3. There's a comprehensive HList library on Hackage. As HLists are quite simple to implement using type families, I've not used this package in my code. I believe the HList package originated before type families were available, so that the implementation of an HList structure required a fair amount of type wizardry.
Cooper, R. 1983. Quantification and Syntactic Theory. D. Reidel: Dordrecht.
Geach, P. 1968. A History of the Corruptions of Logic: An Inaugural Lecture. Reprinted in Logic Matters. University of California Press. 1972.
Kobele, G. 2018. The Cooper Storage Idiom. Journal of Language, Logic and Information 27:95-131.
Montague, R. 1973. The Proper Treatment of Quantification in Ordinary English. In Thomason, R. (ed.) Formal Philosophy. New Haven: Yale University Press, pp. 247–270.