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

-----------------------------------------------------------------------------
-- |
-- Module      :  Control.Recursion
-- Copyright   :  2004 Dave Menendez
-- License     :  public domain
-- 
-- 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').
--
-----------------------------------------------------------------------------

module Control.Recursion
  (
  -- * Folding
    fold
  , para
  , zygo
  , histo
  , g_histo
  , foldWith
  
  -- * Unfolding
  , unfold
  , apo
  , g_apo
  , unfoldWith

  -- * Transforming
  , refold
  
  -- * Functor fixpoints
  , Fixpoint(..)
  , Fix(..)
  , ConsPair(..)
  , cons
  
  ) where

----
import Control.Arrow
import Control.Functor
import Control.Monad
import Control.Comonad
import Data.BranchingStream

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' ('Id' . fmap 'unId') (f . fmap 'unId')
@
-}
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 'Id' . 'unId') (fmap 'Id' . 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 ('Strf') 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 (Strf 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 (Strf 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' ('genStrf' (fmap 'hdf') (g . fmap 'tlf'))
@
-}
g_histo :: (Functor h, Fixpoint f t)
       => (forall b. f (h b) -> h (f b))  --  distributive law for /h/ and /f/
       -> (f (Strf h a) -> a) -> t -> a
g_histo g = foldWith (genStrf (fmap hdf) (g . fmap tlf))


{-|
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/.

* 'Id' recovers 'fold'

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

* 'Strf' 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'

* 'Id' 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

----

-- defined for internal use
{-
infixr 2 &&&, |||
f &&& g = \x -> (f x, g x)
(|||) = either
-}