-----------------------------------------------------------------------------
-- |
-- 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 Generics.Pointless.Combinators
import Prelude hiding (Functor(..))

-- * Functors

-- ** Definition and operations over functors

-- | Identity functor.
newtype Id x = Id {unId :: x}

-- | Constant functor.
newtype Const t x = Const {unConst :: t}

-- | Sum of functors.
infixr 5 :+:
data (g :+: h) x = Inl (g x) | Inr (h x)

-- | Product of functors.
infixr 6 :*:
data (g :*: h) x = g x :*: h x

-- | Composition of functors.
infixr 9 :@:
newtype (g :@: h) x = Comp {unComp :: g (h x)}

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

instance Show (Rep f (Fix f)) => Show (Fix f) where
   show (Fix f) = "(Fix " ++ show f ++ ")"

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

-- | Polytypic 'Prelude.Functor' class for functor representations
class Functor (f :: * -> *) where
   fmap :: Fix f                          -- ^ For desambiguation purposes, the type of the functor must be passed as an explicit paramaeter to 'fmap'
        -> (x -> y) -> Rep f x -> Rep f y -- ^ The mapping over representations

instance Functor Id where
   fmap _ f = f
-- ^ The identity functor applies the mapping function the argument type

instance Functor (Const t) where
   fmap _ f = id
-- ^ The constant functor preserves the argument type

instance (Functor g,Functor h) => Functor (g :+: h) where
   fmap _ f (Left x) = Left (fmap (_L :: Fix g) f x)
   fmap _ f (Right x) = Right (fmap (_L :: Fix h) f x)
-- ^ The sum functor recursively applies the mapping function to each alternative

instance (Functor g,Functor h) => Functor (g :*: h) where
   fmap _ f (x,y) = (fmap (_L :: Fix g) f x,fmap (_L :: Fix h) f y)
-- ^ The product functor recursively applies the mapping function to both sides

instance (Functor g,Functor h) => Functor (g :@: h) where
   fmap _ f x = fmap (_L :: Fix g) (fmap (_L :: Fix h) f) x
-- ^ The composition functor applies in the nesting of the mapping function to the nested functor applications

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

-- | 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) => 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 (_::a) f = fmap (_L :: 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

instance Mu (Fix f) where
   inn = Fix
   out = unFix
-- ^ 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

-- ** Int

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

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