Presuppositions as Haskell type class constraints, or Agda instance arguments

[Darryl McAdams]

in modern functional programming languages such as Haskell, it's often useful to have polymorphic functions which apply generically to any type, subject to constraints on that type.

for instance, in Haskell we can define the following function (at the designated type indicated on the first line -- haskell uses :: for type signatures):

    double :: forall a. Monoid a => a -> a

    double x = mappend x x

this function takes any value x, of type a, and appends x to itself using the mappend function. The "Monoid a" type class constraint in the type signature is Haskell's way of saying that this doesn't work for any old type a, but rather it only works for a's that are Monoids, and which thus support the mappend function. in this way, "Monoid a" is sort of like a presupposition that `a' is a monoid. The way Haskell makes this work is actually quite straight forward: types that look like "C => T" for some constraint C and some type T are secretly just function types from C to T, so secretly, the above function really has the type

    double :: forall a. Monoid a -> a -> a

when it gets uses, the *type checker* supplies the "Monoid a" argument automatically by searching the program context for an appropriate witness to the claim that `a' is a monoid. Agda has a similar feature: instead of writing "C => T" you would write "{{c : C}} -> T", to create a depending function from C to T with a type-checker-supplied argument for C (the {{...}} indicates type-checker-supplied-ness). but because Agda has full dependent types, we can say all sorts of interesting things, such as this:

    Know : (P : Proposition) -> {{proofOfP : P}} -> Entity -> Proposition

***note: in agda, we would write (x : A) -> B instead of the usual dependent type Πx:A.B. it's just notation, but suggests that its a dependent _function_ type more readily that Π does***

this type captures the fact the word "know" presupposes its clausal argument is true, so the proposition

    Know (Tall frank) susan

would mean that Susan knows Frank is tall, with a secretly supplied proof that "Tall frank" is true. this is handled as in Haskell, by having this expand out in the type-checker to something like this:

    Know (Tall frank) {{tcs}} susan

where tcs is the type-checker-supplied proof of "Tall frank". but prior to the type checker supplying the proof, there is actually an intermediate form of the proposition with a hole in place of that proof, which we can write as

    Know (Tall frank) {{ ?0 }} susan

the type checker then lists all of the holes -- in this case just   ?0 : Tall frank   -- together with the variable context that they appear in. ?0 appears under no binders, so the variable context is empty, modulo whatever initial content the context has. If the initial context does in fact contain a proof of "Tall frank", because the speaker believes that to be true, then the type checker can look up that proof -- what i called `tcs' -- and supply it as the value for the goal ?0.

we can also use this for pronouns, as well. we could, for instance, imagine that the pronoun "she" has the type and definition

    she : {{x : Entity}} -> Entity

    she = λ{{x}}. x

which is to say, pronouns are identity functions (as the categorial grammar tradition often suggests), except the arguments are supplied by the type checker. consider now the sentence "every girl thinks she is tall", with the (first pass) semantics

    (x : Entity) -> Girl x -> Thinks x (Tall she)

because `she' has an implicit argument, the type checker would expand this out with a new hole like so:

    (x : Entity) -> Girl x -> Thinks x (Tall (she {{ ?1 }}))

which it must now supply. ?1 has the type Entity, since what must be supplied is an entity. the current variable context that ?1 appears in is in fact inside a binder: the depending function binder (x : Entity), so the context for ?1 is "x : Entity", together with whatever globally supplied things exist. notice now that not only are we "presupposing" propositions like "Tall frank", but also things such as `x'. this is more or less what DRT and dynamic implication get us.

so now when the type checker has to solve for ?1 : Entity, it can look into the context for ?1, and it finds `x', yielding

    (x : Entity) -> Girl x -> Thinks x (Tall (she {{x}}))

after beta reduction:

    (x : Entity) -> Girl x -> Thinks x (Tall x)

and hey presto, every girl thinks she's tall! this sort of thing works for donkey anaphora as well, but may have difficulties with bach-peters sentences (depending on how you translate from the syntax to the semantics).

also probably we wouldn't want to actually use the variable context for the solutions to holes like ?0 and ?1, but rather a separate, but similarly defined, discourse context. certain problems arise from using the variable context together with a naive solver to find solutions to holes which a proper discourse context could mitigate.

[Darryl McAdams]

possible an alternative to this is, instead of having presuppositions in the type, as in

    she : {{x : E}} -> {{f : Fem x}} -> E

    she = λ{{x : E}}. λ{{f : Fem x}}. x

it might be preferable to have something like

    she : E

    she = require x : E in (require f : Fem x in x)

which would serve a similar purpose, but which would be more straightforward in both the type system and the elaboration system that manages/solves presuppositions