recursor

FAlg.hs

data I = T | F
data TreeF :: (I -> Type) -> (I -> Type) where
  Tip    :: Int -> TreeF f T
  Forest :: f F -> TreeF f T
  Nil    :: TreeF f F
  Cons   :: f T -> f F -> TreeF f F

data Tree :: I -> Type where
  Fold :: TreeF Tree i -> Tree i

mapTreeF :: forall (f :: I -> Type) (g :: I -> Type).
            (forall i. f i -> g i) -> (forall i. TreeF f i -> TreeF g i)
mapTreeF phi (Tip n)    = Tip n
mapTreeF phi (Forest f) = Forest (phi f)
mapTreeF phi (Nil)      = Nil
mapTreeF phi (Cons t f) = Cons (phi t) (phi f)

recTree :: forall (f :: I -> Type).
           (forall i. TreeF f i -> f i) -> (forall i. Tree i -> f i)
recTree alg (Fold t) = alg (mapTreeF (recTree alg) t)

IndexedInd.hs

data I = T | F
data Tree :: I -> Type where
  Tip    :: Int -> Tree T
  Forest :: Tree F -> Tree T
  Nil    :: Tree F
  Cons   :: Tree T -> Tree F -> Tree F

recTree :: forall (a :: I -> Type). (Int -> a T) -> (a F -> a T) -> (a F) -> (a T -> a F -> a F) -> forall i. Tree i -> a i
recTree tip forest nil cons (Tip n)    = tip n
recTree tip forest nil cons (Forest f) = forest (recTree tip forest nil cons f)
recTree tip forest nil cons (Nil)      = nil
recTree tip forest nil cons (Cons t f) = cons (recTree tip forest nil cons t) (recTree tip forest nil cons f)

MutInd.hs

data Tree = Tip Int | Forest Forest
data Forest = Nil | Cons Tree Forest

recTree :: (Int -> a) -> (b -> a) -> b -> (a -> b -> b) -> Tree -> a
recTree tip forest nil cons (Tip n) = tip n
recTree tip forest nil cons (Forest f) = forest (recForest tip forest nil cons f)

recForest :: (Int -> a) -> (b -> a) -> b -> (a -> b -> b) -> Forest -> b
recForest tip forest nil cons Nil = nil
recForest tip forest nil cons (Cons t f) = cons (recTree tip forest nil cons t) (recForest tip forest nil cons f)