Main.hs

{-# Language GADTs #-}
module Main where
import Control.Monad.Cont

data Proper = John | Mary -- Proper -> john | mary
data Det = A | The -- DET -> a | the
data N = Man | Woman -- N -> man | woman
data NP = NP0 Det N | NP1 Proper -- NP -> Det N | Proper
data VI = Sleeps | Walks -- VI -> sleeps | walks
data VT = Loves -- VT -> loves
data VP = VP0 VI | VP1 VT NP  -- VP -> VI | VT NP
data S = S0 NP VP -- S -> NP P

sent0 :: S -- a man walks
sent0 = (A `NP0` Man) `S0` (VP0 Walks)

sent1 :: S -- a man loves a woman
sent1 = (A `NP0` Man) `S0` (Loves `VP1` (A `NP0` Woman))

data Proper' where
  John' :: Proper' -- N
  Mary' :: Proper' -- N
  Crazy' :: Proper' -> Proper' -- N/N
    -- (形容詞の限定用法と叙述用法  意味論的には?)

data Sentence_GADT where
  Walks' :: Proper' -> Sentence_GADT -- S/N

  Kicks' :: Proper' -> Proper' -> Sentence_GADT -- (S/N)/N
  Thinks' :: Proper' -> Sentence_GADT -> Sentence_GADT -- (S/N)/N

  Anyone' :: (Proper' -> Sentence_GADT) -> Sentence_GADT -- S/(S/N)      ∀x. P(x)
    -- λP.  ∀x. P(x)

  Someone' :: (Proper' -> Sentence_GADT) -> Sentence_GADT -- S/(S/N)      ∃x. P(x)
    -- λP.  ∃x. P(x)

  Teacher :: Proper' -> Sentence_GADT -- S/N
    -- λx. Teacher(x)

  The' :: (Proper' -> Sentence_GADT) -> (Proper' -> Sentence_GADT) -> Sentence_GADT -- (S/(S/N))/(S/N)
    -- λP, Q.   (∃!x. P(x)) & (∀x. P(x) -> Q(x))
    -- "The _ being is _." -> "The minimum prime being is preceding 3."
  And' :: Sentence_GADT -> Sentence_GADT -> Sentence_GADT -- (S/S)/S
  But' :: Sentence_GADT -> Sentence_GADT -> Sentence_GADT -- (S/S)/S
  Or' :: Sentence_GADT -> Sentence_GADT -> Sentence_GADT -- (S/S)/S
  Unfortunately' :: Sentence_GADT -> Sentence_GADT -- S/S
  For' :: Proper' -> Sentence_GADT -> Sentence_GADT -- (S/S)/N

type Predicate = Proper' -> Sentence_GADT  -- S/N
type Qualifier = Predicate -> Sentence_GADT -- S/(S/N)
type Conjunctive = Sentence_GADT -> Sentence_GADT -> Sentence_GADT -- (S/S)/S
type Adverb = Sentence_GADT -> Sentence_GADT -- (S/S)
type Preposition = Proper' -> Sentence_GADT -- (S/S)

crazy_john_kicks_mary :: Sentence_GADT
crazy_john_kicks_mary = (Crazy' John') `Kicks'` Mary'

someone_kicks_john :: Sentence_GADT
someone_kicks_john = Someone' (`Kicks'` John')

kicks_himself :: Proper' -> Sentence_GADT -- S/N   ("kick himself")
kicks_himself = (\x -> x `Kicks'` x)

someone_kicks_himself :: Sentence_GADT
someone_kicks_himself = Someone' kicks_himself -- ∃x. Kicks(x, x)

x & f = f x

the_teacher_kicks_himself :: Sentence_GADT
the_teacher_kicks_himself = (`runCont` id) $ do
  the_teacher <- (cont (The' Teacher))
  return (the_teacher & kicks_himself)
  -- (∃!x. Teacher(x)) & (∀x. Teacher(x) -> Kicks(x, x)) になっている?

john_kicks_someone :: Sentence_GADT
john_kicks_someone = (`runCont` id) $ (return . (John' `Kicks'`)) =<< (cont Someone')


ka :: Proper' -> Proper' -> (Cont Sentence_GADT) Proper' -- 固有名詞同士の「か」(or)
ka x y = cont (\p -> p x `Or'` p y)

john_believes_john_or_mary_walks :: Sentence_GADT -- ジョンは[ジョンかメアリーが歩いた]と思っている (どちらかなのかの確証があるとは限らない)
john_believes_john_or_mary_walks = John' `Thinks'` john_or_mary_walks
 where
   john_or_mary_walks :: Sentence_GADT
   john_or_mary_walks = (`runCont` id) $ do
    john_or_mary <- John' `ka` Mary'
    return (john_or_mary & Walks')

john_believes_john_or_mary_walks2 :: Sentence_GADT -- [ジョンはジョンかメアリーが歩いたと思っている] (ジョンはどちらか１つを信じている)
john_believes_john_or_mary_walks2 = (`runCont` id) $ do
  john_or_mary <- John' `ka` Mary'
  return (John' `Thinks'` (john_or_mary & Walks'))

main :: IO ()
main = do
  putStrLn "hello world" -- 入出力はなし