Continuations and opposite kinds

ContKind.idr

namespace OpKind
  data Kind : Type where 
    Set : Kind -- Set
    Op : Kind -> Kind -- Set^op
  
  data Ty : Kind -> Type where 
    NAT : Ty k 
    Zero : Ty k
    Add : Ty k -> Ty k -> Ty k 
    One : Ty k
    Mult : Ty k -> Ty k -> Ty k 
-- what should negation be?
--    Neg : Ty (Op k) -> Ty k

  -- values represent inert terms in both Set and Set^op
  data Value : Ty k -> Ty k -> Type where
    Id  : Value a a
    Inl  : Value a (Add a b) 
    Inr  : Value b (Add a b) 
    InTen : {g, a, b : Ty k} -> Value g a -> Value g b -> Value g (Mult a b)
    Triv : Value co One

  EvalKind : Kind -> Type 
  EvalKind Set = Type -- Set
  EvalKind (Op x) = Type -- Set^op has same objects as Set?

  EvalArr : Type -> (k : Kind) -> Type -> Type -> Type 
  EvalArr r Set s t = (t -> r) -> s -> r   -- Interpret Set in Kleisli Cont 
  EvalArr r (Op k) s t = EvalArr r k t s   -- interpret C^op by flipping s and t 

  EvalTy : Type -> (k : Kind) -> Ty k -> Type 
  -- interpret objects of Set as before
  EvalTy r Set NAT = Nat
  EvalTy r Set (Add x y) = Either (EvalTy r Set x) (EvalTy r Set y)
  EvalTy r Set (Mult x y) = Pair (EvalTy r Set x) (EvalTy r Set y)
  EvalTy r Set One = Unit
  EvalTy r Set Zero = Void

  -- `Op Set` is interpreted by flipping product and coproducts 
  EvalTy r (Op Set) (NAT) = Nat
  EvalTy r (Op Set) (Zero) = Unit
  EvalTy r (Op Set) (One) = Void
  EvalTy r (Op Set) ((Add x y)) = Pair (EvalTy r (Op Set) x) (EvalTy r (Op Set) y) 
  EvalTy r (Op Set) ((Mult x y)) = Either (EvalTy r (Op Set) x) (EvalTy r (Op Set) y)

  -- `Op k` is evaluated by...?
  EvalTy r (Op k) ty = EvalTy r k ?xo -- <- cant evaluate without negation?


  evalVal : (k : Kind) -> {s, t : Ty k}  
        -> Value s t -> EvalArr r k (EvalTy r k s) (EvalTy r k t)  
  evalVal Set Id = id
  evalVal Set Inl = \f => \y => f $ Left y
  evalVal Set Inr = \f => \y => f $ Right y
  evalVal Set (InTen x y) = ?evalVal_rhs_5
  evalVal Set Triv = ?evalVal_rhs_6
  evalVal (Op Set) Id = id
  evalVal (Op Set) Inl = \f => \y => f ?evalVal_rhs_10
  evalVal (Op Set) Inr = ?evalVal_rhs_11
  evalVal (Op Set) (InTen x y) = ?evalVal_rhs_12
  evalVal (Op Set) Triv = ?evalVal_rhs_13
  evalVal (Op (Op y)) x = ?evalVal_rhs_8