{-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-}

module PFRecPat where

-- Functors

data (g :+: h) x = Inl (g x) | Inr (h x)
data (g :*: h) x = g x :*: h x
data (g :@: h) x = Comp {unComp :: g (h x)}
data Unit x = Unit
newtype Rec x = Rec {unRec :: x}
newtype Const t x = Const {unConst :: t}

instance Functor Unit
    where fmap f Unit = Unit

instance Functor Rec
    where fmap f (Rec x) = Rec (f x)

instance Functor (Const t)
    where fmap f (Const x) = Const x

instance (Functor g, Functor h) => Functor (g :+: h)
    where fmap f (Inl x) = Inl (fmap f x)
	  fmap f (Inr x) = Inr (fmap f x)

instance (Functor g, Functor h) => Functor (g :*: h)
    where fmap f (x :*: y) = (fmap f x) :*: (fmap f y)

instance (Functor g, Functor h) => Functor (g :@: h)
    where fmap f (Comp x) = Comp (fmap (fmap f) x)

-- From functors to sums of products

class Iso a b | a -> b
    where to :: a -> b
	  from :: b -> a

instance Iso (Unit x) ()
    where to Unit = ()
	  from () = Unit

instance Iso (Rec x) x
    where to (Rec x) = x
	  from x = Rec x

instance Iso (Const t x) t
    where to (Const t) = t
	  from t = Const t

instance (Iso (g x) y, Iso (h x) z) => Iso ((g :+: h) x) (Either y z)
    where to (Inl a) = Left (to a)
	  to (Inr a) = Right (to a)
	  from (Left a) = Inl (from a)
	  from (Right a) = Inr (from a)

instance (Iso (g x) y, Iso (h x) z) => Iso ((g :*: h) x) (y, z)
    where to (a :*: b) = (to a, to b)
	  from (a, b) = from a :*: from b

instance (Functor g, Iso (h x) y, Iso (g y) z) => Iso ((g :@: h) x) z
    where to (Comp x) = to (fmap to x) 
	  from y = Comp (fmap from (from y))

-- We also need the (obvious) representation of type functors

instance Iso [x] [x]
    where to = id
	  from = id

-- Data types as fixed points of functors PolyP style

class (Functor f) => FunctorOf f d | d -> f
    where inn' :: f d -> d
	  out' :: d -> f d

-- Bridge to data types as explicit fixed points of functors

newtype Mu f = Mu {unMu :: f (Mu f)}

instance (Functor f) => FunctorOf f (Mu f)
    where inn' = Mu
	  out' = unMu

-- Point free programming primitives

infix 5  ><
infix 4  -|-
infix 6 /\
infix 7 \/
infix 9 !

(\/) = either

(-|-) :: (a -> b) -> (c -> d) -> Either a c -> Either b d
f -|- g = (Left . f) \/ (Right . g)

split :: (a -> b) -> (a -> c) -> a -> (b,c)
split f g x = (f x, g x)

(/\) = split

(><) :: (a -> b) -> (c -> d) -> (a,c) -> (b,d)
f >< g = (f . fst) /\ (g . snd)

app :: (a -> b, a) -> b
app = uncurry ($)

fexp :: (a -> b) -> (c -> a) -> (c -> b)
fexp f = curry (f . app)

grd :: (a -> Bool) -> a -> Either a a
grd p x = if p x then Left x else Right x

(!) :: a -> b -> a
a ! b = a

-- Isomorphisms

swap :: (a,b) -> (b,a)
swap = snd /\ fst

distl :: (Either a b, c) -> Either (a,c) (b,c)
distl (Left  x, y) = Left  (x,y)
distl (Right x, y) = Right (x,y)

distr :: (c, Either a b) -> Either (c,a) (c,b)
distr (y, Left  x) = Left  (y,x)
distr (y, Right x) = Right (y,x)

assocl :: (a,(b,c)) -> ((a,b),c)
assocl = (id >< fst) /\ (snd . snd)

assocr :: ((a,b),c) -> (a,(b,c))
assocr = (fst . fst) /\ (snd >< id)

coassocl :: Either a (Either b c) -> Either (Either a b) c
coassocl = (Left . Left) \/ (Right -|- id)

coassocr :: Either (Either a b) c -> Either a (Either b c)
coassocr = (id -|- Left) \/ (Right . Right)

-- Auxiliary definitions

comp :: (b -> c, a -> b) -> (a -> c)
comp = curry (app . (id >< app) . assocr)

-- Helper functions to deal with isomorphisms

bot :: a
bot = undefined

out :: (FunctorOf f d, Iso (f d) a) => d -> a
out = to . out'

inn :: (FunctorOf f d, Iso (f d) a) => a -> d
inn = inn' . from

mapp :: (FunctorOf f d, Iso (f a) c, Iso (f b) e) => d -> (a -> b) -> (c -> e)
mapp (x::d) f = to . (fmap:: (FunctorOf f d) => (a -> b) -> (f a -> f b)) f . from

-- Recursion partterns

hylo (_::d) g h = g . mapp (bot::d) (hylo (bot::d) g h) . h

cata (_::d) f (x::d) = hylo (bot::d) f out x

ana (_::d) f x = (hylo (bot::d) inn f x)::d

para (_::d) f (x::d) = hylo (bot :: FunctorOf f d => Mu (f :@: (Rec :*: Const d))) f (mapp (bot::d) (id /\ id) . out) x

apo (_::d) f x = (hylo (bot :: FunctorOf f d => Mu (f :@: (Rec :+: Const d))) (inn . mapp (bot::d) (id \/ id)) f x)::d

afold (_::d) t f (x::d, y::a) = hylo (bot :: FunctorOf f d => Mu (f :*: (Const a))) f ((t /\ snd) . (out >< id)) (x,y)