RecursionSchemes.hs

{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE DeriveFunctor #-}
module RecursionSchemes where

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

import Data.Smash
import Data.Function ((&))

--------------------------------------------------------------------------------
-- F-Algebras and Fixed Points

type Algebra f a = f a -> a
type Coalgebra f a = a -> f a

-- | The Fixed Point of @f@
newtype Fix f = Fix { unfix :: f (Fix f) }

-- | Given a natural transformation between two functors @f@ and @g@,
-- we can map from 'Fix' of @f@ to 'Fix' of @g@.
hoistFix :: Functor f => (forall a. f a -> g a) -> Fix f -> Fix g  
hoistFix nt (Fix f) = Fix $ nt (fmap (hoistFix nt) f)

-- | 'Nu' represents a recursive type as its unfold. 'Nu f' is the
-- greatest (aka terminal) fixed point of 'f'.
data Nu f where
  Nu :: Coalgebra f a -> a -> Nu f

-- | 'Mu' represents a recursive type as its fold. 'Mu f' is the least
-- (aka initial) fixed point of 'f'.
newtype Mu f = Mu { unmu :: forall a. Algebra f a -> a } 

inMu :: Functor f => f (Mu f) -> Mu f
inMu fmu = Mu $ \fa -> fa $ fmap (flip unmu fa) fmu

outMu :: Functor f => Mu f -> f (Mu f)
outMu (Mu f) = undefined

--------------------------------------------------------------------------------
-- Catamorphism

cataFix :: Functor f => Algebra f a -> Fix f -> a
cataFix alg fix = alg $ fmap (cataFix alg) $ unfix fix

cataNu :: Functor f => Algebra f a -> Nu f -> a
cataNu alg (Nu coalg seed) = seed & hylo alg coalg

cataNu' :: Functor f => Algebra f a -> Nu f -> a
cataNu' alg (Nu coalg seed) =
  let f = alg . fmap f . coalg
  in f seed

cataMu :: Functor f => Algebra f a -> Mu f -> a
cataMu alg (Mu f) = f alg

--------------------------------------------------------------------------------
-- Anamorphism

anaFix :: Functor f => Coalgebra f a -> a -> Fix f
anaFix coalg = Fix . fmap (anaFix coalg) . coalg

anaNu :: Functor f => Coalgebra f a -> a -> Nu f
anaNu coalg seed = Nu coalg seed

anaMu' :: Functor f => Coalgebra f a -> a -> Mu f
anaMu' coalg seed = Mu \alg ->
  let h = alg . fmap h . coalg
  in h seed

anaMu :: Functor f => Coalgebra f a -> a -> Mu f
anaMu coalg seed = Mu $ \alg -> seed & hylo alg coalg

--------------------------------------------------------------------------------
-- Hylmorphism

hylo :: Functor f => Algebra f b -> Coalgebra f a -> a -> b
hylo alg coalg =
  let h = alg . fmap h . coalg
  in h

data Iso f g = Iso { from :: f -> g, to :: g -> f }

fixNuIso :: Functor f => Iso (Fix f) (Nu f)
fixNuIso = Iso {..}
  where
    from :: Fix f -> Nu f
    from fix = Nu unfix fix

    to :: Functor f => Nu f -> Fix f
    to (Nu coalg seed) = anaFix coalg seed

fixMuIso :: Functor f => Iso (Fix f) (Mu f)
fixMuIso = Iso {..}
  where
    from :: Functor f => Fix f -> Mu f
    from fix = Mu \alg -> cataFix alg fix

    to :: Mu f -> Fix f
    to (Mu alg) = alg Fix

muNuIso :: Functor f => Iso (Mu f) (Nu f)
muNuIso = Iso {..}
  where
    from :: Functor f => Mu f -> Nu f
    from (Mu alg)  = Nu unfix $ alg Fix

    to :: Functor f => Nu f -> Mu f
    to (Nu coalg seed) = Mu \alg -> hylo alg coalg seed

-- | Linked Lists are the fixed point of the smash product on @a@. In
-- other words, 'List a = Fix (Compose Maybe (,) a)'.
type List a = Fix (Smash a)
type List' a = Nu (Smash a) 

listIso :: Iso (List a) [a]
listIso = Iso {..}
  where
    from :: List a -> [a]
    from xf = xf & cataFix \case
       Nada -> []
       Smash x xs -> x : xs

    to :: [a] -> List a
    to xs = xs & anaFix \case
       [] -> Nada
       x : xs' -> Smash x xs'

lengthF :: List a -> Int
lengthF = cataFix \case
   Nada -> 0
   Smash _ i -> i + 1

lengthN :: List' a -> Int
lengthN = cataNu \case
  Nada -> 0
  Smash _ i -> i + 1

--------------------------------------------------------------------------------
-- Naturals

-- | 'Nat' is isomorphic to 'List ()'
natListIso :: Iso (List ()) Nat
natListIso = Iso {..}
  where
    from :: List () -> Nat
    from xs = xs & cataFix \case
       Nada -> Z
       Smash _ nat -> S nat

    to :: Nat -> List ()
    to n = n & anaFix \case
       Z -> Nada
       S nat -> Smash () nat

-- | We can also use fixed points of 'Maybe' to define the naturals.
--
-- We can explain this by expanding out the 'List' alias:
-- List () == Fix (Smash ()) == Fix (Compose Maybe ((,) ())) == Fix Maybe
zeroNu :: Nu Maybe
zeroNu = Nu (const Nothing) Nothing

succNu :: Nu Maybe -> Nu Maybe
succNu (Nu coalg seed) =
  Nu (fmap coalg) (Just seed)

one :: Nu Maybe
one = succNu zeroNu

two :: Nu Maybe
two = succNu $ succNu zeroNu

data Nat = Z | S Nat
  deriving Show

-- | We can prove our 'Nu Maybe' representation with an 'Iso'.
natNuIso :: Iso (Nu Maybe) Nat
natNuIso = Iso {..}
  where
    from :: Nu Maybe -> Nat
    from (Nu coalg seed) =
      case coalg seed of
        Nothing -> Z
        Just a -> S $ from (Nu coalg a)

    to :: Nat -> Nu Maybe
    to = \case
      Z -> zeroNu
      S nat -> succNu $ to nat

-- | Because 'Nu' represents 'Nat' as an Unfold, we can use it to
-- describe infinity.
inftyNu :: Nu Maybe
inftyNu = Nu Just ()

-- | We can also use 'Mu' and 'Fix' to represent 'Nat' but we lose the
-- ability to represent infinity.
zeroMu :: Mu Maybe
zeroMu = Mu $ \alg -> alg Nothing

succMu :: Mu Maybe -> Mu Maybe
succMu (Mu f) = Mu \alg -> alg . Just $ f alg

-- | 'Mu Maybe' is isomorphic to 'Nat'
natMuIso :: Iso (Mu Maybe) Nat
natMuIso = Iso {..}
  where
    from :: Mu Maybe -> Nat
    from (Mu f) = f \case
       Nothing -> Z
       Just nat -> S nat

    to :: Nat -> Mu Maybe
    to = \case
          Z -> zeroMu
          S nat -> succMu $ to nat