A (pseudocode) scheme for parsing a CCG

gistfile1.hs

{- 
  Given a universe Type with base types in <_> and functions in _~>_, and a language Tm over Type, 
  and decidable equality for types and for terms, we can parse strings of tokens in Tm into trees in Tm.
  We should end up with all possible syntactic interpretations of a given string, but I've not proved this.
  
  Given the following lexicon:
  
    πέδας :: Tm <N>
    ἔβαλε :: Tm (<D> ~> <V>)
    det :: Tm (<N> ~> <D>)
    χρυσείας :: Tm (<N> ~> <N>)

  we can parse a sentence as follows:
  
    parse [πέδας, ἔβαλε, det, χρυσείας] => [ πέδας < (ἔβαλε >B (det >B χρυσείας)) ]

  From here, it is trivial to reduce the sentence to all possible semantic interpretations.

  This is probably a terribly inefficient algorithm, but it would seem to work on paper at least. Still
  need to actually implement it in a real language (Agda perhaps).
-}

tryRightApp :: (s t :: Type) (x :: Tm s) (y :: Tm t) -> Maybe (Sigma Type Tm)
tryRightApp s t x y <= elim s
  | a ~> b <= elim (t ==? a)
    | yes refl => Just (b, (x > y))
    | _        => Nothing
  | _ => Nothing

tryLeftApp :: (s t :: Type) (x :: Tm s) (y :: Tm t) -> Maybe (Sigma Type Tm)
tryLeftApp s t x y <= elim t
  | a ~> b <= elim (s ==? a)
    | yes refl => Just (x > y)
    | _        => Nothing
  | _ => Nothing

tryRightComp :: (s t :: Type) (x :: Tm s) (y :: Tm t) -> Maybe (Sigma Type Tm)
tryRightComp s t x y <= (elim s, elim t)
  | (b ~> g, a ~> z) <= elim (z ==? b)
    | yes refl => Just (a ~> g, x >B y)
    | _        => Nothing
  | _ => Nothing

tryLeftComp :: (s t :: Type) (x :: Tm s) (y :: Tm t) -> Maybe (Sigma Type Tm)
tryLeftComp s t x y <= (elim s, elim t)
  | (a ~> b, z ~> g) <= elim (z ==? b)
    | yes refl => Just (a ~> g, x <B y)
    | _        => Nothing
  | _ => Nothing

data Options a = [] | a : (Options a)
justs :: Options (Maybe a) -> Options a

merge :: (x y :: Sigma Type Tm) -> Options (Sigma Type Tm)
merge (_,x) (_,y) = justs [ tryRightApp _ _ x y
                          , tryLeftApp _ _ x y
                          , tryRightComp _ _ x y
                          , tryLeftComp _ _ x y
                          ]

data Tokens a = [] | a : (Tokens a)

normalize :: (s :: Type) (x :: Tm s) -> Tm s
trim :: Eq a => Options a -> Options a

trimNf :: Options (Sigma Type Tm) -> Options (Sigma Type Tm)
trimNf xs = trim (normalize <$> xs)

parse :: Tokens (Sigma Type Tm) -> Options (Sigma Type Tm)
parse xs <= elim xs
  | [] => []
  | (x:zs) <= elim zs
    | [] => [x]
    | y:ys => let xys = merge x y in 
              trimNf $ (merge x =<< parse (y:ys)) ++ (join (merge <$> xys <*> parse ys))