{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ScopedTypeVariables #-}
-- Proper treatment of quantification in the language
-- of denotations. Building denotations in CPS.
-- This is the code accompanying the paper on quantifier-scope
-- and quantifier ambiguity.
module QuanCPS where
import Prelude hiding (max)
-- The language to build denotations: the language DQ
-- The type is annotated with the depth of its environment
-- for free variables. Z means the term is closed.
-- Basic types
data E
data T
-- Levels of environment
data Z = Z
data S n = S n
class Nat n where nat :: n -> Int
instance Nat Z where nat _ = 0
instance Nat n => Nat (S n) where nat _ = 1 + nat (undefined::n)
-- Maximum of two numerals
type family Max n1 n2 :: *
type instance Max Z n2 = n2
type instance Max (S n1) Z = S n1
type instance Max (S n1) (S n2) = S (Max n1 n2)
-- The language itself
class DQ r where
john' :: r Z E
mary' :: r Z E
see' :: r Z (E -> E -> T)
app :: r n1 (a->b) -> r n2 a -> r (Max n1 n2) b
-- Quantification. We use de Bruijn *levels* (not indices!)
-- If forall body :: r n T, then forall quantifies the variable
-- whose name (level) is `n'.
var :: Nat n => n -> r (S n) E
forall :: Nat n => r (S n) T -> r n T
exists :: Nat n => r (S n) T -> r n T
-- sample variables
var0 = var Z
var1 = var (S Z)
var2 = var (S (S Z))
-- Forward and backward applications
($>) = app
($<) = flip app
-- Sample sentences
ts1 = john' $< (see' $> mary')
-- ts1 :: DQ r => r Z T
ts2 = forall (var0 $< (see' $> mary'))
-- ts2 :: DQ r => r Z T
-- The derived type says ts3 is open!
ts3 = forall (var1 $< (see' $> mary'))
-- ts3 :: DQ r => r (S Z) T
ts4 = exists (forall (var0 $< (see' $> var1)))
-- ts4 :: DQ r => r Z T
-- The instance of DQ to show its terms
newtype C n a = C (TranC a)
type family TranC a :: *
type instance TranC E = String
type instance TranC T = String
type instance TranC (a ->b) = TranC a -> TranC b
instance DQ C where
john' = C "john'"
mary' = C "mary'"
see' = C (\o s -> "see'(" ++ o ++ ")(" ++ s ++ ")")
app (C f) (C x) = C (f x)
var _ = r where r = C (num_to_var r)
forall x@(C e) = C ("forall " ++ num_to_var x ++ ". (" ++ e ++ ")")
exists x@(C e) = C ("exists " ++ num_to_var x ++ ". (" ++ e ++ ")")
num_to_var :: forall n a. Nat n => C n a -> String
num_to_var _ = vars !! (nat (undefined::n) - 1)
where vars = ["x","y","z","u","v","w"] ++ map (\n -> "x" ++ show n) [1..]
-- Only closed terms of type T -- sentences -- can be `run'
runC :: C Z T -> String
runC (C x) = x
ts1r = runC ts1
-- "see'(mary')(john')"
ts2r = runC ts2
-- "forall x. (see'(mary')(x))"
-- ts3r = runC ts3 : not closed, can't be shown
ts4r = runC ts4
-- "exists x. (forall y. (see'(y)(x)))"
-- ------------------------------------------------------------------------
-- The calculus of CPS
lift v = \k -> k v -- also called `return' or `pure'
john = lift john'
mary = lift mary'
saw = lift see'
-- Application lifted to CPS
f $$> x = \k -> f (\fv -> x (\xv -> k (fv $> xv)))
x $$< f = \k -> x (\xv -> f (\fv -> k (fv $> xv)))
-- Bind
f $$>> x = \k -> x (\xv -> f xv k)
x $$<< f = \k -> x (\xv -> f xv k)
runCPS e = e id
sen1C = john $$< (saw $$> mary)
sen1Cr = runC . runCPS $ sen1C
-- "see'(mary')(john')"
-- Quantifiers
-- The signature is of great importance! It ensures against the variable
-- `confusion'. Whatever variable the quantifier passes to its
-- continuation, the same variable will be quantified:
-- the level (S n) in r (S n) E determines the name of the variable.
-- The level (S n) in r (S n) T determines the name of the variable
-- bound by the quantifier.
-- The types ensure that multiple occurrences of the quantifier
-- do not `step on each other toes' and automatically `advance' the
-- variable counter. In the examples below, see e.g., sQ5,
-- the types are all inferred. The names are chosen automatically
-- (the names follow control effects, so to speak).
everyone, someone :: (DQ r, Nat n) => (r (S n) E -> r (S n) T) -> r n T
everyone = \k -> forall (k (var undefined))
someone = \k -> exists (k (var undefined))
-- sQ1 :: (Nat n, DQ r) => (r (S n) T -> r (S n) T) -> r n T
sQ1 = everyone $$< (saw $$> mary)
sQ1r = runC . runCPS $ sQ1
-- "forall x. (see'(mary')(x))"
-- sQ2 :: (Nat n, DQ r) => (r (S n) T -> r (S n) T) -> r n T
sQ2 = john $$< (saw $$> everyone)
sQ2r = runC . runCPS $ sQ2
-- "forall x. (see'(x)(john'))"
-- The inferred type shows that two quantifiers are used...
-- sQ5:: (Nat n, DQ r) => (r (S (Max (S n) n)) T -> r (S (S n)) T) -> r n T
sQ5 = someone $$< (saw $$> everyone)
sQ5r = runC . runCPS $ sQ5
-- "exists x. (forall y. (see'(y)(x)))"
-- ------------------------------------------------------------------------
-- The calculus of CPS2
-- Initial continuations and meta-continuations
theta v k = k v
theta_final v = v
runCPS2 e = e theta theta_final
reset1 e = \k1 k2 -> e theta (\v -> k1 v k2)
reset2 = lift . runCPS2
sen1Cr2 = runC . runCPS2 $ sen1C
-- These are the same as everyone and someone before, but written
-- in CPS
-- The type below is general and works at the higher CPS levels.
everyone1, someone1 :: (Nat n, DQ r) =>
(r (S n) E -> (r (S n) T -> a) -> b) -> (r n T -> a) -> b
everyone1 = \k1 k2 -> k1 (var undefined) (\v -> k2 (forall v))
someone1 = \k1 k2 -> k1 (var undefined) (\v -> k2 (exists v))
-- repeating the previous derivations, in CPS2
-- sQ11 :: (Nat n, DQ r) =>
-- (r (S n) T -> (r (S n) T -> r l1 T) -> r l2 T)
-- -> (r n T -> r l1 T) -> r l2 T
sQ11 = everyone1 $$< (saw $$> mary)
sQ11r = runC . runCPS2 $ sQ11
-- "forall x. (see'(mary')(x))"
sQ12 = john $$< (saw $$> everyone1)
sQ12r = runC . runCPS2 $ sQ12
-- "forall x. (see'(x)(john'))"
-- sQ15 :: (Nat n, DQ r) =>
-- (r (S (Max (S n) n)) T -> (r (S (S n)) T -> r l1 T) -> r l2 T)
-- -> (r n T -> r l1 T) -> r l2 T
sQ15 = someone1 $$< (saw $$> everyone1)
sQ15r = runC . runCPS2 $ sQ15
-- "exists x. (forall y. (see'(y)(x)))"
-- Level-2 quantifiers
everyone2, someone2 :: (DQ r, Nat n) =>
(r (S n) E -> k2 -> r (S n) T) ->
k2 -> r n T
everyone2 = \k1 k2 -> forall (k1 (var undefined) k2)
someone2 = \k1 k2 -> exists (k1 (var undefined) k2)
-- sQ21 :: (Nat n, DQ r) => (r (S n) T -> k2 -> r (S n) T) -> k2 -> r n T
sQ21 = everyone2 $$< (saw $$> mary)
sQ21r = runC . runCPS2 $ sQ21
-- "forall x. (see'(mary')(x))"
sQ22 = john $$< (saw $$> everyone2)
sQ22r = runC . runCPS2 $ sQ22
-- "forall x. (see'(x)(john'))"
-- sQ23 :: (Nat n, DQ r) =>
-- (r (S (Max (S n) n)) T -> k2 -> r (S (S n)) T) -> k2 -> r n T
sQ23 = someone2 $$< (saw $$> everyone2)
sQ23r = runC . runCPS2 $ sQ23
-- "exists x. (forall y. (see'(y)(x)))"
-- sQ24 :: (Nat n1, Nat n, DQ r) =>
-- (r (S (Max n1 n)) T -> (r (S n1) T -> r l1 T) -> r (S n) T)
-- -> (r n1 T -> r l1 T) -> r n T
sQ24 = someone2 $$< (saw $$> everyone1)
sQ24r = runC . runCPS2 $ sQ24
-- "exists x. (forall y. (see'(y)(x)))"
-- The type of sQ25 differs from the type of sQ24
-- sQ25 :: (Nat l2, Nat n, DQ r) =>
-- (r (S (Max l2 n)) T -> (r (S n) T -> r l1 T) -> r (S l2) T)
-- -> (r n T -> r l1 T) -> r l2 T
-- However, when we pass initial continuations and instantiate the type
-- variables, the types of sQ24 and sQ25 are actually the same.
sQ25 = someone1 $$< (saw $$> everyone2)
sQ25r = runC . runCPS2 $ sQ25
-- "forall x. (exists y. (see'(x)(y)))"
-- ------------------------------------------------------------------------
-- The calculus of CPSn
runCPS3 e = e theta theta theta_final
runCPS4 e = e theta theta theta theta_final
-- Raising the quantifiers up one level
up :: ((t2 -> t1) -> t) ->
(t2 -> t3 -> t1) -> t3 -> t
up e = \k1 k2 -> e (\v -> k1 v k2)
-- Level-2 quantifiers, in CPSn
-- The work for all CPSn, n>=2
everyone2n :: (Nat n, DQ r) =>
(r (S n) E -> t3 -> (r (S n) T -> a) -> b)
-> t3 -> (r n T -> a) -> b
everyone2n = up everyone1
someone2n = up someone1
-- ------------------------------------------------------------------------
-- Islands and inverse linking
-- First we extend the language with more constants and the
-- composition rule for noun and relative clauses
class DQE r where
max' :: r Z E
-- common nouns
man', lady', boy', teacher', fcountry'
:: r Z (E -> T)
-- VP (vi)
admitted', disappear', leave'
:: r Z (E -> T)
-- Vt
upset' :: r Z (E -> E -> T)
-- Vs
report' :: r Z (T -> E -> T)
-- other relations on entities (location, etc)
from' :: r Z (E -> E -> T)
-- others
conj :: r Z (T -> T -> T)
neg :: r Z (T -> T)
imply :: r Z (T -> T -> T)
that' :: r Z (T -> E)
-- conjunction of properties: PP attachments, adjective adjunction, etc.
prop_conj :: r Z ((E->T) -> (E->T) -> (E->T))
-- An entity that is the union of two others
e_union :: r Z (E -> E -> E)
instance DQE C where
max' = C "max'"
man' = C (arg1 "man'")
lady' = C (arg1 "lady'")
boy' = C (arg1 "boy'")
teacher' = C (arg1 "teacher'")
fcountry' = C (arg1 "foreign_country'")
admitted' = C (arg1 "admitted'")
disappear' = C (arg1 "disappear'")
leave' = C (arg1 "leave'")
upset' = C (arg2 "upset'")
from' = C (arg2 "from'")
report' = C (\c s -> arg2 "report'" c s)
conj = C (\x y -> x ++ " && " ++ y)
neg = C (\x -> "~" ++ x)
imply = C (\x y -> "(" ++ x ++ ")" ++ " => " ++ y)
that' = C (arg1 "that'")
prop_conj = C (\p1 p2 x -> p1 x ++ " && " ++ p2 x)
e_union = C (arg2 "along_with")
arg1 tag x = tag ++ "(" ++ x ++ ")"
arg2 tag x y = tag ++ "(" ++ x ++ ")(" ++ y ++ ")"
-- Whereas CN (common noun word) has the type r Z (E -> T),
-- (in the paper: (et)), N' has the type r n E -> r n T, or
-- its CPS equivalent (in the paper: e^n -> {n\alpha})
-- The following semantic operation liftN' corresponds to the
-- syntactic production
-- N' -> CN
liftN' :: DQ r => r Z (E -> T) -> (r n E -> (r n T -> t) -> t)
liftN' cn = \x k -> k (cn $> x)
-- More lexical entries
max = lift max'
man = liftN' man'
lady = liftN' lady'
boy = liftN' boy'
teacher = liftN' teacher'
foreign_country = liftN' fcountry'
disappeared = lift disappear'
was_admitted = lift admitted'
left = lift leave'
upset = lift upset'
reported = lift report'
-- Union of two NPs
along_with e1 e2 = lift e_union $$> e1 $$> e2
-- runCPS2 enforcing that the result is of type r Z T:
-- the closed denotation of type t
-- Actually we are using runCPS3 since we CPS all quantifiers one more level
-- so they stay in the tail-recursive form and work on every level
banana2 e = asZT $ runCPS3 e
where asZT :: r Z T -> r Z T; asZT = id
-- Semantic forms corresponding to noun clauses
-- (we will re-define them later, when considering wide-scope indefinites)
-- VP -> Vs that S
the_fact_that vs s = vs $$> (lift (banana2 s))
-- NP -> that S
that s = lift (that' $> banana2 s)
-- Quantifier determiners
-- NP -> Det N'
-- Det -> every | a | some | no
-- In the paper, in Sec 5.1, we let Det take CN as an argument, for
-- simplification. We introduce general Det below in Sec 5.3
every1,a1,some1,no1 :: (Max n n ~ n, Nat n, DQ r, DQE r) =>
(r (S n) E -> (r (S n) T -> (r n T -> a) -> b) -> g)
-> (r (S n) E -> (r (S n) T -> a) -> b)
-> g
every1 n' = \k1 ->
let x = var undefined in
n' x (\rv k2 ->
k1 x (\v ->
k2 (forall (imply $> rv $> v))))
a1 n' = \k1 ->
let x = var undefined in
n' x (\rv k2 ->
k1 x (\v ->
k2 (exists (conj $> rv $> v))))
some1 = a1
no1 n' = \k1 ->
let x = var undefined in
n' x (\rv k2 ->
k1 x (\v ->
k2 (neg $> exists (conj $> rv $> v))))
every2 n' = up (every1 n')
a2 n' = up (a1 n')
no2 n' = up (no1 n')
-- Simple examples
sbl = (every1 boy) $$< left
sblr = runC . runCPS3 $ sbl
-- "forall x. ((boy'(x)) => leave'(x))"
sbl2 = (every2 boy) $$< left
sbl2r = runC . runCPS3 $ sbl2
-- The same
-- A boy upset every teacher
sabet = (a1 boy) $$< (upset $$> (every2 teacher))
sabetr = runC . runCPS3 $ sabet
-- "forall x. ((teacher'(x)) => exists y. (boy'(y) && upset'(x)(y)))"
-- That every boy left upset a teacher.
sblt11 = that ((every1 boy) $$< left) $$<
(upset $$> (a1 teacher))
sblt11r = runC . runCPS3 $ sblt11
-- "exists x. (teacher'(x) && upset'(x)
-- (that'(forall x. ((boy'(x)) => leave'(x)))))"
sblt21 = that ((every2 boy) $$< left) $$<
(upset $$> (a1 teacher))
sblt21r = runC . runCPS3 $ sblt21
-- The same
-- Someone reported that John saw everyone.
srjse11 =
someone1 $$< (reported `the_fact_that` (john $$< (saw $$> everyone1)))
srjse11r = runC . runCPS3 $ srjse11
-- "exists x. (report'(forall x. (see'(x)(john')))(x))"
srjse12 =
someone1 $$< (reported `the_fact_that` (john $$< (saw $$> (up everyone1))))
srjse12r = runC . runCPS3 $ srjse12
-- The same
{-
-- Generalized Coordination
-- We leave this for another time. After all, it can't represent the collective
-- meaning of conjunction like
-- Bill and Jim lifted a table [together]
-- No shirt was red and striped.
BTW, when writing the coordination as
and2 e1 e2 = \k1 k2 k3 ->
e1 k1 k2 (\v1 -> e2 k1 k2 (\v2 -> k3 (conj $> v1 $> v2)))
or
and1 e1 e2 = \k -> e1 (\v1 -> e2 (\v2 -> conj $> k v1 $> k v2))
and1 e1 e2 = \k -> e1 k && e2 k
One should keep in mind that e1 and e2 may be at different levels
(e1 has a quantifier but e2 doesn't). So, we need to insert weakening.
-}
-- ------------------------------------------------------------------------
-- Wide-scope indefinites
-- Lower the CPS level by two: the opposite of up . up
-- Here we come to the limit of Haskell type inference.
-- The operation down2 is supposed to be overloaded based on the CPS
-- level (see the paper). However, the term like \k -> k (john' $< leave')
-- have the schematic type (r Z T -> a) -> a
-- that fits the CPS type of any level (depending on the instantiation
-- of a). One can unambiguously determine that the term belong to
-- CPS 1 because its type matches (r n T -> r n T) -> r Z T.
-- (for example, someone2n $$< left does not match that type; it really
-- has a higher-level CPS type).
-- Alas, such determination is beyond Haskell (unless we use dodgy extensions).
-- Therefore, we introduce two versions of down2:
-- down20 e should be used when e is is at CPS level3 and below
-- down2 e should be used when e is at the CPS level at least 4
-- The type inference will tell which term should be used: if we use
-- down20 when down2n was needed (or vice versa), a type error
-- will be signaled. There are cases when either term could be used, with the
-- same result. Incidentally, this is the reason Haskell type inference
-- fails: it can't cope with a _superficial_ ambiguity, when there are
-- several choices all of which are equivalent.
down20 e = \k -> k (banana2 e)
down2 :: ((t2 -> (t2 -> t1) -> t1) -> (t4 -> (t4 -> t3) -> t3) -> t) -> t
down2 e = e theta theta
-- Just for the sake of comparison:
-- reset2 re-written to work on every level ...
reset23 e = \k1 k2 k3 -> e theta theta (\v -> k1 v k2 k3)
-- A few simple tests
tx :: (DQE r, Nat n, DQ r) =>
(r (S n) T -> (r (S n) T -> a) -> b) -> (r n T -> a) -> b
tx = someone1 $$< left
txr = runC . runCPS3 $ tx
-- Here, eithe down2 or down20 could be used
-- john $$< left, tx0,tx0' :: (DQE r, DQ r) => (r Z T -> t) -> t
tx0 = down2 (john $$< left)
tx0r = runC . runCPS3 $ tx0
tx0' = down20 (john $$< left)
tx0'r = runC . runCPS3 $ tx0'
-- The difference in inferred signatures is important!
-- tx1 has the type that will create superficial ambiguity
-- if tx1 is used with another quantifier.
tx1 :: (DQE r, Nat n, DQ r) => (r n T -> t3) -> t3
tx1 = down2 (someone1 $$< left)
tx1r = runC . runCPS3 $ tx1
tx1' :: (DQE r, DQ r) => (r Z T -> t) -> t
tx1' = down20 (someone1 $$< left)
tx1'r = runC . runCPS3 $ tx1'
-- Superficial ambiguity in n2!
-- td1 :: (DQE r, Nat n2, Nat n, DQ r) =>
-- (r (Max n2 (S n)) T -> (r (S n) T -> a) -> b) -> (r n T -> a) -> b
-- td1 = lift conj $$> down2 (someone1 $$< left) $$> (someone1 $$< disappeared)
-- td1r = runC . runCPS3 $ td1
-- Couldn't match type `Max n20 (S Z)' with `S Z'
-- No ambiguity
td1' :: (DQE r, Nat n, DQ r) =>
(r (S n) T -> (r (S n) T -> a) -> b) -> (r n T -> a) -> b
td1' = lift conj $$> down20 (someone1 $$< left) $$> (someone1 $$< disappeared)
td1'r = runC . runCPS3 $ td1'
--"exists x. (exists x. (leave'(x)) && disappear'(x))"
-- The same situation as with tx1/tx1'
tx2 :: (DQE r, Nat n, DQ r) => (r n T -> b) -> b
tx2 = down2 ((up $ someone1) $$< left)
tx2r = runC . runCPS3 $ tx2
tx2' :: (DQE r, DQ r) => (r Z T -> t) -> t
tx2' = down20 ((up $ someone1) $$< left)
tx2'r = runC . runCPS3 $ tx2'
tx3 :: (DQE r, Nat n, DQ r) =>
(r (S n) T -> (r (S n) T -> a) -> b) -> (r n T -> a) -> b
tx3 = down2 ((up . up $ someone1) $$< left)
tx3r = runC . runCPS3 $ tx3
-- (up . up $ someone1) is at the level 3. Therefore, the down20
-- can no longer be used. The following won't type check
-- tx3' = down20 ((up . up $ someone1) $$< left)
td3:: (DQE r, Nat n, DQ r) =>
(r (S (Max n (S n))) T -> (r (S (S n)) T -> a) -> b)
-> (r n T -> a)
-> b
td3 = lift conj $$> down2 ((up . up $ someone1) $$< left) $$>
(someone1 $$< disappeared)
td3r = runC . runCPS3 $ td3
-- "exists x. (exists y. (leave'(x) && disappear'(y)))"
tx4 :: (DQE r, Nat n, DQ r) =>
(r (S n) T -> t3 -> (r (S n) T -> a) -> b)
-> t3 -> (r n T -> a) -> b
tx4 = down2 ((up . up . up $ someone1) $$< left)
tx4r = runC . runCPS3 $ tx4
td4:: (DQE r, Nat n1, Nat n, DQ r) =>
(r (S (Max n n1)) T -> (r (S n1) T -> a1) -> (r (S n) T -> a) -> b)
-> (r n1 T -> a1)
-> (r n T -> a)
-> b
td4 = lift conj $$> down2 ((up . up . up $ someone1) $$< left) $$>
(someone1 $$< disappeared)
td4r = runC . runCPS3 $ td4
-- "exists x. (exists y. (leave'(x) && disappear'(y)))"
-- Level 3 quantifier, works for CPSn, n>=3
-- We postulate that only indefinites can be at the level n>=3
someone3 = up someone2n
someone4 = up someone3
-- Re-define the_fact_that and that to use down2
-- rather than the absolutist \banana, which collapses the whole
-- hierarchy.
the_fact_that30 vs s = vs $$> (down20 s)
the_fact_that3 vs s = vs $$> (down2 s)
that30 s = (lift that') $$> down20 s
that3 s = (lift that') $$> down2 s
-- The main example
-- Everyone reported that [Max and some lady] disappeared.
sml1 = everyone1 $$<
(reported `the_fact_that30`
((max `along_with` (some1 lady)) $$< disappeared))
sml1r = runC . runCPS3 $ sml1
-- "forall x. (report'
-- (exists x. (lady'(x) && disappear'(along_with(max')(x)))) (x))"
some2 n' = up (some1 n')
some3 n' = up (some2 n')
some4 n' = up (some3 n')
a3 = some3
a4 = some4
-- Incidentally, if we use the_fact_that3 in sml1, we get the type error
-- Occurs check: cannot construct the infinite type: n20 = Max n20 n20
-- It is obvious to us that Max n n _is_ n. But GHC can't see that.
sml2 = everyone1 $$<
(reported `the_fact_that30`
((max `along_with` (some2 lady)) $$< disappeared))
sml2r = runC . runCPS3 $ sml2
-- the same denotation
sml3 = everyone1 $$<
(reported `the_fact_that3`
((max `along_with` (some3 lady)) $$< disappeared))
sml3r = runC . runCPS3 $ sml3
-- "forall x. (exists y. (lady'(y) &&
-- report'(disappear'(along_with(max')(y)))(x)))"
sml4 = everyone1 $$<
(reported `the_fact_that3`
((max `along_with` (some4 lady)) $$< disappeared))
sml4r = runC . runCPS3 $ sml4
-- "exists x. (lady'(x) &&
-- forall y. (report'(disappear'(along_with(max')(x)))(y)))"
-- ------------------------------------------------------------------------
-- Inverse linking
-- [No man from a foreign country] was admitted.
{-
-- First we try a naive way, without an island around PP
-- Prepositional phrases and prepositional attachment
-- PP -> P NP
from0 = lift from'
-- -- PP attachment, or conjunction of properties
-- N' -> N' PP
pp_adj0 n pp = lift prop_conj $$> n $$> pp
-- The inverse-linking reading is fine.
snmfc11 = (no1 $$>> (man `pp_adj0` (from0 $$> (a1 $$>> foreign_country))))
$$< was_admitted
snmfc11r = runC . runCPS3 $ snmfc11
-- "exists x. (foreign_country'(x) &&
-- ~exists y. (man'(y) && from'(x)(y) && admitted'(y)))"
-- But we can't get the direct-scope reading.
-- The following has the scope extrusion! As expected.
-- snmfc21 = (no2 $$>> (man `pp_adj` (from $$> (a1 $$>> foreign_country))))
-- $$< was_admitted
-- Therefore, the following won't type
-- snmfc21r = runC . runCPS3 $ snmfc21
-}
-- We need to make PP a scope island.
-- from will make an island.
-- PP -> P NP
-- Don't ever use down20! z is a variable, so the result can't
-- be closed. BTW, this is the first case of a function
-- that takes an open term as an argument. We didn't have such
-- functions before and did not have to worry about variable
-- confusion.
from :: (DQ r, DQE r) =>
((r n1 E -> (r (Max n1 n2) T -> t1) -> t1)
-> (t4 -> (t4 -> t3) -> t3) -> t)
-> r n2 E -> t
from np = \z -> down2 (lift from' $$> np $$> lift z)
-- -- PP attachment, or conjunction of properties
-- N' -> N' PP
{-
pp_adj :: (DQE r, DQ r) =>
(t3 -> (r n1 T -> t1) -> t)
-> (t3 -> (r n2 T -> t2) -> t1)
-> t3
-> (r (Max n1 n2) T -> t2)
-> t
-}
pp_adj :: (DQE r, DQ r, n ~ Max n n) =>
(e -> (r n T -> t1) -> t)
-> (e -> (r n T -> t2) -> t1)
-> (e -> (r n T -> t2) -> t)
pp_adj n' pp = \z -> lift conj $$> (n' z) $$> (pp z)
-- A few simple tests (all signatures are inferred)
tf0 :: (Max n n ~ n, DQE r, Nat n, DQ r) =>
(r (S n) T -> (r (S n) T -> a) -> b) -> (r n T -> a) -> b
tf0 = no1 (man `pp_adj` from max) $$< left
tf0r = runC . runCPS3 $ tf0
-- "~exists x. (man'(x) && from'(max')(x) && leave'(x))"
tf1 :: (Max n n ~ n, Max (S n) n ~ S n, DQE r, Nat n, DQ r) =>
(r (S n) T -> (r (S n) T -> a) -> b) -> (r n T -> a) -> b
tf1 = no1 (man `pp_adj` from (a1 foreign_country)) $$< left
tf1r = runC . runCPS3 $ tf1
-- "~exists x. (man'(x) &&
-- exists y. (foreign_country'(y) && from'(y)(x)) && leave'(x))"
tf2 = no1 (man `pp_adj` from (a2 foreign_country)) $$< left
tf2r = runC . runCPS3 $ tf2
-- The same
tf3 :: (Max n (S n) ~ S n, Max n n ~ n, DQE r, Nat n, DQ r) =>
(r (S (S n)) T -> (r (S (S n)) T -> t1) -> t) -> (r n T -> t1) -> t
tf3 = no1 (man `pp_adj` from (a3 foreign_country)) $$< left
tf3r = runC . runCPS3 $ tf3
-- "exists x. (foreign_country'(x) &&
-- ~exists y. (man'(y) && from'(x)(y) && leave'(y)))"
tf4 :: (Max n1 n1 ~ n1, Max n n ~ n, Max n1 n ~ n, DQE r, Nat n1,
Nat n, DQ r) =>
(r (S n) T -> (r (S n) T -> t2) -> (r (S n1) T -> t1) -> t)
-> (r n T -> t2) -> (r n1 T -> t1) -> t
tf4 = no1 (man `pp_adj` from (a4 foreign_country)) $$< left
tf4r = runC . runCPS3 $ tf4
-- "exists x. (foreign_country'(x) &&
-- ~exists y. (man'(y) && from'(x)(y) && leave'(y)))"
-- The main example
snmfcf11 = no1 (man `pp_adj` from (a1 foreign_country))
$$< was_admitted
snmfcf11r = runC . runCPS3 $ snmfcf11
-- "~exists x. (man'(x) &&
-- exists y. (foreign_country'(y) && from'(y)(x)) && admitted'(x))"
snmfcf13 = no1 (man `pp_adj` from (a3 foreign_country))
$$< was_admitted
snmfcf13r = runC . runCPS3 $ snmfcf13
-- "exists x. (foreign_country'(x) &&
-- ~exists y. (man'(y) && from'(x)(y) && admitted'(y)))"