{-# LANGUAGE 
    Rank2Types
  , MultiParamTypeClasses
  , FunctionalDependencies
  , FlexibleInstances
  #-}

-----------------------------------------------------------------------------
-- |
-- Module      :  Control.Recursion
-- Copyright   :  2004 Dave Menendez
-- License     :  BSD3
-- 
-- Maintainer  :  dan.doel@gmail.com
-- Stability   :  experimental
-- Portability :  non-portable (rank-2 polymorphism, fundeps)
--
-- Provides implementations of /catamorphisms/ ('fold'), 
-- /anamorphisms/ ('unfold'), and /hylomorphisms/ ('refold'),
-- along with many generalizations implementing various 
-- forms of iteration and coiteration.
--
-- Also provided is a type class for transforming a functor
-- to its fixpoint type and back ('Fixpoint'), along with
-- standard functors for natural numbers and lists ('ConsPair'),
-- and a fixpoint type for arbitrary functors ('Fix').
--
-- Several combinators herein ((g_)futu, (g_)chrono, refoldWith, ...)
-- are due to substantial help by Edward Kmett.
--
-----------------------------------------------------------------------------

module Control.Recursion
  (
  -- * Folding
    fold
  , para
  , zygo
  , histo
  , g_histo
  , foldWith
  
  -- * Unfolding
  , unfold
  , apo
  , g_apo
  , unfoldWith
  , futu
  , g_futu
    
  -- * Transforming
  , refold
  , refoldWith
  , chrono
  , g_chrono

  -- * Dynamic Programming
  , dyna
  , g_dyna
  , codyna
  , g_codyna
    
  -- * Functor fixpoints
  , Fixpoint(..)
  , Fix(..)
  , ConsPair(..)
  , cons
  
  ) where

----
import Control.Arrow
import Control.Functor
import Control.Monad.Identity
import Control.Monad.Free
import Control.Comonad
import Control.Comonad.Cofree

class Functor f => Fixpoint f t | t -> f where
  inF  :: f t -> t
  -- ^ formally, @in[f]: f -> mu f@

  outF :: t -> f t
  -- ^ formally, @in^-1[f]: mu f -> f@

-- | Creates a fixpoint for any functor.
newtype Fix f = In (f (Fix f))

instance Functor f => Fixpoint f (Fix f) where
  inF         = In
  outF (In f) = f

instance Fixpoint Unit () where
  inF Unit = ()
  outF ()  = Unit

instance Fixpoint Maybe Int where
  inF Nothing        = 0
  inF (Just n)       = n + 1
  
  outF n | n > 0     = Just (n - 1)
         | otherwise = Nothing

instance Fixpoint Maybe Integer where
  inF Nothing        = 0
  inF (Just n)       = n + 1
  
  outF n | n > 0     = Just (n - 1)
         | otherwise = Nothing

-- | Fixpoint of lists
data ConsPair a b = Nil | Pair a b deriving (Eq, Show)

instance Functor (ConsPair a) where
  fmap _ Nil        = Nil
  fmap f (Pair a b) = Pair a (f b)

instance Fixpoint (ConsPair a) [a] where
  inF Nil        = []
  inF (Pair a b) = a : b
  
  outF []        = Nil
  outF (x:xs)    = Pair x xs


-- | Deconstructor for 'ConsPair'
cons :: c -> (a -> b -> c) -> (ConsPair a b -> c)
cons d _ Nil        = d
cons _ f (Pair a b) = f a b

{-|
A generalized @map@, known formally as a /hylomorphism/ and written [| f, g |].

@
	refold f g == 'fold' f . 'unfold' g
@
-}
refold :: Functor f => (f b -> b) -> (a -> f a) -> a -> b
refold f g = f . fmap (refold f g) . g

{-|
A generalized @foldr@, known formally as a /catmorphism/ and written (| f |).

@
	fold f == 'refold' f 'outF'
	fold f == 'foldWith' ('Identity' . fmap 'runIdentity') (f . fmap 'runIdentity')
@
-}
fold :: Fixpoint f t => (f a -> a) -> t -> a
fold f = refold f outF

{-|
A generalized @unfoldr@, known formally as an /anamorphism/ and written [( f )].

@
	unfold f == 'refold' 'inF' f
	unfold f == 'unfoldWith' (fmap 'Identity' . 'unIdentity') (fmap 'Identity' . f)
@
-}
unfold :: Fixpoint f t => (a -> f a) -> a -> t
unfold f = refold inF f

{-|
A variant of 'fold' where the function /f/ also receives the result of the
inner recursive calls. Formally known as a /paramorphism/ and written \<| f |\>.
Dual to 'apo'.

@
	para   == 'zygo' 'inF'
	para f == 'refold' f (fmap (id &&& id) . 'outF')
	para f == f . fmap (id &&& para f) . 'outF'
@

Example: Computing the factorials.

> fact :: Integer -> Integer
> fact = para g
>   where
>     g Nothing      = 1
>     g (Just (n,f)) = f * (n + 1)

* For the base case 0!, @g@ is passed @Nothing@. (Note that @'inF' Nothing == 0@.)

* For subsequent cases (/n/+1)!, @g@ is passed /n/ and /n/!.
(Note that @'inF' (Just n) == n + 1@.)

Point-free version: @fact = para $ maybe 1 (uncurry (*) . first (+1))@.

Example: @dropWhile@

> dropWhile :: (a -> Bool) -> [a] -> [a]
> dropWhile p = para f
>   where
>     f Nil         = []
>     f (Pair x xs) = if p x then snd xs else x : fst xs

Point-free version:

> dropWhile p = para $ cons [] (\x xs -> if p x then snd xs else x : fst xs)
-}
para :: Fixpoint f t => (f (t,a) -> a) -> t -> a
para = zygo inF


{-|
Implements course-of-value recursion. At each step, the function
receives an F-branching stream ('Cofree') containing the previous
values. Formally known as a /histomorphism/ and written {| f |}.

@
	histo == 'g_histo' id
@

Example: Computing Fibonacci numbers.

> fibo :: Integer -> Integer
> fibo = histo next
>   where
>     next :: Maybe (Cofree Maybe Integer) -> Integer
>     next Nothing                             = 0
>     next (Just (Consf _ Nothing))            = 1
>     next (Just (Consf m (Just (Consf n _)))) = m + n

* For the base case F(0), @next@ is passed @Nothing@ and returns 0.
(Note that @'inF' Nothing == 0@)

* For F(1), @next@ is passed a one-element stream, and returns 1.

* For subsequent cases F(/n/), @next@ is passed a the stream
[F(/n/-1), F(/n/-2), ..., F(0)] and returns F(/n/-1)+F(/n/-2).

-}

histo :: Fixpoint f t => (f (Cofree f a) -> a) -> t -> a
histo = g_histo id

-----

{-|
A generalization of 'para' implementing \"semi-mutual\" recursion.
Known formally as a /zygomorphism/ and written \<| f |\>^g, where /g/ is an
auxiliary function. Dual to 'g_apo'.

@
	zygo g == 'foldWith' (g . fmap fst &&& fmap snd)
@
-}
zygo :: Fixpoint f t => (f b -> b) -> (f (b,a) -> a) -> t -> a
zygo g f = snd . fold (g . fmap fst &&& f)


{-|
Generalizes 'histo' to cases where the recursion functor and the
stream functor are distinct. Known as a /g-histomorphism/.

@
	g_histo g == 'foldWith' ('anaCofree' (fmap 'headCofree') (g . fmap 'tailCofree'))
@
-}
g_histo :: (Functor h, Fixpoint f t)
       => (forall b. f (h b) -> h (f b))  --  distributive law for /h/ and /f/
       -> (f (Cofree h a) -> a) -> t -> a
g_histo = foldWith . distribCofree


{-|
Generalizes 'fold', 'zygo', and 'g_histo'. Formally known as a /g-catamorphism/
and written (| f |)^(w,k), where /w/ is a 'Comonad' and /k/ is a distributive law between
/n/ and the functor /f/.

The behavior of @foldWith@ is determined by the comonad /w/.

* 'Identity' recovers 'fold'

* @((,) a)@ recovers 'zygo' (and 'para')

* 'Cofree' recovers 'g_histo' (and 'histo')

-}
foldWith :: (Fixpoint f t, Comonad w)
         => (forall b. f (w b) -> w (f b))  --  distributive law for /f/ and /w/
         -> (f (w a) -> a) -> t -> a
foldWith k f = extract . fold (fmap f . k . fmap duplicate)

----

{-| /apomorphisms/, dual to 'para'

@
	apo   == 'g_apo' 'outF'
 	apo f == 'inF' . fmap (id ||| apo f) . f
@

Example: Appending a list to another list

> append :: [a] -> [a] -> [a]
> append = curry (apo f)
>   where
>     f :: ([a],[a]) -> ConsPair a (Either [a] ([a],[a]))
>     f ([], [])   = Nil
>     f ([], y:ys) = Pair y (Left ys)
>     f (x:xs, ys) = Pair x (Right (xs,ys))

-}
apo :: Fixpoint f t => (a -> f (Either t a)) -> a -> t
apo = g_apo outF

{-|
Generalized apomorphisms, dual to 'zygo'

@
	g_apo g == 'unfoldWith' (fmap Left . g ||| fmap Right)
@
-}
g_apo :: Fixpoint f t => (b -> f b) -> (a -> f (Either b a)) -> a -> t
g_apo g f = unfold (fmap Left . g ||| f) . Right


{-|
Generalized anamorphisms parameterized by a monad, dual to 'foldWith'

 * @Identity@ recovers 'unfold'

 * @(Either a)@ recovers 'g_apo' (and 'apo')
-}
unfoldWith :: (Fixpoint f t, Monad m)
           => (forall b. m (f b) -> f (m b)) -> (a -> f (m a)) -> a -> t
unfoldWith k f = unfold (fmap join . k . liftM f) . return


{-|
Generalized hylomorphisms parameterized by both a monad and a comonad.
This one combinator subsumes most-if-not-all the other combinators in
this library.

 * @w = Identity@ yields 'unfoldWith'

 * @m = Identity@ yields 'foldWith'

 * @Free m@ and @Cofree w@ yields 'g_chrono', and therefore 'g_histo' and 'g_futu'

@e@ and @g@ are additional functors related to @f@ by natural transformations
that have been fused into the distributive laws.
-}
refoldWith :: (Comonad w, Functor f, Monad m) =>
              (forall c. f (w c) -> w (g c)) ->
              (forall c. m (e c) -> f (m c)) ->
              (g (w b) -> b) ->
              (a -> e (m a)) ->
              a -> b
refoldWith w m f g = extract . refoldWith' w m f g . return

-- | The kernel of the generalized hylomorphism.
refoldWith' :: (Comonad w, Functor f, Monad m) =>
               (forall c. f (w c) -> w (g c)) ->
               (forall c. m (e c) -> f (m c)) ->
               (g (w b) -> b) ->
               (a -> e (m a)) ->
               (m a -> w b)
refoldWith' w m f g = liftW f . w . fmap (duplicate . refoldWith' w m f g . join) . m . liftM g

