{-# LANGUAGE EmptyDataDecls, NoMonomorphismRestriction #-}
{-# LANGUAGE TypeFamilies #-}

-- | Context-free grammar with quantifiers
-- A different ways to add quantification, via 
-- Higher-Order abstract syntax (HOAS).
-- This is a "rational reconstruction" of Montague's
-- general approach of `administrative pronouns', which
-- later gave rise to the Quantifier Raising (QR)
--
module Lambda.QHCFG where

import Lambda.Semantics
import Lambda.CFG                               -- we shall re-use our earlier work

-- | No longer any need in a new syntactic category QNP
-- We leave out CN as an exercise
--
-- > data CN                                      -- Common noun
--
-- We extend our earlier fragment with quantifiers everyone, someone.
-- In contrast to QCFG.hs, we do not add any new syntactic category,
-- so we don't need to add any rules to our CFG.
--
class (Symantics repr) => Quantifier repr where
  everyone :: (repr NP -> repr S) -> repr S
  someone  :: (repr NP -> repr S) -> repr S

-- | Sample sentences (or, CFG derivations):
-- compare with those in QCFG.hs
-- We stress that the inferred type of sen2-sen4
-- is S. So, these are the derivations of
-- complete sentences.
--
sen2 = everyone (\he -> r1 he (r2 like mary))

sen3 = someone (\she -> r1 john (r2 like she))

sen4 = everyone (\he -> someone (\she -> r1 he (r2 like she)))

-- | We extend our EN interpreter (interpreter of
-- derivations as English phrases) to deal
-- with quantifiers.
--
instance Quantifier EN where
  everyone     f = f (EN "everyone")
  someone      f = f (EN "someone")

-- | We can now see the English sentences that
-- correspond to the derivations sen2-sen4.
sen2_en = sen2 :: EN S
sen3_en = sen3 :: EN S
sen4_en = sen4 :: EN S

-- | We also extend the semantics interpreter:
-- the interpreter of a derivation into a
-- formula of STT, or Lambda-calculus.
-- We reconstruct Montague's ``pronoun trick''
instance (Lambda lrepr) => Quantifier (Sem lrepr) where
  everyone       f = Sem (app forall       (lam (\he  -> unSem (f (Sem he)))))
  someone        f = Sem (app exists       (lam (\she -> unSem (f (Sem she)))))

-- | We can see the semantic yield of our derivations
sen2_sem = sen2 :: Sem (P C) S  -- We encode universal via existential
sen3_sem = sen3 :: Sem C S -- now reduced!
sen4_sem = sen4 :: Sem (P C) S

-- | As in QCFG.hs, sen4_sem demonstrates the linear reading.
-- Now however we can get the inverse reading of the phrase.
--
-- We build the following derivation
sen4' = someone (\she -> everyone (\he -> r1 he (r2 like she)))

-- | which corresponds to the same English phrase
sen4'_en = sen4' :: EN S
-- everyone likes someone

-- | The semantics shows the inverse reading
sen4'_sem = sen4' :: Sem (P C) S