{- Recursion Schemes:
   - Ana, Cata, Futu, Histo;
   - Inductive and Coinductive types.
   Copyright (c) Groupoid Infinity, 2014-2018. -}

module recursion where

{- Here is model of F-algebras with their recursors cana and ana.
   This is fixpoint version of recursion schemes which is defined
   in control module along with functor definition. -}

import control

-- Fixpoint Equations:
--      A B : U , F : U -> U
--       mu (F) = A + F(B)
--      fix (F) = F(fix(F))
--       nu (F) = A * F(B)

-- Fixpoint Functor
data fix    (F:U->U) = Fix (point: F (fix F))
out_        (F:U->U) : fix F -> F (fix F) = split Fix f -> f
in_         (F:U->U) : F (fix F) -> fix F = \(x: F (fix F)) -> Fix x

-- Mu and Nu Functors
data mu     (F:U->U) (A B:U) = Return (a: A) | Bind (f: F B)
data nu     (F:U->U) (A B:U) = CoBind (a: A)        (f: F B)

-- Free and CoFree Functors
data free   (F:U->U) (A:U)   = Free    (_: fix (mu F A))
data cofree (F:U->U) (A:U)   = CoFree  (_: fix (nu F A))
unfree      (F:U->U) (A:U):  free   F A -> fix (mu F A) = split Free   a -> a
uncofree    (F:U->U) (A:U):  cofree F A -> fix (nu F A) = split CoFree a -> a

cata (A: U) (F: functor) (alg: F.1 A -> A) (f: fix F.1): A
   = alg (F.2 (fix F.1) A (cata A F alg) (out_ F.1 f))

ana  (A: U) (F: functor) (coalg: A -> F.1 A) (a: A): fix F.1
   = Fix (F.2 A (fix F.1) (ana A F coalg) (coalg a))

para (A: U) (F: functor) (alg: F.1 (tuple (fix F.1) A)->A) (f: fix F.1): A
   = alg (F.2 (fix F.1) (tuple (fix F.1) A)
              (\(m: fix F.1) -> pair m (para A F alg m)) (out_ F.1 f))

hylo (A B: U) (F: functor) (alg: F.1 B -> B) (coalg: A-> F.1 A) (a: A): B
   = alg (F.2 A B (hylo A B F alg coalg) (coalg a))

zygo (A B: U) (F: functor) (g: F.1 A -> A)
     (alg: F.1 (tuple A B) -> B) (f: fix F.1): B
  = snd A B (cata (tuple A B) F
        (\(x: F.1 (tuple A B)) -> pair (g (F.2 (tuple A B) A
             (\(y: tuple A B) -> fst A B y) x)) (alg x)) f)

prepro (A: U) (F: functor) (nt: F.1(fix F.1) -> F.1(fix F.1))
       (alg: F.1 A -> A) (f: fix F.1): A
  = alg (F.2 (fix F.1) A (\(x: fix F.1) ->
        prepro A F nt alg (cata (fix F.1) F (\(y: F.1(fix F.1))
    -> Fix (nt y)) x)) (out_ F.1 f))

postpro (A: U) (F: functor) (nt : F.1(fix F.1) -> F.1(fix F.1))
        (coalg: A -> F.1 A) (a: A): fix F.1
  = Fix (F.2 A (fix F.1) (\(x: A) -> ana (fix F.1) F (\(y: fix F.1)
    -> nt (out_ F.1 y)) (postpro A F nt coalg x)) (coalg a))

apo (A: U) (F: functor)
    (coalg: A -> F.1 (either (fix F.1) A)) (a: A): fix F.1
  = Fix (F.2 (either (fix F.1) A) (fix F.1) (\(x: either (fix F.1) A)
    -> eitherRec (fix F.1) A (fix F.1) (idfun (fix F.1)) (apo A F coalg) x) (coalg a))

gapo (A B: U) (F: functor)
     (coalg: A -> F.1 A) (coalg2: B -> F.1(either A B)) (b: B): fix F.1
  = Fix ((F.2 (either A B) (fix F.1) (\(x: either A B)
    -> eitherRec A B (fix F.1) (\(y: A) -> ana A F coalg y) (\(z: B)
    -> gapo A B F coalg coalg2 z) x) (coalg2 b)))

