Folding/Unfolding

anacata.hs

 {-# LANGUAGE NPlusKPatterns #-}
module Main where

import Test.QuickCheck

data NatF a
  = ZeroF
  | SuccF a

instance Functor NatF where
  fmap _ ZeroF     = ZeroF
  fmap f (SuccF x) = SuccF (f x)

newtype Fix f = Fix { runFix :: f (Fix f) }

type Nat = Fix NatF

type Algebra f a = f a -> a

alg :: Algebra NatF Int
alg ZeroF     = 0
alg (SuccF n) = n + 1

-- | Folding
cata :: Functor f => Algebra f b -> Fix f -> b
cata alg = alg . fmap (cata alg) . runFix

type CoAlgebra f a = a -> f a

coAlg :: CoAlgebra NatF Int
coAlg 0       = ZeroF
coAlg (n + 1) = SuccF n

-- | Unfolding
ana :: Functor f => CoAlgebra f b -> b -> Fix f
ana coAlg = Fix . fmap (ana coAlg) . coAlg

prop_ana_cata_inverse :: Int -> Property
prop_ana_cata_inverse n = n >= 0 ==>
  cata alg (ana coAlg n) == n

main :: IO ()
main = quickCheck prop_ana_cata_inverse