fixpointcata.idr

module Cata

import Data.Morphisms

data Expr a
  = Lit Int
  | Plus a a
  | Times a a
  
instance Show (Expr a) where
  show x = "<expr>"
  
data Fix : (Type -> Type) -> Type  where
  In : (Functor f) => f (Fix f) -> Fix f

instance Functor Expr where
  map f (Lit i) = Lit i
  map f (Plus a b) = Plus (f a) (f b)
  map f (Times a b) = Times (f a) (f b)
  
data Catamorphism : (Type -> Type) -> Type -> Type where
  Cata : Functor f => (f a -> a) -> Catamorphism f a

value : Expr Int -> Int
value (Lit i) = i
value (Plus a b) = a + b
value (Times a b) = a * b

runCata : Catamorphism f a -> Fix f -> a
runCata (Cata f) (In t) = f (map (runCata (Cata f)) t)

valueCata : Catamorphism Expr Int
valueCata = Cata value

main : IO ()
main = print $ runCata valueCata (In (Plus (In (Lit 5)) (In (Lit 2))))