{-|
Futumorphism: course of argument coiteration

@
        futu == 'chrono' ('inF' . fmap 'headCofree')
        futu == 'g_futu' id
@

Example, translated from /Primitive (Co)Recursion and Course-of-Value
(Co)Iteration, Categorically/ 
(<http://citeseer.ist.psu.edu/uustalu99primitive.html>):

> phi (x:y:zs) = Pair y . inFree . Pair x $ return zs

> exch = futu phi

> l = exch [1..] -- [2,1,4,3,6,5,8,7,10,9..]
-}
futu :: (Fixpoint f t) => (a -> f (Free f a)) -> a -> t
futu = g_futu id

{-|
Generalized futumorphism

@
        g_futu m == 'g_chrono' (const 'Unit') m ('inF' . fmap 'headCofree')
        g_futu m == 'unfoldWith' ('distribFree' m)
@
-}
g_futu :: (Functor h, Fixpoint f t) =>
          (forall b. h (f b) -> f (h b)) ->
          (a -> f (Free h a)) ->
          a -> t
g_futu = unfoldWith . distribFree

-- | a chronomorphism, coined by Edward Kmett, subsumes both histo
-- and futumorphisms.
chrono :: Functor f =>
          (f (Cofree f b) -> b) ->
          (a -> f (Free f a)) ->
          a -> b
chrono = g_chrono id id

{-|
Generalized chronomorphism. The recursion functor is separated from
the Free and Cofree functors, and related by distributive laws.

@
        g_chrono w m == 'refoldWith' ('distribCofree' w) ('distribFree' m)
@
-}
g_chrono :: (Functor f, Functor m, Functor w) =>
            (forall c. f (w c) -> w (f c)) ->
            (forall c. m (f c) -> f (m c)) ->
            (f (Cofree w b) -> b) ->
            (a -> f (Free m a)) ->
            a -> b
g_chrono w m = refoldWith (distribCofree w) (distribFree m)

{-|
Dynamorphisms: a hylomorphism like combinator that captures dynamic
programming.

@
        dyna f g == 'g_dyna' id (fmap Identity . runIdentity) f (fmap Identity . g)
        dyna f g == 'chrono' f (fmap return . g)
@

Example, translated from /Recursion Schemes for Dynamic Programming/
(<http://citeseer.ist.psu.edu/748315.html>) section 4.2:

> data Poly a = Term | Single a | Double a a

> instance Functor Poly where
>   fmap _ Term = Term
>   fmap f (Single a) = Single (f a)
>   fmap f (Double a b) = Double (f a) (f b)

> psi 0 = Term
> psi n
>   | odd n  = Single (n-1)
>   | even n = Double (n-1) (n `div` 2)

> phi Term = 1
> phi (Single n) = n
> phi (Double m n) = m + n

> bp1 = refold phi psi -- hylo version; ineffcient

> zeta 0 = Nil
> zeta n = Pair n (n-1)

> epsilon = headCofree

> theta = tailCofree

> pie x = let (Pair m y) = theta x in y

> pieN 0 x = x
> pieN n x = pieN (n-1) (pie x)

> sigma Nil = Term
> sigma (Pair n x)
>   | odd n  = Single (epsilon x)
>   | even n = Double (epsilon x) (epsilon (pieN (n`div`2 - 1) x))

> bp2 = dyna (phi . sigma) zeta -- dynamically programmed

-}
dyna :: (Functor f) =>
        (f (Cofree f b) -> b) ->
        (a -> f a) ->
        a -> b
dyna f g = extract . dyna' f g

-- | Kernel of the dynamorphism
dyna' :: (Functor f) =>
         (f (Cofree f b) -> b) ->
         (a -> f a) ->
         a -> Cofree f b
dyna' f g = refold (f &&& id >>> Cofree) g

{-|
Generalized dynamorphism

@
        g_dyna w == 'refoldWith' ('distribCofree' w)
@
-}
g_dyna :: (Functor f, Functor h, Monad m) =>
          (forall c. f (h c) -> h (f c)) ->
          (forall c. m (e c) -> f (m c)) ->
          (f (Cofree h b) -> b) ->
          (a -> e (m a)) ->
          a -> b
g_dyna = refoldWith . distribCofree

{- Generalized dynamorphism kernel
g_dyna' :: (Functor f, Functor h, Monad m) =>
           (forall c. f (h c) -> h (f c)) ->
           (forall c. m (e c) -> f (m c)) ->
           (f (Cofree h b) -> b) ->
           (a -> e (m a)) ->
           m a -> Cofree h b
g_dyna' = refoldWith' . distribCofree
-}

{-|
The dual of dynamorphisms.
-}
codyna :: (Functor f) =>
          (f b -> b) ->
          (a -> f (Free f a)) ->
          a -> b
codyna f g = chrono (f . fmap extract) g

{-|
Generalized codynamorphisms.
-}
g_codyna :: (Functor f, Functor h, Comonad w) =>
            (forall c. f (w c) -> w (g c)) ->
            (forall c. h (f c) -> f (h c)) ->
            (g (w b) -> b) ->
            (a -> f (Free h a)) ->
            a -> b
g_codyna w = refoldWith w . distribFree