{-# LANGUAGE DataKinds              #-}
{-# LANGUAGE PolyKinds              #-}
{-# LANGUAGE TypeFamilies           #-}
{-# LANGUAGE TypeInType             #-}
{-# LANGUAGE TypeOperators          #-}
{-# LANGUAGE UndecidableInstances   #-}
{-# OPTIONS_GHC -Wall                       #-}
{-# OPTIONS_GHC -Werror=incomplete-patterns #-}

{-|
Module      : Fcf.Alg.Morphism
Description : Algebra, ColAlgebra, and other stuff
Copyright   : (c) gspia 2020-
License     : BSD
Maintainer  : gspia

= Fcf.Alg.Morphism

Type-level 'Cata' and 'Ana' can be used to do complex computation that live only
on type-level or on compile-time. As an example, see the sorting algorithm
in Fcf.Alg.Tree -module.

This module also provides some other type-level functions that probably will
find other place after a while. E.g. 'First' and 'Second' and their instances
on Either and tuple.

-}

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

module Fcf.Alg.Morphism where

import           Fcf

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

-- For the doctests:

-- $setup
-- >>> import qualified GHC.TypeLits as TL
-- >>> import           Fcf.Alg.List
-- >>> import           Fcf.Data.Nat

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

-- | Structure that 'Cata' can fold and that is a result structure of 'Ana'.
data Fix f = Fix (f (Fix f))

-- | Commonly used name describing the method 'Cata' eats.
type Algebra f a = f a -> Exp a

-- | Commonly used name describing the method 'Ana' eats.
type CoAlgebra f a = a -> Exp (f a)

-- | Commonly used name describing the method 'Para' eats.
type RAlgebra f a = f (Fix f, a) -> Exp a

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


-- | Write the function to give a 'Fix', and feed it in together with an
-- 'Algebra'.
-- 
-- Check Fcf.Alg.List to see example algebras in use. There we have e.g.
-- ListToFix-function.
data Cata :: Algebra f a -> Fix f -> Exp a
type instance Eval (Cata alg ('Fix b)) = alg @@ (Eval (Map (Cata alg) b))

-- | Ana can also be used to build a 'Fix' structure.
--
-- === __Example__
-- 
-- >>> data NToOneCoA :: CoAlgebra (ListF Nat) Nat
-- >>> :{ 
--   type instance Eval (NToOneCoA b) = 
--     If (Eval (b < 1) )
--         'NilF
--         ('ConsF b ( b TL.- 1))
-- :}
-- 
-- >>> :kind! Eval (Ana NToOneCoA 3)
-- Eval (Ana NToOneCoA 3) :: Fix (ListF Nat)
-- = 'Fix ('ConsF 3 ('Fix ('ConsF 2 ('Fix ('ConsF 1 ('Fix 'NilF))))))
data Ana :: CoAlgebra f a -> a -> Exp (Fix f)
type instance Eval (Ana coalg a) = 'Fix (Eval (Map (Ana coalg) (Eval (coalg a))))


-- | 
-- Hylomorphism uses first 'Ana' to build a structure (unfold) and then 'Cata'
-- to process the structure (fold).
-- 
-- === __Example__
-- 
-- >>> data NToOneCoA :: CoAlgebra (ListF Nat) Nat
-- >>> :{ 
--   type instance Eval (NToOneCoA b) = 
--     If (Eval (b < 1) )
--         'NilF
--         ('ConsF b ( b TL.- 1))
-- :}
-- 
-- >>> :kind! Eval (Hylo SumAlg NToOneCoA 5)
-- Eval (Hylo SumAlg NToOneCoA 5) :: Nat
-- = 15
data Hylo :: Algebra f a -> CoAlgebra f b -> b -> Exp a
type instance Eval (Hylo alg coalg a) = Eval (Cata alg =<< Ana coalg a)


-- Helper for Para so that we can do fmap
data Fanout :: RAlgebra f a -> Fix f -> Exp ( Fix f, a)
type instance Eval (Fanout ralg ('Fix f)) = '( 'Fix f, Eval (Para ralg ('Fix f)))


-- | Write a function to give a 'Fix', and feed it in together with an
-- 'RAlgebra'
--
-- Check Fcf.Alg.List to see example algebras in use. There we have e.g.
-- ListToParaFix-function.
data Para :: RAlgebra f a -> Fix f -> Exp a
type instance Eval (Para ralg ('Fix  a)) =  ralg @@ (Eval (Map (Fanout ralg) a))

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

-- | Annotate (f r) with attribute a
-- (from Recursion Schemes by example, Tim Williams).
newtype AnnF f a r = AnnF (f r, a)

-- | Annotated fixed-point type. A cofree comonad
-- (from Recursion Schemes by example, Tim Williams).
type Ann f a = Fix (AnnF f a)

-- | Attribute of the root node
-- (from Recursion Schemes by example, Tim Williams).
data Attr :: Ann f a -> Exp a
type instance Eval (Attr ('Fix ( 'AnnF '(_, a)))) = a

-- | Strip attribute from root
-- (from Recursion Schemes by example, Tim Williams).
data Strip :: Ann f a -> Exp (f (Ann f a))
type instance Eval (Strip ('Fix ( 'AnnF '(x,_)))) = x

-- | Annotation constructor
-- (from Recursion Schemes by example, Tim Williams).
data AnnConstr :: (f (Ann f a), a) -> Exp (Fix (AnnF f a))
type instance Eval (AnnConstr fxp) = Eval (Pure ('Fix ('AnnF fxp)))

-- | Synthesized attributes are created in a bottom-up traversal
-- using a catamorphism
-- (from Recursion Schemes by example, Tim Williams).
-- 
-- This is the algebra that is fed to the cata.
data SynthAlg :: (f a -> Exp a) -> f (Ann f a) -> Exp (Ann f a)
type instance Eval (SynthAlg alg faf) =
    Eval (AnnConstr '(faf, Eval (alg  =<< Map Attr faf)))

-- | Synthesized attributes are created in a bottom-up traversal
-- using a catamorphism
-- (from Recursion Schemes by example, Tim Williams).
-- 
-- For the example, see "Fcf.Data.Alg.Tree.Sizes".
data Synthesize :: (f a -> Exp a) -> Fix f -> Exp (Ann f a)
type instance Eval (Synthesize f fx) = Eval (Cata (SynthAlg f) fx)

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

-- | Histo takes annotation algebra and takes a Fix-structure
-- (from Recursion Schemes by example, Tim Williams).
-- 
-- This is a helper for 'Histo' as it is implemented with 'Cata'.
data HistoAlg :: (f (Ann f a) -> Exp a) -> f (Ann f a) -> Exp (Ann f a)
type instance Eval (HistoAlg alg faf) =
    Eval (AnnConstr '(faf, Eval (alg faf)))

-- | Histo takes annotation algebra and takes a Fix-structure
-- (from Recursion Schemes by example, Tim Williams).
-- 
-- Examples can be found from "Fcf.Data.Alg.Tree" and "Fcf.Data.Alg.List"
-- modules.
data Histo :: (f (Ann f a) -> Exp a) -> Fix f -> Exp a
type instance Eval (Histo alg fx) = Eval (Attr =<< Cata (HistoAlg alg) fx)

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

-- | Type-level First. Tuples @(,)@ and @Either@ have First-instances.
-- 
-- === __Example__
-- 
-- >>> :kind! Eval (First ((+) 1) '(3,"a"))
-- Eval (First ((+) 1) '(3,"a")) :: (Nat, TL.Symbol)
-- = '(4, "a")
data First :: (a -> Exp b) -> f a c -> Exp (f b c)

-- (,)
type instance Eval (First f '(a,b)) = '(f @@ a, b)

-- Either
type instance Eval (First f ('Left a)) = 'Left (f @@ a)
type instance Eval (First f ('Right b)) = 'Right b

-- | Type-level Second. Tuples @(,)@ and @Either@ have Second-instances.
-- 
-- === __Example__
-- 
-- >>> :kind! Eval (Second ((+) 1) '("a",3))
-- Eval (Second ((+) 1) '("a",3)) :: (TL.Symbol, Nat)
-- = '("a", 4)
data Second :: (c -> Exp d) -> f a c -> Exp (f a d)

-- (,)
type instance Eval (Second f '(a,b)) = '(a, f @@ b)

-- Either
type instance Eval (Second f ('Left a)) = 'Left a
type instance Eval (Second f ('Right b)) = 'Right (f @@ b)