Church encoding of initial algebras

church.hs

{-# LANGUAGE RankNTypes, DeriveFunctor #-}

-- The usual recursive way of obtaining the initial algebra of a functor f
newtype Mu f = In { inOp :: f (Mu f) }

cata :: Functor f => (f a -> a) -> Mu f -> a
cata alg = alg . fmap (cata alg) . inOp

-- Church encoding of initial algebras
type Mu' f = forall a . (f a -> a) -> a

cata' :: Functor f => (f a -> a) -> Mu' f -> a
cata' alg x = x alg

-- These two ways are isomorphic 

iso :: Functor f => Mu f -> Mu' f
iso x = \ alg -> cata alg x

isoOp :: Functor f => Mu' f -> Mu f
isoOp y = y In

{-

These two definitions are isomorphic:

   iso (isoOp y)
=  iso (y In)
=  \alg -> cata alg (y In)
   {- Parametricity of |y|: |In| and |alg| are related by |cata alg| (as an algebra morphism). 
      Thus |y In| and |y alg| are related by |cata alg| (as a function) too. -}
=  \alg -> y alg
=  y

   isoOp (iso x)
=  isoOp (\alg -> cata alg x)
=  (\alg -> cata alg x) In
=  cata In x
   {- reflection law: there is exactly one morphism |id| from algebra |In| to |In| -}
=  x

-}

-- As an example, defining lists with Mu'
data ListF a x = Nil | Cons a x deriving Functor

type List a = Mu' (ListF a)

-- Then append is automatically O(1) because |append xs ys| only creates a new function.
-- In fact, it's an application of Cayley's theorem. How beautiful!
append :: List a -> List a -> List a
append xs ys alg = xs k where
  k Nil         = ys alg
  k (Cons a b)  = alg (Cons a b)