-- Solving Fix / Mu / Nu exercise in
-- https://stackoverflow.com/questions/45580858/what-is-the-difference-between-fix-mu-and-nu-in-ed-kmetts-recursion-scheme-pac

{-# LANGUAGE RankNTypes, GADTs #-}

----------------------------------------
-- Fix / Mu / Nu

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

inFix :: f (Fix f) -> Fix f
inFix = Fix

outFix :: Fix f -> f (Fix f)
outFix (Fix f) = f

newtype Mu f = Mu { unMu :: forall a. (f a -> a) -> a }

inMu :: Functor f => f (Mu f) -> Mu f
inMu fmu = Mu $ \f -> f (flip unMu f <$> fmu)

outMu :: Functor f => Mu f -> f (Mu f)
outMu = flip unMu $ fmap inMu

data Nu f where
    Nu ::(a -> f a) -> a -> Nu f

inNu :: Functor f => f (Nu f) -> Nu f
inNu = Nu (fmap outNu)

outNu :: Functor f => Nu f -> f (Nu f)
outNu (Nu f a) = Nu f <$> f a

----------------------------------------
-- Catamorphism / Anamorphism

cataFix :: Functor f => (f a -> a) -> Fix f -> a
cataFix alg = alg . fmap (cataFix alg) . unFix

cataMu :: (f a -> a) -> Mu f -> a
cataMu f (Mu g) = g f

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

anaNu :: (a -> f a) -> a -> Nu f
anaNu g a = Nu g a

----------------------------------------
-- Mu <-> Fix <-> Nu isomorphism (in Haskell)

muToFix :: Mu f -> Fix f
muToFix (Mu f) = f Fix

-- Requires recursion.
fixToMu :: Functor f => Fix f -> Mu f
fixToMu x = Mu (flip cataFix x)

fixToNu :: Fix f -> Nu f
fixToNu x = Nu unFix x

-- Requires recursion.
nuToFix :: Functor f => Nu f -> Fix f
nuToFix (Nu coalg a) = Fix (fmap (anaFix coalg) (coalg a))

----------------------------------------
-- Natural / Co-Natural

zeroMu :: Mu Maybe
zeroMu = Mu $ \alg -> alg Nothing

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

muToInt :: Mu Maybe -> Int
muToInt (Mu f) = f alg
  where
    alg Nothing = 0
    alg (Just n) = 1 + n

zeroNu :: Nu Maybe
zeroNu = Nu (const Nothing) ()

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

inftyNu :: Nu Maybe
inftyNu = Nu Just ()

nuToInt :: Nu Maybe -> Int
-- nuToInt nu = muToInt . fixToMu . nuToFix $ nu
nuToInt (Nu coalg a) = f (coalg a)
  where
    f Nothing = 0
    f (Just x) = 1 + f (coalg x)

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

main :: IO ()
main = do
    -- Mu
    print $ muToInt $ zeroMu -- 0
    print $ muToInt $ succMu $ zeroMu -- 1
    print $ muToInt $ succMu . succMu $ zeroMu -- 2

    -- Nu
    print $ nuToInt $ zeroNu -- 0
    print $ nuToInt $ succNu $ zeroNu -- 1
    print $ nuToInt $ succNu . succNu $ zeroNu -- 2
    print $ nuToInt $ inftyNu -- infinity