Skip to content

Instantly share code, notes, and snippets.

@zanzix
Created September 16, 2023 18:14
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
Star You must be signed in to star a gist
Save zanzix/0e113d5aef1c7e0a985328fac35fa032 to your computer and use it in GitHub Desktop.
Kappa and Zetta calculi, and their dual versions
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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment