Free Cartesian Categories using Recursion Schemes

CartCata.idr

infixr 5 ~~> -- Morphisms of graphs

-- | Boilerplate for recursion schemes

-- Objects are graphs 
Graph : Type -> Type 
Graph o = o -> o -> Type 

-- Morphisms are vertex-preserving transformations between graphs
(~~>) : {o : Type} -> (o -> o -> Type) -> (o -> o -> Type) -> Type  
(~~>) f g = {s, t : o} -> f s t -> g s t 

-- Fixpoints of functors over graphs 
data Mu : (Graph o -> Graph o) -> Graph o where
  In : {f : Graph o -> Graph o} -> f (Mu f) ~~> Mu f

-- F-Algebras over the category of graphs
Algebra : {o : Type} -> (Graph o -> Graph o) -> Graph o -> Type
Algebra f a = f a ~~> a 

-- Coyoneda lemma for the category of graphs
data Coyoneda : {o : Type} -> (pattern: (Graph o -> Graph o)) -> Graph o -> Graph o  where
  Coyo : f ~~> g -> h f ~~> Coyoneda h g

-- Mendler Algebras over 'f' are Algebras over 'Coyoneda f' 
MAlgebra : {o : Type} -> (Graph o -> Graph o) -> Graph o -> Type
MAlgebra f c = Algebra (Coyoneda f) c 

-- Mendler catamorphism - doesn't require a functor constraint
mcata : MAlgebra f c -> Mu f ~~> c
mcata alg (In op) = alg $ Coyo (mcata alg) op

-- A category of Idris types
Idr : Graph Type
Idr a b = a -> b 

-- | Our first example
namespace Category
  -- Pattern functor for a free category over a graph 
  data CatF : Graph obj -> Graph obj -> Graph obj where 
    Id : CatF g h a a 
    Comp : {g, h : Graph obj} -> {a, b, c : obj} -> g b c -> h a b -> CatF g h a c 

  -- A free category over a graph is the least fixpoint of our CatF functor
  Cat : Graph obj -> Graph obj 
  Cat g = Mu (CatF g)

  -- Example Algebra, the category of Idris functions
  IdrAlg : Algebra (CatF Idr) Idr
  IdrAlg Id = id 
  IdrAlg (Comp f g) = f . g 

  -- Mendler Algebra version
  IdrAlg' : MAlgebra (CatF Idr) Idr 
  IdrAlg' (Coyo cont Id) = id 
  IdrAlg' (Coyo cont (Comp f g)) = f . (cont g) 

  -- We get the evaluator for free
  evalIdr : MAlgebra (CatF Idr) Idr -> Algebra Cat Idr 
  evalIdr = mcata 
  
  
-- | Let's try a more involved version, this time with types
namespace Cartesian
  -- Cartesian Types
  data Ty : Type -> Type where
    Base : a -> Ty a 
    Prod : Ty a -> Ty a -> Ty a  

  -- Base functor for the Free Cartesian Category over a graph with products 
  data CartCatF : Graph (Ty obj) -> Graph (Ty obj) -> Graph (Ty obj) where 
    Id : CartCatF g h a a 
    Comp : {g : Graph (Ty obj)} -> {a, b, c : Ty obj} 
      -> g b c -> h a b -> CartCatF g h a c
    Prj1 : {a, b : Ty obj} -> CartCatF g h (Prod a b) a
    Prj2 : {a, b : Ty obj} -> CartCatF g h (Prod a b) b
    ProdI : {a, b, c : Ty obj} -> h a b -> h a c -> CartCatF g h a (Prod b c)

  -- A free cartesian category is the least fixpoint of our base functor
  CartCat : Graph (Ty obj) -> Graph (Ty obj) 
  CartCat g = Mu (CartCatF g)

  -- Before we define an example algebra, we must translate the types
  
  -- Evaluate cartesian types into Idris products
  evalTy : Ty Type -> Type 
  evalTy (Base a) = a 
  evalTy (Prod a b) = (evalTy a, evalTy b)

  -- Translate morphisms between cartesian types into Idris functions
  IdrCar : Ty Type -> Ty Type -> Type 
  IdrCar a b = (evalTy a) -> (evalTy b)

  -- Algebra for a free cartesian category over Idris types
  cartAlgIdr : Algebra (CartCatF IdrCar) IdrCar  
  cartAlgIdr Id = id 
  cartAlgIdr (Comp f g) = f . g
  cartAlgIdr Prj1  = fst
  cartAlgIdr Prj2 = snd
  cartAlgIdr (ProdI f g) = \c => (f c, g c)

  -- Mendler version
  cartAlgIdr' : MAlgebra (CartCatF IdrCar) IdrCar  
  cartAlgIdr' (Coyo cont Id) = id 
  cartAlgIdr' (Coyo cont (Comp f g)) = f . (cont g)
  cartAlgIdr' (Coyo cont Prj1) = fst
  cartAlgIdr' (Coyo cont Prj2) = snd
  cartAlgIdr' (Coyo cont (ProdI f g)) = \c => ((cont f) c, (cont g) c)

  -- We get our evaluator for free
  evalCart : MAlgebra (CartCatF (IdrCar)) IdrCar -> Algebra CartCat IdrCar
  evalCart = mcata