lam.agda

module lam where

open import Data.List
open import Data.Unit
open import Data.Empty
open import Data.Product
open import Data.Sum

data Ty : Set where
  _⊗_ : Ty → Ty → Ty
  _⊕_ : Ty → Ty → Ty
--  _&_ : Ty → Ty → Ty
  _⊸_ : Ty → Ty → Ty
  !_ : Ty → Ty
  Unit : Ty
  Nil  : Ty
  AUnit : Ty
  ANil  : Ty

¬ : Ty → Ty
¬ x = (x ⊸ Nil)

data Comp (F : Ty → Ty → Set) : Ty → Ty → Set where
  id : ∀{a} → Comp F a a
  _∘_ : ∀{a b c} → F b c → Comp F a b → Comp F a c

data Op : Ty → Ty → Set where
  split : ∀{a b c d} → Comp Op a c → Comp Op b d → Op (a ⊗ b) (c ⊗ d)
  assl  : ∀{a b c} → Op (a ⊗ (b ⊗ c)) ((a ⊗ b) ⊗ c) 
  assr  : ∀{a b c} → Op ((a ⊗ b) ⊗ c) (a ⊗ (b ⊗ c))
  insl  : ∀{a} → Op a (Unit ⊗ a)
  dell  : ∀{a} → Op (Unit ⊗ a) a
  exch  : ∀{a b} → Op (a ⊗ b) (b ⊗ a)
  app   : ∀{a b} → Op ((a ⊸ b) ⊗ a) b
  cur   : ∀{a b c} → Comp Op (a ⊗ b) c → Op a (b ⊸ c)
  --fst   : ∀{a b} → Op (a & b) a
  --snd   : ∀{a b} → Op (a & b) b
  --pair  : ∀{a b c} → Comp Op a b → Comp Op a c → Op a (b & c)
  inl   : ∀{a b} → Op a (a ⊕ b)
  inr   : ∀{a b} → Op b (a ⊕ b)
  alt   : ∀{a b c} → Comp Op a c → Comp Op b c → Op (a ⊕ b) c
  read  : ∀{a} → Op (! a) a
  kill  : ∀{a} → Op (! a) Unit
  copy   : ∀{a} → Op (! a) ((! a) ⊗ (! a))
  make  : ∀{a b} → Comp Op a b → Comp Op a Unit → Comp Op a (a ⊗ a) → Op a (! b)
  --absurd : ∀{a} → Op Nil a
  --halt : ∀{a} → Op a AUnit
  callcc : ∀{a} → Op (¬ (¬ a)) a