An attempt to encode Hybrid Type-Logical Categorial Grammar in Haskell... which fails horribly, as I can't use closed type families in the current release of GHC. I'll have another go at it in November.

README.md

An attempt to encode Hybrid Type-Logical Categorial Grammar in Haskell...

Based on "Lambda: The Ultimate Syntax-Semantics Interface" as taught by Oleg Kiselyov and Chung-chieh Shan and "Hybrid Type-Logical Categorial Grammar" as taught by Yusuke Kubota and Robert Levine, at ESSLLI 2013.

HTCG.hs

{-# LANGUAGE TypeFamilies, TypeOperators #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances, FlexibleContexts #-}
{-# LANGUAGE RankNTypes, ExistentialQuantification #-}
{-# LANGUAGE UndecidableInstances, NoMonomorphismRestriction #-}
{-# LANGUAGE FunctionalDependencies #-}

import Prelude hiding (and)



-- * Tectogrammatical Types

data S
data N
data NP
type IV = NP :\ S
type TV = IV :/ NP
data a :\ b
data a :/ b

-- |The domain of tectogrammatical types is constructed as one of the
--  basic tectogrammatical types S, N or NP, together with all possible
--  compositions over these types, using the composition functions
--  @(/)@ and @(\)@ from Lambek grammars and @(|)@ from linear grammars.
class IsTecto a
instance IsTecto S
instance IsTecto N
instance IsTecto NP
instance (IsTecto a, IsTecto b) => IsTecto (a :/ b)
instance (IsTecto a, IsTecto b) => IsTecto (a :\ b)



-- * Phenogrammatical Types

-- |The domain of pheno grammatical types is constructod as either a
--  string, or a function over phenogrammatical types.
class IsPheno a
instance IsPheno String
instance (IsPheno a, IsPheno b) => IsPheno (a -> b)

-- |We can compute the phenogrammatical types from the tectogrammatical
--  types by applying the @Pheno@ type family.
type family Pheno (a :: *)
type instance Pheno (S)      = String
type instance Pheno (N)      = String
type instance Pheno (NP)     = String
type instance Pheno (b :/ a) = Pheno a -> Pheno b
type instance Pheno (a :\ b) = Pheno a -> Pheno b



-- * Semantic Types

data E = John | Mary | Bill deriving (Eq,Show,Enum,Bounded)
type T = Bool

-- |The domain of semantic types is constructed as either of the type
--  constants E or T, and any function over semantic types types.
class IsSem a
instance IsSem E
instance IsSem T
instance (IsSem a, IsSem b) => IsSem (a -> b)

-- |We can compute the lambda denotation types from the tectogrammatical
--  types by applying the @Sem@ type family.
type family Sem (a :: *)
type instance Sem (S)      = T
type instance Sem (N)      = E -> T
type instance Sem (NP)     = E
type instance Sem (b :/ a) = Sem a -> Sem b
type instance Sem (a :\ b) = Sem a -> Sem b



-- * Representations

-- |Representation of a word as a tectogrammatical type, combined with
--  a phenogrammatical realisation and a lambda denotation.
data Repr a = (IsTecto a) => Repr { pheno :: Pheno a , sem   :: Sem a }

-- |We can print representations as long as their phenogrammatical form
--  is not a higher-order expression.
instance (Pheno a ~ String) => Show (Repr a)
  where show (Repr σ _) = σ
  
  

-- * Compositions

infixr 6 ○

class Compose a b c | a b -> c where
  (○) :: a -> b -> c

instance (IsTecto a, IsTecto b) =>
  Compose (Repr a) (Repr (a :\ b)) (Repr b) where
  (○) (Repr σ1 φ1) (Repr σ2 φ2) = Repr (σ2 σ1) (φ2 φ1)
  
instance (IsTecto a, IsTecto b) =>
  Compose (Repr (b :/ a)) (Repr a) (Repr b) where
  (○) (Repr σ1 φ1) (Repr σ2 φ2) = Repr (σ1 σ2) (φ1 φ2)

instance (IsTecto a, IsTecto b, IsTecto c) =>
  Compose (Repr (a :\ b)) (Repr (b :\ c)) (Repr (a :\ c)) where
  (○) (Repr σ1 φ1) (Repr σ2 φ2) = Repr (σ2 . σ1) (φ2 . φ1)

instance (IsTecto a, IsTecto b, IsTecto c) =>
  Compose (Repr (c :/ b)) (Repr (b :/ a)) (Repr (c :/ a)) where
  (○) (Repr σ1 φ1) (Repr σ2 φ2) = Repr (σ1 . σ2) (φ1 . φ2)
  
-- instance (IsTecto a, IsTecto b, IsTecto c) =>
--   Compose (Repr a) (Repr (b :/ c)) (Repr ((b :/ a) :\ c)) where
--   (○) (Repr σ1 φ1) (Repr σ2 φ2) = Repr (\f -> σ2 (f σ1)) (\f -> φ2 (f φ1))

-- instance (IsTecto a, IsTecto b, IsTecto c) =>
--   Compose (Repr (b :/ c)) (Repr a) (Repr (c :/ (a :\ b))) where
--   (○) (Repr σ1 φ1) (Repr σ2 φ2) = Repr (\f -> σ1 (f σ2)) (\f -> φ1 (f φ2))
  
  
-- * Generalized Conjunction

-- |There is a subdomain of the semantic types which corresponds to the
--  truth functions; that is, any function that when given all its arguments
--  will return a boolean value.
--  Over this domain we can define generalized conjunction by induction.
class IsTruth a where
  (/\) :: a -> a -> a

instance IsTruth T where
  x /\ y = x && y

instance (IsSem a) => IsTruth (a -> T) where
  f /\ g = \x -> f x /\ g x

-- |Furthermore, we can make all first-order phenogrammatical types composable
--  by inserting the empty string whenever we encounter a function.
instance Compose String String String where
  a ○ b = a ++ " " ++ b
  
instance (IsPheno a, IsPheno b, IsPheno c, Compose a b c) =>
  Compose (String -> a) (String -> b) c where
  f ○ g = f "" ○ g ""
  
-- |And use this generalized conjunction to define an entry
--  for the general usage of the word "and".
class And a where
  and :: Repr ((a :\ a) :/ a)

instance (IsTecto a, Compose (Pheno a) (Pheno a) (Pheno a), IsTruth (Sem a)) => And a where
  and = Repr (○) (/\)
  
  
  
-- * Lexical Definitions

john, mary, bill :: Repr NP
john = Repr "john" John
mary = Repr "mary" Mary
bill = Repr "bill" Bill

walks :: Repr (NP :\ S)
walks = Repr (\z -> z ○ "walks") walks' where
  walks' John = True
  walks' _    = False
  
sleeps :: Repr (NP :\ S)
sleeps = Repr (\z -> z ○ "sleeps") sleeps' where
  sleeps' Bill = True
  sleeps' _    = False

likes :: Repr ((NP :\ S) :/ NP)
likes = Repr (\x z -> z ○ "likes" ○ x) (flip likes') where
  likes' John Mary = True
  likes' Bill Mary = True
  likes' Mary John = True
  likes' John John = True
  likes' Mary Mary = True
  likes' _    _    = False

entities :: [E]
entities = [minBound .. maxBound]
  
everybody :: Repr (S :/ (NP :\ S))
everybody = Repr (\σ -> σ "everybody") (\p -> all p entities)
  
somebody :: Repr (S :/ (NP :\ S))
somebody = Repr (\σ -> σ "somebody") (\p -> any p entities)
  
nobody :: Repr (S :/ (NP :\ S))
nobody = Repr (\σ -> σ "nobody") (\p -> not (any p entities))



-- * Example Sentences

sentence1 :: Repr S
sentence1 = john ○ walks

sentence2 :: Repr S
sentence2 = mary ○ sleeps
  
sentence3a :: Repr S
sentence3a = john ○ likes ○ mary

sentence3b :: Repr S
sentence3b = mary ○ likes ○ mary

sentence3c :: Repr S
sentence3c = bill ○ likes ○ mary

sentence4 :: Repr S
sentence4 = everybody ○ likes ○ mary

sentence5 :: Repr S
sentence5 = somebody ○ likes ○ john

sentence6a :: Repr S
sentence6a = nobody ○ likes ○ bill

sentence6b :: Repr S
sentence6b = nobody ○ likes ○ mary