RecursionPrinciples.hs

module RecursionPrinciples where

data List a = Nil | Cons a (List a)
    --         1  +     (a * r )

    -- foldr   : (() -> r) -> ((a, r) -> r) -> List a -> r
    -- unfoldr : (r -> Maybe (a, r))        -> r -> [a]
foldr_list :: ((a, r) -> r) -> r -> List a -> r
foldr_list _ r Nil = r
foldr_list f r (Cons a as) = foldr_list f (f (a, r)) as

unfoldr_list :: (r -> Maybe (a, r)) -> r -> List a
unfoldr_list f r =
    case f r of
      Nothing -> Nil
      Just (a, r) -> Cons a (unfoldr_list f r)

data Tree a = Leaf | Node (Tree a) a (Tree a)
    --          1  +  (r * a * r)

    -- foldr   : (() -> r) -> (a -> r -> r -> r) -> Tree a -> r
    -- unfoldr : (r -> Maybe (r, a, r)) -> r -> Tree a

unfoldr_tree :: (r -> Maybe (r, a, r)) -> r -> Tree a
unfoldr_tree f r =
    case f r of
      Nothing -> Leaf
      Just (l, a, r) -> Node (unfoldr_tree f l) a (unfoldr_tree f r)

data Nat = S Nat | Z
    --     r     + 1

    -- foldr_nat   : ((r -> r) -> () -> r) -> Nat -> r
    -- unfoldr_nat : (r -> Maybe r) -> r -> Nat

foldr_nat :: (r -> r) -> r -> Nat -> r
foldr_nat _ r Z = r
foldr_nat f r (S n ) = foldr_nat f (f r) n

unfoldr_nat :: (r -> Maybe r) -> r -> Nat
unfoldr_nat f r =
    case f r of
      Nothing -> Z
      Just r -> S (unfoldr_nat f r)

pow :: (Monoid m) => m -> Nat -> m
pow m n = foldr_nat (mappend m) m n

data Rose a = a :> [Rose a]
--            a  * [r]

foldRose :: ((a, [r]) -> r) -> Rose a -> r 
foldRose f (a :> rs) = f (a, fmap (foldRose f) rs)

unfoldRose :: (r -> (a, [r])) -> r -> Rose a
unfoldRose f r = 
  let (a, xs) = f r
  in a :> fmap (unfoldRose f) xs