Recursion schemes in Idris starter pack

Fix.idr

-- standard algebra 
Algebra : (Type -> Type) -> Type -> Type  
Algebra f a = f a -> a

-- Mendler Algebra == Algebra (Coyoneda f) a
MAlgebra : (Type -> Type) -> Type -> Type
MAlgebra f c = {x : Type} -> (x -> c) -> f x -> c

data Coyoneda : (Type -> Type) -> Type -> Type  where
  Coyo : (a -> b) -> f a -> Coyoneda f b

-- Fix
data Mu : (pattern : Type -> Type) -> Type where
    In : {f: Type -> Type} -> f (Mu f) -> Mu f

-- Catamorphism
cata : Functor f => Algebra f a -> Mu f -> a
cata alg (In op) = alg (map (cata alg) op)

-- Mendler catamorphism
mcata : Algebra (Coyoneda f) c -> Mu f -> c
mcata alg (In op) = alg $ Coyo (mcata alg) op

-- example of a pattern functor with a fixed carrier, Nat
namespace FixedCarrier 
  -- Pattern functor for addition over Naturals 
  data ArithF a = Val Nat | Add a a 

  -- Functor for ArithF
  Functor ArithF where 
    map f (Val n) = Val n 
    map f (Add a b) = Add (f a) (f b)

  -- | Algebra for addition
  addAlg : ArithF Nat -> Nat
  addAlg (Val i)  = i
  addAlg (x `Add` y) = x + y

  -- | Algebra for multiplication
  multAlg : ArithF Nat -> Nat
  multAlg (Val i)  = i
  multAlg (x `Add` y) = x * y

  -- Arith is a least fixpoint of ArithF
  Arith : Type 
  Arith = Mu ArithF 

  -- Example Term
  ex : Arith
  ex = In $ Add (In $ Val 6) (In $ Val 2) 

  -- Examples of evaluation
  public export
  exeval1 : Nat 
  exeval1 = cata addAlg ex 

  public export
  exeval2 : Nat 
  exeval2 = cata multAlg ex 


-- Same example, but generalised for an arbitrary carrier
namespace GeneralCarrier
  data ArithF a r = Val a | Add r r 

  -- Functor for ArithF
  Functor (ArithF a) where 
    map f (Val n) = Val n 
    map f (Add a b) = Add (f a) (f b)

  -- | Algebra for addition
  addAlg : ArithF Nat Nat -> Nat
  addAlg (Val i)  = i
  addAlg (x `Add` y) = x + y

  -- | Algebra for multiplication
  multAlg : ArithF Nat Nat -> Nat
  multAlg (Val i)  = i
  multAlg (x `Add` y) = x + y

  -- | Algebra for composing strings
  stringAlg : ArithF String String -> String
  stringAlg (Val s)  = s
  stringAlg (x `Add` y) = x ++ y

  -- Example Term for Natural numbers
  ex : Mu (ArithF Nat)
  ex = In $ Add (In (Val 6)) (In (Val 2)) 

  -- Example Term for Strings
  ex' : Mu (ArithF String)
  ex' = In $ Add (In (Val "hello")) (In (Val "world")) 

  public export
  exeval3 : Nat 
  exeval3 = cata addAlg ex 

  public export
  exeval4 : Nat 
  exeval4 = cata multAlg ex 

  public export
  exeval5 : String 
  exeval5 = cata stringAlg ex'