Concategories

Concategory.idr

%hide Neg 

-- Base types. Unit, Bool, Monoid
data Ty = Unit | B | M | Ten Ty Ty | Sum Ty Ty | Neg Ty 

Val : Ty -> Type 
Val Unit = Unit 
Val (Sum a b) = Either (Val a) (Val b) 
Val (Ten a b) = (Val a, Val b) 
Val B = Bool 
Val M = Nat 
Val (Neg t) = Val t -- negation is trivial (for now)

-- Environment for n-ary products
data All : (p : k -> Type) -> List k -> Type where 
  ANil : All p []
  ACons : {p : k -> Type} -> p x -> All p xs -> All p (x :: xs)

-- Environments for n-ary sums
data Choice : (p : k -> Type) -> List k -> Type where 
  Here : {p : k -> Type} -> p x -> Choice p (x :: xs)
  There : Choice p xs -> Choice p (x :: xs)

-- | Cartesian Multicategory over a signature, the context is shared. 
data Multicat : (List o -> o -> Type) -> List o -> o -> Type where
  -- Embedding of a generator into a multicategory
  InM : {sig : List o -> o -> Type} -> sig as b -> Multicat sig as b
  -- Identity
  IdM : Multicat sig [a] a
  -- Sequential composition along one wire
  Let : Multicat sig as s -> Multicat sig (s::as) b -> Multicat sig as b

-- | Example Multicategory signature, monoid
data MultiSig : List Ty -> Ty -> Type where 
  UNITM : MultiSig g Unit
  MULTM : MultiSig (M :: M :: g) M

evalMulti : Multicat sig ctx t -> All Val ctx -> Val t 
evalMulti = ?evm 

-- | Concategory over a signature
data Concat : (List o -> List o -> Type) -> List o -> List o -> Type where
  -- Embedding of a generator into a concategory
  In : g as bs -> Concat g as bs
  -- Identity
  Id : Concat g as as
  -- Sequential composition
  Seq : Concat g bs cs -> Concat g as bs -> Concat g as cs

-- | Example con signature, hopf algebra
data ConSig : List Ty -> List Ty -> Type where
--  PUSH    : Val M -> CodeF s (M :: s)
  CREATE  : ConSig s (M :: s)
  MULT    : ConSig (M :: M :: s) (M :: s)
  COPY    : ConSig (n :: s) (n :: n :: s)
  DEL     : ConSig (M :: s) s 
  SWAP    : ConSig (n :: m :: s) (m :: n :: s)

-- Evaluate a concategory into a morphism between two stacks of n-ary products
evalCon : Concat ConSig s t -> All Val s -> All Val t 
evalCon = ?cons 

-- Compact concategory aka Concategory with involution
data InvConcat : (List o -> List o -> Type) -> List o -> List o -> Type where
  -- Embedding of a generator into a concategory
  InI : sig as bs -> InvConcat sig as bs
  -- Identity
  IdI : InvConcat g as as
  -- Sequential composition
  SeqI : InvConcat g bs cs -> InvConcat g as bs -> InvConcat g as cs
  --  NegL   : LK (g |- a::d) -> LK (Neg a :: g |- d)
  NegL : InvConcat sig g (a::d) -> InvConcat sig (Neg a :: g) d 
  --  NegR   : LK (a::g |- d) -> LK (g |- Neg a :: d)
  NegR : InvConcat sig (a::g) d -> InvConcat sig g (Neg a :: d) 
  -- TenL
  TenL : InvConcat sig (a::b::g) d -> InvConcat sig (Ten a b :: g) d 
  -- TenR
  TenR : InvConcat sig g (a::b::d) -> InvConcat sig g (Ten a b :: d) 

-- evaluate an involutive concategory. this might need the Cont monad to do properly. 
evalInv : InvConcat sig s t -> All Val s -> All Val t 
evalInv = ?evinv

-- | Choice category, one-input multi-output
data Term : (Ty -> List Ty -> Type) -> Ty -> List Ty -> Type where 
  CoLet : Term sig s (t::d) -> Term sig t d -> Term sig s d 
  Case : Term sig g [a, b] -> Term sig a [c1] -> Term sig b [c2] -> Term sig g [c2, c1]

-- | Example choice signature
data ChoiceSig : Ty -> List Ty -> Type where 

-- Evaluator for a choice-category
eval : Term ChoiceSig t ctx -> Val t -> Choice Val ctx 
eval (CoLet t1 t2) v = ?lets 
eval (Case t1 t2 t3) v = case eval t1 v of 
  Here v => There (eval t2 v)
  There (Here t) => let (Here ev) = eval t3 t in Here ev

-- Polycategory. Conjunctive vs Disjunctive products
data Poly : (List Ty -> List Ty -> Type) -> List Ty -> List Ty -> Type where 
  CaseP : Poly sig g [a, b] -> Poly sig (a::g) [c1] -> Poly sig (b::g) [c2] -> Poly sig g [c2, c1]

-- Example poly signature. 
data PolySig : List Ty -> List Ty -> Type where 

-- Evaluate a polycategory into a morphism between n-ary sums and n-ary products
evalP : Poly PolySig s t -> All Val s -> Choice Val t 
evalP = ?evps

-- | Rig-contexts
Rig : Type -> Type 
Rig t = List (List t)

-- | Rig-concategory
data RigCat : (Rig Ty -> Rig Ty -> Type) -> Rig Ty -> Rig Ty -> Type where 
  -- Embedding of a generator into a concategory
  InR : g as bs -> RigCat g as bs
  -- Identity
  IdR : RigCat g as as
  -- Sequential composition
  SeqR : RigCat g bs cs -> RigCat g as bs -> RigCat g as cs

RigEnv : (p : k -> Type) -> Rig k -> Type 
RigEnv p k = Choice (All p) k

evalR : RigCat sig s t -> RigEnv Val s -> RigEnv Val t  
evalR = ?rs 

-- | Compact Rig-concategory