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

-- Applicative Symantics

-- The abstract language and the mapping to the surface `syntax'

module Abstract where

import Prelude hiding (and)

{-
This file defines the abstract language fragment to analyze the set
of following examples

Mary left.
John ignored Mary and Mary left.
John ignored Mary and she left.
* She left.

John ignored a woman.
John ignored a woman and she left.
* John ignored every woman and she left.

* It-is-not-the-case-that John ignored a woman and she left.
John ignored a woman and it-is-not-the-case-that she left.

(similar to the sentences by Carl Pollard, analyzes in the CAG-talk)

Further examples to analyze:
 quantifier ambiguity

Other sentences (scoping islands)
 A speaker of every EU language arrived. (ambiguity)
 A person who speaks every EU language arrived. (every is trapped,
 no ambiguity)
-}


-- Types
data NP
data CN					-- common noun
data S
data M					-- matrix

data a :-> b				-- Abstract function space
infixr 1 :->

 
class Abstract r where
  john    :: r NP
  mary    :: r NP
  left    :: r (NP :-> S)
  ignored :: r (NP :-> NP :-> S)
  woman   :: r CN
  man     :: r CN
  dot     :: r (S :-> M)		-- the end of the sentence

  (<#>)   :: r (a:->b) -> r a -> r b	-- combining rule
infixl 4 <#>

-- The inferred type: (check!)
-- NB: type inference, defining and using phrases (parts of sentence),
-- the inferred type of a complete sentence

-- t01 :: Abstract r => r M
t01 = dot <#> (left <#> mary)

-- predicate
-- ignmary :: Abstract r => r (NP :-> S)
ignmary = ignored <#> mary

-- clause
-- imj :: Abstract r => r S
imj = ignmary <#> john

-- complete sentence
-- t02 :: Abstract r => r M
t02 = dot <#> imj  -- john ignored mary

-- Extension: conjunction

class Abstract r => ACnj r where
  and     :: r (S :-> S :-> S)

-- t03 :: ACnj r => r M
t03 = dot <#> 
        (and <#> imj <#> (left <#> mary))

-- Extension: pronouns (Anaphora)

class Abstract r => APro r where
  she     :: r NP


-- sheleft :: APro r => r S
sheleft = (left <#> she)

-- tp1 :: APro r => r M
tp1 = dot <#> sheleft
tp2 = dot <#> (and <#> imj <#> sheleft)

-- Extensions: indefinite and universals

class Abstract r => AInd r where
  a     :: r (CN :-> NP)

class Abstract r => AEvr r where
  every :: r (CN :-> NP)

-- tq1 :: AInd r => r M
tq1 = dot <#> (left <#> (a <#> woman))
tq2 = dot <#> (left <#> (every <#> woman))

tq3 = dot <#> 
      (and <#> (left <#> john) <#> (left <#> (every <#> woman)))

tqp1 = dot <#> 
        (and <#> (ignored <#> (a <#> woman) <#> john) <#> sheleft)

-- NB: the type shows the extensions in use
-- tqp2 :: (ACnj r, APro r, AEvr r) => r M
tqp2 = dot <#> 
        (and <#> (ignored <#> (every <#> woman) <#> john) <#> sheleft)

-- Quantifier ambiguity
tEmanAwoman = dot <#>
  (ignored <#> (a <#> man) <#> (every <#> woman))

tAmanEwoman = dot <#>
  (ignored <#> (every <#> man) <#> (a <#> woman))


-- ------------------------------------------------------------------------
-- String interpreter
-- This is the first interpreter of Abstract, to let us see its terms

-- Interpret every type as a string
newtype Sh a = Sh String

instance Abstract Sh where
    john = Sh "john"
    mary = Sh "mary"
    left = Sh "left"
    ignored = Sh "ignored"
    woman   = Sh "woman"
    man     = Sh "man"
    dot     = Sh "dot"
    Sh x <#> Sh y = Sh ("(" ++ x ++ " <#> " ++ y ++ ")")

instance ACnj Sh where
    and     = Sh "and"

instance APro Sh where
    she  = Sh "she"

instance AInd Sh where
    a    = Sh "a"

instance AEvr Sh where
    every = Sh "every"

instance Show (Sh a) where
    show (Sh x) = x

-- The tests show that an Abstract formula looks as it seems in the code
sheleftSh = sheleft :: Sh S
-- (left <#> she)

t01Sh  = t01 :: Sh M
tqp2Sh = tqp2 :: Sh M
-- (dot <#> ((and <#> ((ignored <#> (every <#> woman)) <#> john)) <#> (left <#> she)))


-- ------------------------------------------------------------------------
-- 'Syntactic' implementations of Abstract language:
-- mapping Abstract to Syntax

-- Since the language of Syntax is so simple (with string
-- constants and the binary concatenation operation), we don't
-- bother to define a type class for it.

newtype Syn a = Syn (SynT a)

-- Interpretation of types: all base types are interpreted
-- as strings; (:->) is interpreted as arrow
type family SynT a :: *
type instance SynT NP = String
type instance SynT CN = String
type instance SynT S  = String
type instance SynT M  = String
type instance SynT (a :-> b)  = SynT a -> SynT b

instance Abstract Syn where
    john = Syn "John"
    mary = Syn "Mary"
    left = Syn (\subj -> subj ++ " left")
    ignored = Syn (\obj subj -> subj ++ " ignored " ++ obj)
    woman  = Syn "woman"
    man  = Syn "man"
    dot  = Syn (\s -> s ++ ".")

    Syn x <#> Syn y = Syn (x y)

instance ACnj Syn where
    and  = Syn (\s1 s2 -> s1 ++ " and " ++ s2)

instance APro Syn where
    she  = Syn "she"

instance AInd Syn where
    a    = Syn (\cn -> "a " ++ cn)

instance AEvr Syn where
    every = Syn (\cn -> "every " ++ cn)


-- M is the starting symbol of the grammar
runSyn :: Syn M -> String
runSyn (Syn x) = x

-- Error messages are quite good
-- Only complete sentences have `syntax'
{-
*Abstract> runSyn sheleft

<interactive>:1:8:
    Couldn't match expected type `M' with actual type `S'
    Expected type: Syn M
      Actual type: Syn S
    In the first argument of `runSyn', namely `sheleft'
    In the expression: runSyn sheleft
-}

t01Syn = runSyn t01
-- "Mary left."

t02Syn = runSyn t02
-- "John ignored Mary."

t03Syn = runSyn t03
-- "John ignored Mary and Mary left."

tp1Syn = runSyn tp1
-- "she left."

tp2Syn = runSyn tp2
-- "John ignored Mary and she left."

tq1Syn = runSyn tq1
-- "a woman left."

tq2Syn = runSyn tq2
-- "every woman left."

tq3Syn = runSyn tq3
-- "John left and every woman left."

tqp1Syn = runSyn tqp1
-- "John ignored a woman and she left."

tqp2Syn = runSyn tqp2
-- "John ignored every woman and she left."

tEmanAwomanSyn = runSyn tEmanAwoman
-- "every woman ignored a man."

tAmanEwomanSyn = runSyn tAmanEwoman
-- "a woman ignored every man."