-----------------------------------------------------------------------------
-- |
-- Module      :  Generics.Pointless.Functors
-- Copyright   :  (c) 2008 University of Minho
-- License     :  BSD3
--
-- Maintainer  :  hpacheco@di.uminho.pt
-- Stability   :  experimental
-- Portability :  non-portable
--
-- Pointless Haskell:
-- point-free programming with recursion patterns as hylomorphisms
-- 
-- This module defines data types as fixed points of functor.
-- Pointless Haskell works on a view of data types as fixed points of functors, in the same style as the PolyP (<http://www.cse.chalmers.se/~patrikj/poly/polyp/>) library.
-- Instead of using an explicit fixpoint operator, a type function is used to relate the data types with their equivalent functor representations.
--
-----------------------------------------------------------------------------

module Generics.Pointless.Functors where

import Prelude hiding (Functor(..))
import qualified Data.Generics as G
import qualified Data.Typeable as G
import qualified Data.Data as G
import qualified Data.Functor as F
import Generics.Pointless.Combinators

-- * Functors

-- ** Definition and operations over functors

-- | Identity functor.
data Id x = IdF {unIdF :: x} deriving (Eq,Show,G.Typeable)

-- | Constant functor.
data Const t x = ConsF {unConsF :: t} deriving (Eq,Show,G.Typeable)

-- | Sum of functors.
infixr 5 :+:
data (g :+: h) x = InlF (g x) | InrF (h x) deriving (Eq,Show,G.Typeable)

-- | Product of functors.
infixr 6 :*:
data (g :*: h) x = ProdF (g x) (h x) deriving (Eq,Show,G.Typeable)

-- | Composition of functors.
infixr 9 :@:
data (g :@: h) x = CompF {unCompF :: g (h x)} deriving (Eq,Show,G.Typeable)

-- | Explicit fixpoint operator.
newtype Fix f = Inn { -- | The unfolding of the fixpoint of a functor is the functor applied to its fixpoint.
	                   --
	                   -- 'unFix' is specialized with the application of 'Rep' in order to subsume functor application
                         ouT :: Rep f (Fix f)
                    }

instance ShowRep f => Show (Fix f) where
    show f@(Inn r) = "(Fix " ++ showrep (vnn f) showfix r ++ ")"
        where showfix = show :: Fix f -> String

-- | Family of patterns functors of data types.
--
-- The type function is not necessarily injective, this is, different data types can have the same base functor.
type family PF a :: * -> *
-- ^ Semantically, we can say that @a = 'Fix' f@.

type instance PF (Fix f) = f
-- ^ The pattern functor of the fixpoint of a functor is the functor itself.

-- | Family of functor representations.
--
-- The 'Rep' family implements the implicit coercion between the application of a functor and the structurally equivalent sum of products.
type family Rep (f :: * -> *) x :: *
-- ^ Functors applied to types can be represented as sums of products.

type instance Rep Id x = x
-- ^ The identity functor applied to some type is the type itself.

type instance Rep (Const t) x = t
-- ^ The constant functor applied to some type is the type parameterized by the functor.

type instance Rep (g :+: h) x = Rep g x `Either` Rep h x
-- ^ The application of a sum of functors to some type is the sum of applying the functors to the argument type.

type instance Rep (g :*: h) x = (Rep g x,Rep h x)
-- ^ The application of a product of functors to some type is the product of applying the functors to the argument type.

type instance Rep (g :@: h) x = Rep g (Rep h x)
-- ^ The application of a composition of functors to some type is the nested application of the functors to the argument type.
--
-- This particular instance requires that nexted type function application is enabled as a type system extension.

type instance Rep [] x = [x]
-- ^ The application of the list functor to some type returns a list of the argument type.

-- | A specific @Show@ class for functor representations that receives a show function for recursive instances.
-- This avoids infinite loops in the type inference of fixpoints.
class ShowRep f where
    showrep :: Ann (Fix f) -> (x -> String) -> Rep f x -> String
instance ShowRep Id where
    showrep _ f x = f x
instance Show t => ShowRep (Const t) where
    showrep _ _ t = show t
instance (ShowRep f,ShowRep g) => ShowRep (f :*: g) where
    showrep (_ :: Ann (Fix (f :*: g))) f (x,y) = "("++l++","++r++")"
        where l = showrep (ann :: Ann (Fix f)) f x
              r = showrep (ann :: Ann (Fix g)) f y
instance (ShowRep f,ShowRep g) => ShowRep (f :+: g) where
    showrep (_ :: Ann (Fix (f :+: g))) f (Left x) = "(Left "++l++")"
        where l = showrep (ann :: Ann (Fix f)) f x
    showrep (_ :: Ann (Fix (f :+: g))) f (Right y) = "(Right "++r++")"
        where r = showrep (ann :: Ann (Fix g)) f y
instance (ShowRep f,ShowRep g) => ShowRep (f :@: g) where
    showrep (_ :: Ann (Fix (f:@:g))) f x = showrep (ann :: Ann (Fix f)) r x
        where r = showrep (ann :: Ann (Fix g)) f

class ToRep f where
    rep :: f x -> Rep f x
    fun :: f x -> Ann (Fix f)
    val :: f x -> Ann x
    unrep :: Ann (Fix f) -> Ann x -> Rep f x -> f x

instance ToRep [] where
	rep l = l
	fun l = ann
	val l = ann
	unrep _ _ l = l

instance ToRep Id where
    rep (IdF x) = x
    fun _ = ann::Ann (Fix Id)
    val (IdF (x::x)) = ann::Ann x
    unrep _ _ x = IdF x
instance ToRep (Const c) where
    rep (ConsF x) = x
    fun _ = ann::Ann (Fix (Const c))
    val (ConsF _::Const c x) = ann::Ann x
    unrep _ _ x = ConsF x
instance (ToRep f,ToRep g) => ToRep (f :*: g) where
    rep (ProdF x y) = (rep x,rep y)
    fun _ = ann::Ann (Fix (f:*:g))
    val (ProdF (x::f x) (y::g x)) = ann::Ann x
    unrep (_::Ann (Fix (f:*:g))) a (x,y) = ProdF (unrep (ann::Ann (Fix f)) a x) (unrep (ann::Ann (Fix g)) a y)
instance (ToRep f,ToRep g) => ToRep (f :+: g) where
    rep (InlF l) = Left (rep l)
    rep (InrF r) = Right (rep r)
    fun _ = ann::Ann (Fix (f:+:g))
    val (InlF (l::f x)) = ann::Ann x
    val (InrF (r::g x)) = ann::Ann x
    unrep (_::Ann (Fix (f:+:g))) a (Left l) = InlF (unrep (ann::Ann (Fix f)) a l)
    unrep (_::Ann (Fix (f:+:g))) a (Right r) = InrF (unrep (ann::Ann (Fix g)) a r)
instance (Functor f,F.Functor f,ToRep f,ToRep g) => ToRep (f :@: g) where
    rep (CompF x) = rep $ F.fmap rep x
    fun _ = ann::Ann (Fix (f:@:g))
    val (CompF x::(f:@:g) x) = ann::Ann x
    unrep (_::Ann (Fix (f:@:g))) a x = CompF $ (unrep (ann::Ann (Fix f)) (ann::Ann (g a))) $ fmap (ann::Ann (Fix f)) (unrep (ann::Ann (Fix g)) a) x

-- | Polytypic 'Prelude.Functor' class for functor representations
class Functor (f :: * -> *) where
   fmap :: Ann (Fix f)                          -- ^ For desambiguation purposes, the type of the functor must be passed as an explicit parameter to 'fmap'
        -> (x -> y) -> Rep f x -> Rep f y -- ^ The mapping over representations
   fzip :: Ann (Fix f) -> (a -> c) -> (Rep f a,Rep f c) -> Rep f (a,c)      -- ^ The polytypic functor zipping combinator.
        -- Gives preference to the abstract (first) F-structure.

instance F.Functor Id where
   fmap f (IdF x) = IdF $ f x
instance Functor Id where
   fmap _ f = f
   fzip _ create = id
-- ^ The identity functor applies the mapping function the argument type

instance F.Functor (Const t) where
   fmap f (ConsF x) = ConsF x
instance Functor (Const t) where
   fmap _ f = id
   fzip _ create = fst
-- ^ The constant functor preserves the argument type

instance (F.Functor g,F.Functor h) => F.Functor (g :+: h) where
   fmap f (InlF x) = InlF (F.fmap f x)
   fmap f (InrF x) = InrF (F.fmap f x)
instance (Functor g,Functor h) => Functor (g :+: h) where
   fmap (_::Ann (Fix (g:+:h))) f (Left x) = Left (fmap (ann :: Ann (Fix g)) f x)
   fmap (_::Ann (Fix (g:+:h))) f (Right x) = Right (fmap (ann :: Ann (Fix h)) f x)
   fzip (_::Ann (Fix (g:+:h))) create = (l -|- r) . dists
    where l = fzip (ann::Ann (Fix g)) create \/ fmap (ann::Ann (Fix g)) (id /\ create) . fst
          r = fmap (ann::Ann (Fix h)) (id /\ create) . fst \/ fzip (ann::Ann (Fix h)) create
-- ^ The sum functor recursively applies the mapping function to each alternative

instance (F.Functor g,F.Functor h) => F.Functor (g :*: h) where
   fmap f (ProdF x y) = ProdF (F.fmap f x) (F.fmap f y)
instance (Functor g,Functor h) => Functor (g :*: h) where
   fmap (_::Ann (Fix (g:*:h))) f (x,y) = (fmap (ann :: Ann (Fix g)) f x,fmap (ann :: Ann (Fix h)) f y)
   fzip (_::Ann (Fix (g:*:h))) create = (fzip (ann::Ann (Fix g)) create >< fzip (ann::Ann (Fix h)) create) . distp
-- ^ The product functor recursively applies the mapping function to both sides

instance (F.Functor g,F.Functor h) => F.Functor (g :@: h) where
   fmap f (CompF x) = CompF $ F.fmap (F.fmap f) x
instance (Functor g,Functor h) => Functor (g :@: h) where
   fmap (_::Ann (Fix (g:@:h))) f x = fmap (ann :: Ann (Fix g)) (fmap (ann :: Ann (Fix h)) f) x
   fzip (_::Ann (Fix (g:@:h))) create = fmap g (fzip h create) . fzip g (fmap h create)
    where g = ann::Ann (Fix g)
          h = ann::Ann (Fix h)
-- ^ The composition functor applies in the nesting of the mapping function to the nested functor applications

instance Functor [] where
   fmap _ = map
   fzip _ create = lzip create
-- ^ The list functor maps the specific 'map' function over lists of types

lzip :: (a -> c) -> ([a],[c]) -> [(a,c)]
lzip create ([],lc) = []
lzip create (a:la,[]) = (a,create a) : lzip create (la,[])
lzip create (a:la,c:lc) = (a,c) : lzip create (la,lc)

-- | Short alias to express the structurally equivalent sum of products for some data type
type F a x = Rep (PF a) x

-- | Polytypic map function
pmap :: Functor (PF a) => Ann a                          -- ^ A value of a data type that is the fixed point of the desired functor
                       -> (x -> y) -> F a x -> F a y -- ^ The mapping over the equivalent sum of products
pmap (_::Ann a) f = fmap (ann:: Ann (Fix (PF a))) f

-- | The 'Mu' class provides the value-level translation between data types and their sum of products representations
class Mu a where
    -- | Packs a sum of products into one equivalent data type
    inn :: F a a -> a
    -- | unpacks a data type into the equivalent sum of products
    out :: a -> F a a

inn' :: Mu a => Ann a -> F a a -> a
inn' _ = inn

out' :: Mu a => Ann a -> a -> F a a
out' _ = out

instance Mu (Fix f) where
   inn = Inn
   out = ouT
-- ^ Expanding/contracting the fixed point of a functor is the same as consuming/applying it's single type constructor

-- ** Fixpoint combinators

-- | In order to simplify type-level composition of functors, we can create fixpoint combinators that implicitely assume fixpoint application.

data I = FixId
-- ^ Semantically, we can say that @'I' = 'Fix' 'Id'@.
type instance PF I = Id

instance Mu I where
   inn = id
   out = id

data K a = FixConst {unFixConst :: a}
-- ^ Semantically, we can say that @'K' t = 'Fix' ('Const' t)@.
type instance PF (K a) = Const a

instance Mu (K a) where
   inn = FixConst
   out = unFixConst

infixr 5 :+!:
data (a :+!: b) = FixSum {unFixSum :: F (a :+!: b) (a :+!: b)}
-- ^ Semantically, we can say that @'Fix' f :+!: 'Fix' g = 'Fix' (f :+: g)@.
type instance PF (a :+!: b) = PF a :+: PF b

instance Mu (a :+!: b) where
   inn = FixSum
   out = unFixSum

infixr 6 :*!:
data (a :*!: b) = FixProd {unFixProd :: F (a :*!: b) (a :*!: b)}
-- ^ Semantically, we can say that @'Fix' f :*!: 'Fix' g = 'Fix' (f :*: g)@.
type instance PF (a :*!: b) = PF a :*: PF b

instance Mu (a :*!: b) where
   inn = FixProd
   out = unFixProd

infixr 9 :@!:
data (a :@!: b) = FixComp {unFixComp :: F (a :@!: b) (a :@!: b)}
-- ^ Semantically, we can say that @'Fix' f :\@!: 'Fix' g = 'Fix' (f ':\@: g)@.
type instance PF (a :@!: b) = PF a :@: PF b

instance Mu (a :@!: b) where
   inn = FixComp
   out = unFixComp

-- * Default definitions for commonly used data types

-- ** List

type instance PF [a] = Const One :+: Const a :*: Id

instance Mu [a] where
    inn (Left _) = []
    inn (Right (x,xs)) = x:xs
    out [] = Left _L
    out (x:xs) = Right (x,xs)

nil :: One -> [a]
nil = inn . inl

cons :: (a,[a]) -> [a]
cons = inn . inr

-- ** Natural Numbers

-- Implemented as "boxed" integers for efficiency
data Nat = Nat Int deriving (Eq,Show,Read,G.Typeable,G.Data)

type instance PF Nat = Const One :+: Id

instance Mu Nat where
    inn (Left _) = Nat 0
    inn (Right (Nat n)) = Nat (succ n)
    out (Nat 0) = Left _L
    out (Nat n) = if n < 1 then error "negative natural not expected" else Right (Nat $ pred n)

nzero = Nat 0
nsucc (Nat n) = Nat (succ n)

-- ** Int (positive only)

type instance PF Int = Const One :+: Id

instance (Mu Int) where
    inn (Left _) = 0
    inn (Right n) = succ n
    out 0 = Left _L
    out n = Right (pred n)

zero :: One -> Int
zero = inn . inl

suck :: Int -> Int
suck = inn . inr

natInt :: Nat -> Int
natInt (Nat n) = n

intNat :: Int -> Nat
intNat n = if n < 0 then error "negative natural not expected" else Nat n

-- ** Bool

type instance PF Bool = Const One :+: Const One

instance Mu Bool where
	inn (Left _) = True
	inn (Right _) = False
	out True = Left _L
	out False = Right _L

true :: One -> Bool
true = inn . inl

false :: One -> Bool
false = inn . inr

-- ** Maybe

type instance PF (Maybe a) = Const One :+: Const a

instance Mu (Maybe a) where
    inn (Left _) = Nothing
    inn (Right x) = Just x
    out Nothing = Left _L
    out (Just x) = Right x

maybe2bool :: Maybe a -> Bool
maybe2bool = inn . (id -|- bang) . out