Free Operad as a free relative monad over Fin

Operad.idr

import Data.Fin 

-- Free operad over a signature
data Op : (Nat -> Type) -> Nat -> Type where 
  Var : Fin n -> Op f n 
  In : {n : Nat} -> f n -> (Fin n -> Op f m) -> Op f m

-- Algebra over a functor f
Algebra : (Type -> Type) -> Type -> Type 
Algebra f a = f a -> a 

-- Mendler algebra over f
MAlgebra : (Type -> Type) -> Type -> Type
MAlgebra f c = {x : Type} -> (x -> c) -> f x -> c

-- Kan algebra over f
KAlgebra : (Nat -> Type) -> (Nat -> Type) -> Type -> Type
KAlgebra j f c = {x : Nat} -> (j x -> c) -> f x -> c

-- Evaluator for a free operad
eval : (Fin n -> c) -> KAlgebra Fin f c -> Op f n -> c 
eval g alg = go where 
  go : Op f n -> c
  go (Var a) = g a
  go (In op env) = alg (go . env) op

-- Pattern functor for a Semiring
data SemiringF : Type -> Type where
  ZeroF : SemiringF a 
  OneF : SemiringF a
  MultF : a -> a -> SemiringF a
  AddF : a -> a -> SemiringF a 

-- Signature for a Semiring
data SemiringN : Nat -> Type where 
  ZeroN : SemiringN 0
  OneN : SemiringN 0
  MultN : SemiringN 2 
  AddN : SemiringN 2

-- Algebra for a semiring 
nats : Algebra SemiringF Nat
nats (ZeroF) = 0
nats (OneF) = 1
nats (MultF x y) = x + y
nats (AddF x y) = x * y

-- Convert a functor-algebra for a semiring to an operad-algebra for a semiring
toLanAlg : Algebra SemiringF a -> KAlgebra Fin SemiringN a
toLanAlg alg = \env, op => case op of 
  ZeroN => alg ZeroF 
  OneN => alg OneF
  MultN => alg (MultF (env FZ) (env (FS FZ)))
  AddN => alg (MultF (env FZ) (env (FS FZ)))

-- | Example Terms

-- (* x1 (+ x2 x2))
ex1 : Op SemiringN 2
ex1 = In MultN (\f => case f of 
  FZ => Var FZ
  FS FZ => In AddN (\f => case f of 
    FZ => Var (FS FZ)
    FS FZ => Var (FS FZ)))

-- (+ x1 x1)
ex2 : Op SemiringN 1 
ex2 = In AddN (\f => case f of 
  FZ => Var FZ
  FS FZ => Var FZ)

-- example environment
env : Fin 2 -> Nat 
env FZ = 3 
env (FS FZ) = 5

-- (* 3 (+ 5 5)) = 13
e1 : Nat 
e1 = eval env (toLanAlg nats) ex1