{-# 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)