Second-Order Algebraic Theories

SOAT.idr

-- Our data-type for signatures
data Signature a = Sig (List a) a

-- Synonym for first-order signatures
infix 4 |-
(|-) : List a -> a -> Signature a
(|-) = Sig

-- Synonym for second-order signatures
infix 4 ||-
(||-) : List a -> a -> Signature a
(||-) = Sig

-- | Let's start with 1-theories

-- First-order signature for the theory of semigroups over natural numbers
data Semigroup : Signature Type -> Type where 
  AddS : Semigroup $ (Nat :: Nat :: s) |- Nat

-- First-order cartesian multicategory over a signature
data Multicat1 : (Signature Type -> Type) -> Signature Type -> Type where 
  Var1 : Multicat1 sig ([s] |- s)
  In1 : sig (ctx |- s) -> Multicat1 sig (ctx |- s)
  Let1 : Multicat1 sig (ctx |- s) -> Multicat1 sig ((s :: ctx) |- t) -> Multicat1 sig (ctx |- t) 

-- An operad for Semigroups
ArithOp : Signature Type -> Type 
ArithOp = Multicat1 Semigroup

-- Environments for first-order signatures
data All : {a : Type} -> (p : a -> Type) -> List a -> Type where 
  Nil : All p Nil 
  Cons : {x : a} -> (px : p x) -> (pxs : All p xs) -> All p (x :: xs)

-- Value predicate for first-order signatures. It's just identity.
Val : Type -> Type 
Val a = a

-- An evaluator for a first-order signature. 
eval1 : Multicat1 Semigroup (ctx |- t) -> All Val ctx -> Val t


-- | Let's do it one more time: Second-order signatures

-- Example second-order signature, the theory of Let binders
data LetSig' : Signature (List Type, Type) -> Type where 
  Let1S' : LetSig' $ ((ctx, s) :: (s::ctx, t) :: g) ||- (ctx, t) 

-- Second-order signatures are actually just signatures of signatures
data LetSig : Signature (Signature Type) -> Type where 
  Let1S : LetSig $ ((ctx |- s) :: (s::ctx |- t) :: g) ||- (ctx |- t) 

-- Second-order cartesian multicategory over second-order signatures. We now have contexts and 2-contexts
data Multicat2 : (Signature (Signature Type) -> Type) -> (Signature (Signature Type) -> Type) where 
  Var2 : Multicat2 sig ([s] ||- s)
  In2 : sig (hctx ||- (ctx |- s)) -> Multicat2 sig (hctx ||- (ctx |- s)) 
  Let2 : Multicat2 sig (hctx ||- (ctx |- s)) -> Multicat2 sig (((ctx |- s) :: hctx) ||- (ctx' |- t)) 
    -> Multicat2 sig (hctx ||- (ctx' |- t)) 

-- A second-order operad for the theory of Let binders
LetOp : Signature (Signature Type) -> Type
LetOp = Multicat2 LetSig

-- Predicate for 2-values
Val2 : Signature Type -> Type 
Val2 (Sig Nil t) = t
Val2 (Sig (l :: ls) t) = l -> Val2 (Sig ls t) 

-- Evaluator for a 2nd order algebraic theory
eval2 : Multicat2 LetSig (hctx ||- (ctx |- t)) -> All Val2 hctx -> Val2 (ctx |- t)

-- | Finally, the most general version

data Multicat : {obj : Type} -> (Signature obj -> Type) -> Signature obj -> Type where  
  Var : Multicat sig ([s] |- s)
  In : sig (ctx |- s) -> Multicat sig (ctx |- s)
  Let : Multicat sig (ctx |- s) -> Multicat sig ((s :: ctx) |- t) -> Multicat sig (ctx |- t) 


-- General evaluator for a multicategory
eval : Multicat sig (ctx |- t) -> All p ctx -> p t

-- Multicat1 is just Multicat where the objects are 'Type'
Multicat1' : (Signature Type -> Type) -> Signature Type -> Type   
Multicat1' = Multicat {obj = Type}

-- Multicat2 is Multicat where objects are 'Signature Type'
Multicat2' : (Signature (Signature Type) -> Type) -> (Signature (Signature Type) -> Type)
Multicat2' = Multicat {obj = Signature Type}

-- Evaluating a first-order theory is a special case
eval1' : Multicat1' Semigroup (ctx |- t) -> All Val ctx -> Val t
eval1' = eval

-- Evaluating a second-order theory is also a special case
eval2' : Multicat2' LetSig (hctx ||- (ctx |- t)) -> All Val2 hctx -> Val2 (ctx |- t)
eval2' = eval 

-- | Finally, an application: Simply-Typed lambda calculus as a second-order theory

-- Types for the STLC
data Ty : Type where 
  N : Ty 
  Fun : Ty -> Ty -> Ty 

-- A second-order signature for simply-typed lambda terms
data LamSig : Signature (Signature Ty) -> Type where 
  Lam : LamSig $ ((s::ctx |- t) :: g) ||- (ctx |- (Fun s t))
  App : LamSig $ ((ctx |- (Fun a b)) :: (ctx |- a) :: g) ||- (ctx |- b)

-- A second-order operad of lambda terms
LambdaOperad : Signature (Signature Ty) -> Type 
LambdaOperad = Multicat LamSig

-- Interpret types
ValTy : Ty -> Type 
ValTy N = Nat 
ValTy (Fun s t) = ValTy s -> ValTy t 

-- Interpret signatures over types
ValTy2 : Signature Ty -> Type 
ValTy2 (Sig Nil t) = ValTy t
ValTy2 (Sig (l :: ls) t) = ValTy l -> ValTy2 (Sig ls t) 

-- We get an evaluator for the lambda calculus for free
evalLam : Multicat LamSig (hctx ||- (ctx |- t)) -> All ValTy2 hctx -> ValTy2 (ctx |- t)
evalLam = eval