Symmetric Lambda Calculus

SLC.hs

{-# LANGUAGE GADTs, KindSignatures #-}

data Val = B Int | Unit | Pair Val Val | In1 Val | In2 Val | Closr (Val -> Cnt -> Ans) | Contx Val Cnt
type Cnt = Val -> Ans
type Env = Ide -> Either Val Cnt

type Ans = IO ()
type Ide = String

data E :: * -> * where
  CstE   :: Val -> E t
  VarE   :: Ide -> E t
  AppE   :: E s -> F s t -> E t
  UnitE  :: E ()
  ProdE  :: E a -> E b -> E (a, b)
  ClosrE :: F s t -> E (s -> t)

data C :: * -> * where
  CstC   :: Cnt -> C t
  VarC   :: Ide -> C t
  AppC   :: C t -> F s t -> C s
  NullC  :: C ()
  SumC   :: C a -> C b -> C (a, b)
  ContxC :: F s t -> C (s -> t)
  
data F :: * -> * -> * where
  CstF   :: (Val -> Val) -> F s t
  FunX   :: X s -> E t -> F s t
  ClosrF :: E (s -> t) -> F s t
  FunY   :: Y t -> C s -> F s t
  ContxF :: C (s -> t) -> F s t

data X :: * -> * where
  VarX  :: Ide -> X t
  UnitX :: X ()
  ProdX :: X a -> X b -> X (a, b)

data Y :: * -> * where
  VarY  :: Ide -> Y s
  NullY :: Y ()
  SumY  :: Y a -> Y b -> Y (a, b)

semE :: E t -> Env -> Cnt -> Ans
semE (CstE v)      r k = k v
semE (VarE i)      r k = let Left v = r i in k v 
semE (ProdE e1 e2) r k = semE e1 r $ \v1 -> semE e2 r $ \v2 -> k (Pair v1 v2)
semE UnitE         r k = k Unit
semE (AppE e f)    r k = semE e r (\v -> semF f r v k)
semE (ClosrE f)    r k = k (Closr $ \v c -> semF f r v c)

semC :: C t -> Env -> Val -> Ans
semC (CstC k)     r v = k v
semC (VarC i)     r v = let Right k = r i in k v
semC (SumC c1 c2) r v = case v of { In1 v -> semC c1 r v; In2 v -> semC c2 r v }
semC NullC        r v = error "Empty choice"
semC (AppC c f)   r v = semF f r v (\t -> semC c r t)
semC (ContxC f)   r v = let Contx a c = v in semF f r a c

semF :: F s t -> Env -> Val -> Cnt -> Ans
semF (CstF f)   r v k = k (f v) 
semF (FunX x e) r v k = semE e (semX x v r) k
semF (FunY y c) r v k = semC c (semY y k r) v
semF (ClosrF e) r v k = semE e r (\t -> let Closr f = t in f v k)
semF (ContxF c) r v k = semC c r (Contx v k)

semX :: X t -> Val -> Env -> Env
semX (VarX i)      v r = \x -> if x == i then Left v else r x
semX UnitX         v r = let Unit = v in r
semX (ProdX x1 x2) v r = let Pair v1 v2 = v in semX x1 v1 $ semX x2 v2 r

semY :: Y t -> Cnt -> Env -> Env
semY (VarY i)     k r = \y -> if y == i then Right k else r y
semY NullY        k r = r
semY (SumY y1 y2) k r = semY y1 (\v -> k (In1 v)) $ semY y2 (\v -> k (In2 v)) r

emptyEnv :: Env
emptyEnv i = error ("Unknown variable: " ++ i)

instance Show Val where
  show (B x)      = show x
  show Unit       = show ()
  show (Pair x y) = show (x, y)
  show (In1 v) = "In1 " ++ show v
  show (In2 v) = "In2 " ++ show v

-- d :: A x (B + C) -> A x B + A x C
d = 
  FunX (ProdX (VarX "a") (VarX "bc")) $
  AppE (VarE "bc") $
  FunY (SumY (VarY "ab") (VarY "ac")) $
  SumC
    (AppC (VarC "ab") (FunX (VarX "b") (ProdE (VarE "a") (VarE "b"))))
    (AppC (VarC "ac") (FunX (VarX "c") (ProdE (VarE "a") (VarE "c"))))

main = semF d emptyEnv (Pair (B 10) (In2 (B 20))) (print . show)