https://www.fpcomplete.com/user/edwardk/recursion-schemes/catamorphisms

Fix.hs

{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE UndecidableInstances #-}

module Fix where

-- Definitions:
--
-- If (μF,inF) is the initial F-algebra for some endofunctor F
-- and (X,φ) is an F-algebra, then there is an unique F-algebra
-- homomorphism from (μF,inF) to (X,φ), which is denoted (|φ|)F.
--
--               inF
--         FμF -----> μF       <= initial F-algebra    cata  <-  ana  ->
--          |           |                                     |        ^
-- F(|φ|)  |           | (|φ|) <= catamorphism              v        |
--          |           |                                      ->       <-
--          v           v
--          FX  ----->  X        <= F-algebra
--                φ
--
-- Laws:
--
-- Rule:            Haskell
-- cata-cancel      cata phi . InF = phi . fmap (cata phi)
-- cata-refl        cata InF = id
-- cata-fusion      f . phi = phi . fmap f => f . cata phi = cata phi
-- cata-compose     eps :: f :~> g => cata phi . cata (In . eps) = cata (phi . eps)
--

type Algebra f a = f a -> a

newtype Mu f = InF { outF :: f (Mu f) } -- μF ≅ FμF, so Mu f = f (Mu f) expresses it.

instance Show (f (Mu f)) => Show (Mu f) where
    show x = "(" ++ show (outF x) ++ ")"

cata :: Functor f => Algebra f a -> Mu f -> a -- Algebra f a is the type of φ. For lifting φ, f must be a Functor. 
cata f = f . fmap (cata f) . outF             -- (of course, f is an endofunctor according to the presupposition)

-- cata f = hylo f outF
-- cata f = para (f . fmap fst)

type CoAlgebra f a = a -> f a

ana :: Functor f => CoAlgebra f a -> a -> Mu f
ana f = InF . fmap (ana f) . f

hylo :: Functor f => Algebra f b -> CoAlgebra f a -> (a -> b)
hylo phi psi = cata phi . ana psi

-------------------------------------------------------------------------------------

data StrF x = Cons Char x | Nil
type Str = Mu StrF

nil :: Str
nil = InF Nil

cons :: Char -> Str -> Str
cons x xs = InF (Cons x xs)

instance Functor StrF where
    fmap  f (Cons a as) = Cons a (f as)
    fmap _f Nil = Nil

length :: Str -> Int
length = cata phi where
    phi (Cons _a b) = 1 + b  -- phi :: Mu StrF -> Int
    phi Nil = 0

-------------------------------------------------------------------------------------

data NatF a = S a | Z deriving (Eq,Show)

type Nat = Mu NatF

instance Functor NatF where
    fmap _f Z = Z
    fmap  f (S z') = S (f z')

z :: Nat
z = InF Z

s :: Nat -> Nat
s = InF . S

plus :: Nat -> Nat -> Nat
plus n = cata phi where
    phi Z = n
    phi (S m) = s m

times :: Nat -> Nat -> Nat
times n = cata phi where
    phi Z = z
    phi (S m) = plus n m

-------------------------------------------------------------------------------------
-- Mendler Style

type MendlerAlgebra f c = forall a. (a -> c) -> f a -> c

mcata :: MendlerAlgebra f c -> Mu f -> c
mcata phi = phi (mcata phi) . outF

--   mcata phi
-- = {- definition -}
--   phi (mcata phi) . outF
-- = phi (phi (mcata phi) . outF) . outF

cata' :: Functor f => Algebra f c -> Mu f -> c
cata' phi = mcata (\f -> phi . fmap f)


-------------------------------------------------------------------------------------
-- Mendler and the Yoneda Lemma

-- The definition of a Mendler-sytle algebra above can be seen as the
-- application of Yoneda lemma to the functior in question.
--
-- In type theoretic terms, the Yoneda lemma states that there is an
-- isomorphism between (f a) and ∃b. (b -> a, f b), which can be witnessed
-- by the following definitions.

data CoYoneda f a = forall b. CoYoneda (b -> a) (f b)

toCoYoneda :: f a -> CoYoneda f a
toCoYoneda = CoYoneda id

fromCoYoneda :: Functor f => CoYoneda f a -> f a
fromCoYoneda (CoYoneda f v) = fmap f v

-- Note that in Haskell using an existential requires the use of data, so
-- there is an extra bottom that can inhabit this type that prevents this
-- from being a true isomorphism.
--
-- However, when used in the context of a (CoYoneda f)-Algebra we can
-- rewrite this to use universal quantification because the functor f only
-- occurs in negative position, eliminating the spurious bottom.
--
-- Algebra (CoYoneda f) a
-- = {- by definition -}
--   CoYoneda f a -> a
-- ~ {- by definition -}
--   (exists b. (b -> a, f b)) -> a
-- ~ {- lifting the existential -}
--   forall b. (b -> a, f b) -> a
-- ~ {- by currying -}
--   forall b. (b -> a) -> f b -> a
-- = {- by definition -}
--   MendlerAlgebra f a

-------------------------------------------------------------------------------------
-- Generalized Catamorphisms

-- Most more advanced recursion schemas for foling structures, such as
-- paramorphisms and zygomorphisms can be seen in a common framework as
-- "generalized" catamorphisms. A generalized catamorphism is defined in
-- terms of an F-W-algebra and a distributive law for the comonad W over
-- the functor F which preserves the structure of the comonad W.

class Functor w => Comonad w where
    extract :: w a -> a
    
    duplicate :: w a -> w (w a)
    duplicate = extend id

    extend :: (w a -> b) -> w a -> w b
    extend f = fmap f . duplicate

liftW :: Comonad w => (a -> b) -> w a -> w b
liftW f = extend (f . extract)

type Dist f w = forall a. f (w a) -> w (f a)
type FWAlgebra f w a = f (w a) -> a

g_cata :: (Functor f, Comonad w)
       => Dist f w -> FWAlgebra f w a -> Mu f -> a
g_cata k g = extract . c where
    c = liftW g . k . fmap (duplicate . c) . outF