Cooper Storage and Type-Level Haskell

Dec 29 2018 (minor updates Jan 4 2019; type errors fixed Jan 28 2019)

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.

A demo of the Haskell implementation

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
                          ('Cons ((E -> Bool) -> Bool) ('Cons ((a0 -> Bool) -> c) store)))
                          ('Cons E (Cooper.TracesOf ('Cons ((a0 -> Bool) -> c) store)))
                        -> Bool)
        Actual type: Val
                       (HList (HListConcat 'Nil ('Cons ((E -> Bool) -> Bool) 'Nil)))
                             (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 ((some $$ boy) $$ (likes $$ (store (every $$ girl))))))

Type error! GHC was expecting retrieve to be applied to a semantic value with an (e → t) → t value in its store, but in fact the store was empty.

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 e → e → t with two values in its store. The first value in the store has type e and the second has type (e → t) → t. For each value in the store, the expression has a corresponding parameter whose type is determined by the type of the stored value. Following the usual practice, I've set things up so that e is the corresponding parameter type (or “trace type”) for both (e → t) → t and e.

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.

Background: the problem of quantifiers

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 e → t to intransitive verbs. A simple intransitive sentence like “John smokes” has the following analysis:

“John smokes.”

           1 iff j smokes
           = (λx . 1 iff x smokes)j
   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 e → t, the two can compose by function application. The denotation of the sentence is therefore 1 iff John smokes. (Really, we should define a class of models and specify the denotation of the sentence relative to a given model, but I'm trying to keep things as simple as possible here.)

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” using a curried denotation for “likes”:

“John likes Bill.”

             1 iff j likes b
             = (λy . 1 iff y likes b)j
  │                     λy . 1 iff y likes b= (λx . λy . 1 iff y likes x)be → 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 “No-one” in “No-one smokes” to see one respect in which it goes wrong.

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 “likes Bill” as an argument of “everyone” in “Everyone likes Bill”:

“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)
          │                                    λy . 1 iff y likes b= (λx . λy . 1 iff y likes x)be → 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

Cooper storage

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 x. 1 iff Bill likes x) to the denotation of “everyone”. But how can we derive this function when the object position of “likes” is occupied not by a variable but by “everyone”?

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 (1 iff Bill likes VAR) — we abstract over VAR to obtain x . 1 iff Bill likes x). Finally, we grab the denotation of “everyone” that we set aside earlier and feed our newly-created abstraction into it.

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 λg . j. The denotation of a variable is determined by the assignment. For example, the denotation of 𝓪 is λg . g (𝓪). Composition proceeds as before but with the assignment threaded through. Let

X ⊙ Y = λg . X g (Y g).

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” (λg . j) has type e, and the denotation of “likes” (λgxy . 1 iff y likes x) has type e → e → t. If X has type 𝜏 and Y has type 𝜏→𝜏′, then Y⊙X has type 𝜏′.

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:

(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:

store x = ⟨⟨⟨𝓪, x⟩⟩, 𝓪⟩      (where 𝓪 is a previously unused variable)
retrieve ⟨⟨⟨𝓪, v⟩, s1,…,sn⟩, x⟩ = ⟨s2,…,sn, v ⊙ λg . x  g [𝓪→x]⟩
where g [𝓪→x] = λv . x if v = 𝓪 else g v

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)((λgx . 1 iff b likes x)(g))⟩
              = ⟨⟨⟩,  (λg.λQ . 1 iff ∀x [x is a boy → Qx = 1]) ⊙ (λgx . 1 iff b likes x)⟩
        = ⟨⟨⟩,  (λg.λQ . 1 iff ∀x [x is a boy → Qx = 1]) ⊙ (λgx . (λ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]⟩⟩, λgy . 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⟩
                                   λgxy . 1 iff y likes xstoreevery boy
                                                                                        λg.λQ . 1 iff ∀x [x is a boy → Qx = 1]⟩
                                                                                        (e → t) → t

Making Cooper storage compositional

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:

store⟨⟨⟩, v ⟩ = ⟨⟨v ⟩,  λx . x⟩    (where v  has type (e → t) → t and x  has type e)

Before digging into the details, it's worth noting that most of what follows is an elaboration of the following two principles:

To begin with, take the case of composing “likes” with its object “every boy”. Applying store to (every boy) yields a value together with a single-element store. Ignoring the store for the moment, we can think of this value as a type e value parameterized by another type e value. (Parameters here are just regular function arguments, but it's useful to distinguish certain arguments that play a special role in the semantic composition.) The verb “likes” has a denotation of type e → e → t. If we had an individual to hand, we could use that individual to provide the parameter to the value yielded by store (every boy) and then feed the resulting individual to “likes”. Thus, we compose by adding another abstraction over individuals:

likes composed with store(every boy)
    = λa . likes(store(every boy) a)    [type e → e → t]

Now let's look at an example where store is applied twice:

store (some girl)  composed with  (likes  composed with  store(every boy))
    = store (some girl)  composed with  λa . likes(store(every boy) a)

We need to compose the value yielded by

store(some girl),

which has type e → e, with

a . likes(store(every boy) a))

which has type e → e → t. Each of these values has a single type e parameter. Logically, if A depends on parameter p and B depends on parameter q, then the combination of A and B should, in the general case, depend on p and q. We therefore compose by abstracting twice:

λbc . (store(some girl) b)((λa . likes(store(every boy) a))c)    [type e → e → t]

In general, if

then the composition of ⟨⟨s1sm⟩, A⟩ and ⟨⟨t1tn⟩, B⟩ is

⟨⟨s1sm,t1tn⟩,  λp1pm,q1qn . A(p1pm)(B(q1qn))⟩.

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 graded applicative functor, of which a vanilla applicative functor is a special case.2

The retrieve operation is defined as follows:

retrieve⟨⟨s1sn⟩, f ⟩ =⟨⟨s2sn⟩,  λp1pn-1 . s1q . f(q, p1pn-1)) ⟩

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.

Heterogenous lists in Haskell

There are a couple of reasons why stores and lists of parameters can't be modeled using ordinary Haskell lists:

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 ≥2-tuple. Nor can we write a function that takes an m-tuple and an n-tuple and returns a m+n-tuple (for arbitrary m and n).

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 l — in which case the HList 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 b is an HList parameterized by a ++ b.

We'll also need to be able to split an HList parameterized by a ++ b into two HLists with types HList a and HList 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

Modeling semantic composition in Haskell

We define a type class with three parameters to model semantic composition. An instance for ComposeWith a b c witnesses that a and b can be composed to obtain c. The canonical examples are the instances ComposeWith (a -> b) a b and ComposeWith a (a -> b) b. Functional dependencies are used to ensure that there can only be one instance of the form ComposeWith a b _ for any given 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
        :: 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:

    :: 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)

    :: (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))))
        stored = hListFirst store

Finally, we define the composition of Val s a with Val s b:

    :: ( 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 ->
                (p1, p2) = hListSplit ps
                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:

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.

Scope ambiguities

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 x [person(x) → likes(x, b)]. “Everyone” does not correspond to any constituent of this formula. Even if we make use of restricted quantification to nudge the syntax a little closer to English (∀x : person(x)[likes(x, b)]), we still have the problem that there is no non-ad-hoc way to assign interpretations separately to “x : person(x)” and “likes(x, b)”.

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.