Kappa and Zetta calculi, and their dual versions

Kappa.idr

import Data.List.Elem 

data Ty = U | Base | Prod Ty Ty | Sum Ty Ty | Imp Ty Ty | Sub Ty Ty | S Ty 

infixr 5 :*: 
(:*:) : Ty -> Ty -> Ty
(:*:) = Prod 

infixr 5 ~> 
(~>) : Ty -> Ty -> Ty
(~>) = Imp 

infixr 5 :-: 
(:-:) : Ty -> Ty -> Ty
(:-:) = Sub

infixr 5 :+: 
(:+:) : Ty -> Ty -> Ty
(:+:) = Sum 

Ctx : Type 
Ctx = List Ty  

data All : {k:Type} -> (p : k -> Type) -> List k -> Type where 
  ANil : All p []
  (::) : {p : k -> Type} -> p x -> All p xs -> All p (x :: xs)

lookup : All p ctx -> (Elem x ctx -> p x)
lookup (value :: rest) Here  = value 
lookup (value :: rest) (There later) = lookup rest later 

EvTy : Ty -> Type 
EvTy U = Unit
EvTy Base = Nat
EvTy (Imp t1 t2) = (EvTy t1) -> (EvTy t2)
EvTy (Prod t1 t2) = (EvTy t1, EvTy t2)
EvTy (Sum t1 t2) = Either (EvTy t1) (EvTy t2) 
EvTy (Sub t1 t2) = ?ss  
EvTy (S t1) = ?s2 

namespace Kappa 
  data Term : Ctx -> Ty -> Ty -> Type where
    Arr   : Elem x g -> Term g U x
    Id    : Term g x x 
    Bang  : Term g t U
    Comp  : Term g b c -> Term g a b -> Term g a c
    Lift  : Term g U c -> Term g a (c :*: a)
    Kappa : Term (c :: g) a b -> Term g (c :*: a) b

  eval : Term ctx t1 t2 -> All EvTy ctx -> EvTy t1 -> EvTy t2 
  eval (Arr e) env = \() => lookup env e
  eval Id env = id
  eval Bang env = \e => ()
  eval (Comp t1 t2) env = (eval t1 env) . (eval t2 env)   
  eval (Lift t) env = \a => ((eval t env) (), a)
  eval (Kappa t) env = (\(l, r) => eval t (l :: env) r)

namespace Zeta 
  data Term : Ctx -> Ty -> Ty -> Type where
    Arr  : Elem x g -> Term g U x
    Id   : Term g x x 
    Bang : Term g t U
    Comp : Term g b c -> Term g a b -> Term g a c
    Pass : Term g U c -> Term g (c ~> b) b 
    Zeta : Term (c :: g) a b -> Term g a (c ~> b)

  eval : Term ctx t1 t2 -> All EvTy ctx -> EvTy t1 -> EvTy t2 
  eval (Arr e) env = \() => (lookup env e)
  eval Id env = id
  eval Bang env = \e => ()
  eval (Comp t1 t2) env = (eval t1 env) . (eval t2 env)
  eval (Pass t) env = let ev = eval t env in \f => f (ev ()) 
  eval (Zeta t) env = \a, b => (eval t (b :: env)) a 

namespace KappaStar
  data Term : Ctx -> Ty -> Ty -> Type where
    Arr    : Elem x g -> Term g U x
    Id     : Term g x x 
    Bang   : Term g t U
    Comp   : Term g b c -> Term g a b -> Term g a c
    LiftS  : Term g U (S c) -> Term g a (a :-: c)
    KappaS : Term (S c :: g) a b -> Term g (a :-: c) b

  eval : Term ctx t1 t2 -> All EvTy ctx -> EvTy t1 -> EvTy t2 
  eval (Arr e) env = \() => (lookup env e)
  eval Id env = id
  eval Bang env = \e => ()
  eval (Comp t1 t2) env = (eval t1 env) . (eval t2 env)
  eval (LiftS t) env = ?lifts  
  eval (KappaS t) env = ?kappas

namespace ZetaStar
  data Term : Ctx -> Ty -> Ty -> Type where
    Arr   : Elem x g -> Term g U x
    Id    : Term g x x 
    Bang  : Term g t U
    Comp  : Term g b c -> Term g a b -> Term g a c
    PassS : Term g U (S c) -> Term g (c :+: b) b
    ZetaS : Term (S c :: g) a b -> Term g a (c :+: b)

  eval : Term ctx t1 t2 -> All EvTy ctx -> EvTy t1 -> EvTy t2 
  eval (Arr e) env = \() => (lookup env e)
  eval Id env = id
  eval Bang env = \e => ()
  eval (Comp t1 t2) env = (eval t1 env) . (eval t2 env)
  eval (PassS t) env = ?passs 
  eval (ZetaS t) env = ?zetas

namespace LamLamBar 
  data Term : Ctx -> Ty -> Type where 
    Var : Elem a g -> Term g a
    Lam : {a : Ty} -> Term (a::g) b -> Term g (a ~> b)
    App : Term g (a ~> b) -> Term g a -> Term g b
    Fst : Term g (Prod a b) -> Term g a
    Snd : Term g (Prod a b) -> Term g b
    Pair : Term g a -> Term g b -> Term g (Prod a b)
    InL : Term g a -> Term g (Sum a b)
    InR : Term g b -> Term g (Sum a b)
    Case : {a, b : Ty} -> Term g (Sum a b) -> Term (a::g) c -> Term (b::g) c -> Term g c
    Let :  {s : Ty} -> Term g s -> Term (s::g) t -> Term g t
    Colam : Term (S a :: g) b -> Term g (a :+: b)
    Coapp : Term g (a :+: b) -> Term g (S a) -> Term g b

  eval : {g : List Ty} -> Term g t -> All EvTy g -> EvTy t
  eval (Var v) env = lookup env v
  eval (Lam t) env = \x => eval t (x :: env)
  eval (App t1 t2) env = (eval t1 env) (eval t2 env)
  eval (Pair t1 t2) env = (eval t1 env, eval t2 env)
  eval (Fst t) env = fst (eval t env)
  eval (Snd t) env = snd (eval t env)
  eval (Let t c) env = eval c ((eval t env) :: env)
  eval (InL t) env = Left (eval t env) 
  eval (InR t) env = Right (eval t env) 
  eval (Case t1 t2 t3) env = case eval t1 env of 
    Left l => eval t2 (l :: env)
    Right r => eval t3 (r :: env)
  eval (Colam t) env = ?colams 
  eval (Coapp t1 t2) env = ?coapps