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
data Id x = IdF {unIdF :: x} deriving (Eq,Show,G.Typeable)
data Const t x = ConsF {unConsF :: t} deriving (Eq,Show,G.Typeable)
infixr 5 :+:
data (g :+: h) x = InlF (g x) | InrF (h x) deriving (Eq,Show)
instance (G.Typeable (g x),G.Typeable (h x)) => G.Typeable ((g :+: h) x) where
typeOf _ = G.mkTyCon ":+:" `G.mkTyConApp` [G.typeOf (ann::g x),G.typeOf (ann::h x)]
infixr 6 :*:
data (g :*: h) x = ProdF (g x) (h x) deriving (Eq,Show)
instance (G.Typeable (g x),G.Typeable (h x)) => G.Typeable ((g :*: h) x) where
typeOf _ = G.mkTyCon ":*:" `G.mkTyConApp` [G.typeOf (ann::g x),G.typeOf (ann::h x)]
infixr 9 :@:
data (g :@: h) x = CompF {unCompF :: g (h x)} deriving (Eq,Show)
instance (G.Typeable (g x),G.Typeable (h x)) => G.Typeable ((g :@: h) x) where
typeOf _ = G.mkTyCon ":@:" `G.mkTyConApp` [G.typeOf (ann::g x),G.typeOf (ann::h x)]
newtype Fix f = Inn {
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
type family PF a :: * -> *
type instance PF (Fix f) = f
type family Rep (f :: * -> *) x :: *
type instance Rep Id x = x
type instance Rep (Const t) x = t
type instance Rep (g :+: h) x = Rep g x `Either` Rep h x
type instance Rep (g :*: h) x = (Rep g x,Rep h x)
type instance Rep (g :@: h) x = Rep g (Rep h x)
type instance Rep [] x = [x]
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
class Functor (f :: * -> *) where
fmap :: Ann (Fix f)
-> (x -> y) -> Rep f x -> Rep f y
fzip :: Ann (Fix f) -> (a -> c) -> (Rep f a,Rep f c) -> Rep f (a,c)
instance F.Functor Id where
fmap f (IdF x) = IdF $ f x
instance Functor Id where
fmap _ f = f
fzip _ create = id
instance F.Functor (Const t) where
fmap f (ConsF x) = ConsF x
instance Functor (Const t) where
fmap _ f = id
fzip _ create = fst
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
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
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)
instance Functor [] where
fmap _ = map
fzip _ create = lzip create
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)
type F a x = Rep (PF a) x
pmap :: Functor (PF a) => Ann a
-> (x -> y) -> F a x -> F a y
pmap (_::Ann a) f = fmap (ann:: Ann (Fix (PF a))) f
class Mu a where
inn :: F a a -> a
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
data I = FixId
type instance PF I = Id
instance Mu I where
inn = id
out = id
data K a = FixConst {unFixConst :: a}
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)}
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)}
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)}
type instance PF (a :@!: b) = PF a :@: PF b
instance Mu (a :@!: b) where
inn = FixComp
out = unFixComp
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
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)
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
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
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