futu (A: U) (F: functor)
     (f: A -> F.1 (free F.1 A)) (a: A): fix F.1
  = Fix (F.2 (free F.1 A) (fix F.1) (\(z: free F.1 A) -> w z) (f a)) where
  w: free F.1 A -> fix F.1 = split
    Free x -> unpack_fix x where
  unpack_free: mu F.1 A (fix (mu F.1 A)) -> fix F.1 = split
    Return x -> futu A F f x
    Bind g -> Fix (F.2 (fix (mu F.1 A)) (fix F.1)
                        (\(x: fix (mu F.1 A)) -> w (Free x)) g)
  unpack_fix: fix (mu F.1 A) -> fix F.1 = split
    Fix x -> unpack_free x

histo (A:U) (F: functor)
      (f: F.1 (cofree F.1 A) -> A) (z: fix F.1): A
  = extract A ((cata (cofree F.1 A) F (\(x: F.1 (cofree F.1 A)) ->
    CoFree (Fix (CoBind (f x) ((F.2 (cofree F.1 A)
    (fix (nu F.1 A)) (uncofree F.1 A) x)))))) z) where
  extract (A: U): cofree F.1 A -> A = split
    CoFree f -> unpack_fix f where
  unpack_fix: fix (nu F.1 A) -> A = split
    Fix f -> unpack_cofree f where
  unpack_cofree: nu F.1 A (fix (nu F.1 A)) -> A = split
    CoBind a -> a

chrono (A B: U) (F: functor)
       (f: F.1 (cofree F.1 B) -> B)
       (g: A -> F.1 (free F.1 A))
       (a: A): B = histo B F f (futu A F g a)

-- Mendler's cata
mcata (T: U) (F: U -> U)
      (phi: ((fix F) -> T) -> F (fix F) -> T) (t: fix F): T
    = phi (\(x: fix F) -> mcata T F phi x) (out_ F t)

meta  (A B: U) (F: functor)
      (f: A -> F.1 A) (e: B -> A)
      (g: F.1 B -> B) (t: fix F.1): fix F.1
    = ana A F f (e (cata B F g t))

mutu (A B: U) (F: functor)
     (f: F.1 (tuple A B) -> B)
     (g: F.1 (tuple B A) -> A)
     (t: fix F.1): A
   = g (F.2 (fix F.1) (tuple B A) (\(x: fix F.1) ->
     pair (mutu B A F g f x) (mutu A B F f g x)) (out_ F.1 t))

-- model of inductive types as F-algebras squares
ind   (F: U -> U) (A: U): U
    = (i: F (fix F) -> fix F)
    * (o: fix F -> F (fix F))
    * (fold_: (F A -> A) -> fix F -> A)
    * ((F (cofree F A) -> A) -> fix F -> A)

coind (F: U -> U) (A: U): U
    = (o: fix F -> F (fix F))
    * (i: F (fix F) -> fix F)
    * (unfold_: (A -> F A) -> A -> fix F)
    * ((A -> F (free F A)) -> A -> fix F)

inductive   (F: functor) (A: U): ind F.1 A = (in_ F.1,out_ F.1,cata A F,histo A F)
coinductive (F: functor) (A: U): coind F.1 A = (out_ F.1,in_ F.1,ana A F,futu A F)

data W (A:U) (B:A->U) = sup (x:A) (f:B(x) -> W A B)

whead (A:U)(B:A->U): W A B -> A                            = split sup x f -> x
wtail (A:U)(B:A->U): (x:W A B) -> B (whead A B x) -> W A B = split sup x f -> f

Wrec (A:U) (B:A->U) (P: U)
     (alg: (a:A) -> (B(a)->W A B) -> ((b:B(a)) -> P) -> P)
   : W A B -> P = split sup x g -> alg x g (\(h:B(x)) -> Wrec A B P alg (g h))

Wind (A:U) (B:A->U) (P:W A B -> U)
     (alg: (a:A) (f:B(a)->W A B) -> ((b:B(a))->P (f b)) -> P (sup a f))
   : (w: W A B) -> P w = split sup x g -> alg x g (\(b:B(x)) -> Wind A B P alg (g b))