{-# LANGUAGE
GADTs
, RankNTypes
, TypeOperators
, TemplateHaskell
, ConstraintKinds
, FlexibleContexts
, FlexibleInstances
, ScopedTypeVariables
, UndecidableInstances
, MultiParamTypeClasses
, QuantifiedConstraints
#-}
module Data.Functor.HHCofree where
import Prelude hiding ((.), id)
import Control.Category
import Data.Bifunctor
import Data.Bifunctor.Functor
import Data.Profunctor
import Data.Profunctor.Monad
import Language.Haskell.TH.Syntax
import Data.Functor.Cofree.Internal
type f :~~> g = forall c d. f c d -> g c d
data HHCofree c g a b where
HHCofree :: c f => (f :~~> g) -> f a b -> HHCofree c g a b
deriveHHCofreeInstance :: Name -> Q [Dec]
deriveHHCofreeInstance :: Name -> Q [Dec]
deriveHHCofreeInstance = Name -> Name -> Name -> Q [Dec]
deriveCofreeInstance' ''HHCofree 'HHCofree
counit :: HHCofree c g :~~> g
counit :: forall (c :: (* -> * -> *) -> Constraint) (g :: * -> * -> *).
HHCofree c g :~~> g
counit (HHCofree f :~~> g
k f c d
fa) = f c d -> g c d
f :~~> g
k f c d
fa
leftAdjunct :: c f => (f :~~> g) -> f :~~> HHCofree c g
leftAdjunct :: forall (c :: (* -> * -> *) -> Constraint) (f :: * -> * -> *)
(g :: * -> * -> *).
c f =>
(f :~~> g) -> f :~~> HHCofree c g
leftAdjunct f :~~> g
f = (f :~~> g) -> f c d -> HHCofree c g c d
forall (c :: (* -> * -> *) -> Constraint) (f :: * -> * -> *)
(g :: * -> * -> *) a b.
c f =>
(f :~~> g) -> f a b -> HHCofree c g a b
HHCofree f :~~> g
f
unit :: c g => g :~~> HHCofree c g
unit :: forall (c :: (* -> * -> *) -> Constraint) (g :: * -> * -> *).
c g =>
g :~~> HHCofree c g
unit = (g :~~> g) -> g :~~> HHCofree c g
forall (c :: (* -> * -> *) -> Constraint) (f :: * -> * -> *)
(g :: * -> * -> *).
c f =>
(f :~~> g) -> f :~~> HHCofree c g
leftAdjunct g :~~> g
forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id
rightAdjunct :: (f :~~> HHCofree c g) -> f :~~> g
rightAdjunct :: forall (f :: * -> * -> *) (c :: (* -> * -> *) -> Constraint)
(g :: * -> * -> *).
(f :~~> HHCofree c g) -> f :~~> g
rightAdjunct f :~~> HHCofree c g
f = HHCofree c g c d -> g c d
forall (c :: (* -> * -> *) -> Constraint) (g :: * -> * -> *).
HHCofree c g :~~> g
counit (HHCofree c g c d -> g c d)
-> (f c d -> HHCofree c g c d) -> f c d -> g c d
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. f c d -> HHCofree c g c d
f :~~> HHCofree c g
f
transform :: (forall r. c r => (r :~~> f) -> r :~~> g) -> HHCofree c f :~~> HHCofree c g
transform :: forall (c :: (* -> * -> *) -> Constraint) (f :: * -> * -> *)
(g :: * -> * -> *).
(forall (r :: * -> * -> *). c r => (r :~~> f) -> r :~~> g)
-> HHCofree c f :~~> HHCofree c g
transform forall (r :: * -> * -> *). c r => (r :~~> f) -> r :~~> g
t (HHCofree f :~~> f
k f c d
a) = (f :~~> g) -> f c d -> HHCofree c g c d
forall (c :: (* -> * -> *) -> Constraint) (f :: * -> * -> *)
(g :: * -> * -> *) a b.
c f =>
(f :~~> g) -> f a b -> HHCofree c g a b
HHCofree ((f :~~> f) -> f :~~> g
forall (r :: * -> * -> *). c r => (r :~~> f) -> r :~~> g
t f :~~> f
k) f c d
a
hfmap :: (f :~~> g) -> HHCofree c f :~~> HHCofree c g
hfmap :: forall (f :: * -> * -> *) (g :: * -> * -> *)
(c :: (* -> * -> *) -> Constraint).
(f :~~> g) -> HHCofree c f :~~> HHCofree c g
hfmap f :~~> g
f = (forall (r :: * -> * -> *). c r => (r :~~> f) -> r :~~> g)
-> HHCofree c f :~~> HHCofree c g
forall (c :: (* -> * -> *) -> Constraint) (f :: * -> * -> *)
(g :: * -> * -> *).
(forall (r :: * -> * -> *). c r => (r :~~> f) -> r :~~> g)
-> HHCofree c f :~~> HHCofree c g
transform (\r :~~> f
g -> f c d -> g c d
f :~~> g
f (f c d -> g c d) -> (r c d -> f c d) -> r c d -> g c d
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. r c d -> f c d
r :~~> f
g)
hextend :: (HHCofree c f :~~> g) -> HHCofree c f :~~> HHCofree c g
hextend :: forall (c :: (* -> * -> *) -> Constraint) (f :: * -> * -> *)
(g :: * -> * -> *).
(HHCofree c f :~~> g) -> HHCofree c f :~~> HHCofree c g
hextend HHCofree c f :~~> g
f = (forall (r :: * -> * -> *). c r => (r :~~> f) -> r :~~> g)
-> HHCofree c f :~~> HHCofree c g
forall (c :: (* -> * -> *) -> Constraint) (f :: * -> * -> *)
(g :: * -> * -> *).
(forall (r :: * -> * -> *). c r => (r :~~> f) -> r :~~> g)
-> HHCofree c f :~~> HHCofree c g
transform (\r :~~> f
k -> HHCofree c f c d -> g c d
HHCofree c f :~~> g
f (HHCofree c f c d -> g c d)
-> (r c d -> HHCofree c f c d) -> r c d -> g c d
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (r :~~> f) -> r :~~> HHCofree c f
forall (c :: (* -> * -> *) -> Constraint) (f :: * -> * -> *)
(g :: * -> * -> *).
c f =>
(f :~~> g) -> f :~~> HHCofree c g
leftAdjunct r :~~> f
k)
instance BifunctorFunctor (HHCofree c) where
bifmap :: forall (p :: * -> * -> *) (q :: * -> * -> *).
(p :-> q) -> HHCofree c p :-> HHCofree c q
bifmap = (p :~~> q) -> HHCofree c p :~~> HHCofree c q
forall (f :: * -> * -> *) (g :: * -> * -> *)
(c :: (* -> * -> *) -> Constraint).
(f :~~> g) -> HHCofree c f :~~> HHCofree c g
hfmap
instance BifunctorComonad (HHCofree c) where
biextract :: forall (p :: * -> * -> *). HHCofree c p :-> p
biextract = HHCofree c p a b -> p a b
forall (c :: (* -> * -> *) -> Constraint) (g :: * -> * -> *).
HHCofree c g :~~> g
counit
biextend :: forall (p :: * -> * -> *) (q :: * -> * -> *).
(HHCofree c p :-> q) -> HHCofree c p :-> HHCofree c q
biextend = (HHCofree c p :~~> q) -> HHCofree c p :~~> HHCofree c q
forall (c :: (* -> * -> *) -> Constraint) (f :: * -> * -> *)
(g :: * -> * -> *).
(HHCofree c f :~~> g) -> HHCofree c f :~~> HHCofree c g
hextend
instance ProfunctorFunctor (HHCofree c) where
promap :: forall (p :: * -> * -> *) (q :: * -> * -> *).
Profunctor p =>
(p :-> q) -> HHCofree c p :-> HHCofree c q
promap = (p :~~> q) -> HHCofree c p :~~> HHCofree c q
forall (f :: * -> * -> *) (g :: * -> * -> *)
(c :: (* -> * -> *) -> Constraint).
(f :~~> g) -> HHCofree c f :~~> HHCofree c g
hfmap
instance ProfunctorComonad (HHCofree c) where
proextract :: forall (p :: * -> * -> *). Profunctor p => HHCofree c p :-> p
proextract = HHCofree c p a b -> p a b
forall (c :: (* -> * -> *) -> Constraint) (g :: * -> * -> *).
HHCofree c g :~~> g
counit
produplicate :: forall (p :: * -> * -> *).
Profunctor p =>
HHCofree c p :-> HHCofree c (HHCofree c p)
produplicate = (HHCofree c p :~~> HHCofree c p)
-> HHCofree c p :~~> HHCofree c (HHCofree c p)
forall (c :: (* -> * -> *) -> Constraint) (f :: * -> * -> *)
(g :: * -> * -> *).
(HHCofree c f :~~> g) -> HHCofree c f :~~> HHCofree c g
hextend HHCofree c p :~~> HHCofree c p
forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id
deriveCofreeInstance' ''HHCofree 'HHCofree ''Bifunctor
deriveCofreeInstance' ''HHCofree 'HHCofree ''Profunctor
deriveCofreeInstance' ''HHCofree 'HHCofree ''Strong
deriveCofreeInstance' ''HHCofree 'HHCofree ''Choice
deriveCofreeInstance' ''HHCofree 'HHCofree ''Closed