FixMuNu

FixMuNu.hs

{-# LANGUAGE GADTs #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE UndecidableInstances #-}

{-# LANGUAGE ImplicitParams #-}

module FixMuNu where

--newtype Fix f = Fix { runFix :: f (Fix f) }
--newtype Mu f = Mu { runMu :: forall r. (f r -> r) -> r }
--data Nu f = forall x. Nu x (x -> f x)

newtype Fix f where
  Fix :: forall f. f (Fix f) -> Fix f

newtype Mu f where
  Mu :: forall f.  (forall r. (f r -> r) -> r) -> Mu f

data Nu f where
  Nu :: forall f x. x -> (x -> f x) -> Nu f

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

runMu :: Mu f -> (f r -> r) -> r
runMu (Mu f) = f

--

instance Show (f (Fix f)) => Show (Fix f) where
  showsPrec p (Fix x) = showParen (p > 10)
                      $ showString "Fix " . showsPrec 11 x

instance Show (Fix f) => Show (Mu f) where
  showsPrec p mu = showParen (p > 10)
                 $ showString "fixMu " . showsPrec 11 (muFix mu)

instance (Functor f, Show (Fix f)) => Show (Nu f) where
  showsPrec p nu = showParen (p > 10)
                 $ showString "fixNu " . showsPrec 11 (nuFix nu)

--

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

fixOut :: Fix f -> f (Fix f)
fixOut = runFix

muIn :: Functor f => f (Mu f) -> Mu f
muIn fmuf = Mu (\f -> f . fmap (`runMu` f) $ fmuf)

muOut :: Functor f => Mu f -> f (Mu f)
muOut = (`runMu` fmap muIn)

nuIn :: Functor f => f (Nu f) -> Nu f
nuIn = (`Nu` fmap nuOut)

nuOut :: Functor f => Nu f -> f (Nu f)
nuOut (Nu x f) = fmap (`Nu` f) (f x)

--

fixMu :: Functor f => Fix f -> Mu f
fixMu = muIn . fmap fixMu . fixOut

nuMu :: Functor f => Nu f -> Mu f
nuMu = muIn . fmap nuMu . nuOut

nuFix :: Functor f => Nu f -> Fix f
nuFix = fixIn . fmap nuFix . nuOut

muFix :: Mu f -> Fix f
muFix = (`runMu` fixIn)

muNu :: Functor f => Mu f -> Nu f
muNu = (`runMu` nuIn)

fixNu :: Fix f -> Nu f
fixNu = (`Nu` fixOut)

--

fixZero, fixOne, fixTwo :: Fix Maybe
fixZero = Fix Nothing
fixOne  = Fix . Just . Fix $ Nothing
fixTwo  = Fix . Just . Fix . Just . Fix $ Nothing

muZero, muOne, muTwo :: Mu Maybe
muZero = Mu $ \f -> f Nothing
muOne  = Mu $ \f -> f . Just . f $ Nothing
muTwo  = Mu $ \f -> f . Just . f . Just . f $ Nothing

nuZero, nuOne, nuTwo :: Nu Maybe
nuZero = Nu () (const Nothing)
nuOne  = Nu (Just ()) (fmap (const Nothing))
nuTwo  = Nu (Just (Just ())) (fmap (fmap (const Nothing)))

fixSucc :: Fix Maybe -> Fix Maybe
fixSucc = Fix . Just

muSucc :: Mu Maybe -> Mu Maybe
muSucc mum = Mu (\f -> f (Just (mum `runMu` f)))

nuSucc :: Nu Maybe -> Nu Maybe
nuSucc (Nu x f) = Nu (Just x) (fmap f)

fixToInt :: Fix Maybe -> Integer
fixToInt (Fix Nothing)     = 0
fixToInt (Fix (Just fixm)) = 1 + fixToInt fixm

muToInt :: Mu Maybe -> Integer
muToInt (Mu f) = f go
  where
    go Nothing  = 0
    go (Just r) = 1 + r

nuToInt :: Nu Maybe -> Integer
nuToInt (Nu x f) = go x
  where
    go y = case f y of
      Nothing -> 0
      Just z  -> 1 + go z

--

fixZero' :: Fix Maybe
fixZero' = fixIn Nothing

muZero' :: Mu Maybe
muZero' = muIn Nothing

nuZero' :: Nu Maybe
nuZero' = nuIn Nothing

fixSucc' :: Fix Maybe -> Fix Maybe
fixSucc' = fixIn . Just

muSucc' :: Mu Maybe -> Mu Maybe
muSucc' = muIn . Just

nuSucc' :: Nu Maybe -> Nu Maybe
nuSucc' = nuIn . Just

fixToInt' :: Fix Maybe -> Integer
fixToInt' = maybe 0 (succ . fixToInt') . fixOut

muToInt' :: Mu Maybe -> Integer
muToInt' = maybe 0 (succ . muToInt') . muOut

nuToInt' :: Nu Maybe -> Integer
nuToInt' = maybe 0 (succ . nuToInt') . nuOut