module Hask.Prof where
import Hask.Core
data Prof :: (j -> k -> *) -> (i -> j -> *) -> i -> k -> * where
Prof :: p b c -> q a b -> Prof p q a c
instance Category ((~>) :: i -> i -> *) => Semitensor (Prof :: (i -> i -> *) -> (i -> i -> *) -> i -> i -> *) where
type Tensorable Prof = Profunctor
second = fmap1
associate = associateProf
type instance I Prof = (~>)
instance Category ((~>) :: i -> i -> *) => Tensor (Prof :: (i -> i -> *) -> (i -> i -> *) -> i -> i -> *) where
lambda = lambdaProf
rho = rhoProf
instance Functor Prof where
fmap f = nat3 $ \(Prof p q) -> Prof (runNat2 f p) q
instance Functor (Prof p) where
fmap f = nat2 $ \(Prof p q) -> Prof p (runNat2 f q)
instance Contravariant q => Contravariant (Prof p q) where
contramap f = Nat $ \(Prof p q) -> Prof p (runNat (contramap f) q)
instance Post Functor p => Functor (Prof p q a) where
fmap f (Prof p q) = Prof (fmap1 f p) q
instance Functor q => Functor (Prof p q) where
fmap f = Nat $ \(Prof p q) -> Prof p (runNat (fmap f) q)
instance Post Contravariant p => Contravariant (Prof p q a) where
contramap f (Prof p q) = Prof (contramap1 f p) q
associateProf :: Iso (Prof (Prof p q) r) (Prof (Prof p' q') r')
(Prof p (Prof q r)) (Prof p' (Prof q' r'))
associateProf = dimap
(nat2 $ \ (Prof (Prof a b) c) -> Prof a (Prof b c))
(nat2 $ \ (Prof a (Prof b c)) -> Prof (Prof a b) c)
whiskerProfL :: (p ~> q) -> Prof p r ~> Prof q r
whiskerProfL = first
whiskerProfR :: (p ~> q) -> Prof l p ~> Prof l q
whiskerProfR = fmap
lambdaProf :: (Category k, k ~ Hom, Post Functor p) => Iso (Prof k p) (Prof k q) p q
lambdaProf = dimap (nat2 $ \(Prof k p) -> fmap1 k p) (nat2 $ Prof id)
rhoProf :: (Category k, k ~ Hom, Contravariant p) => Iso (Prof p k) (Prof q k) p q
rhoProf = dimap (nat2 $ \(Prof p k) -> lmap k p) (nat2 $ \q -> Prof q id)
newtype ProfR p q a b = ProfR { runProfR :: forall x. p x a -> q x b }
instance Contravariant ProfR where
contramap f = nat3 $ \(ProfR pq) -> ProfR $ \p -> pq (runNat2 f p)
instance Functor (ProfR p) where
fmap f = nat2 $ \(ProfR pq) -> ProfR $ \p -> runNat2 f (pq p)
instance Post Functor p => Contravariant (ProfR p q) where
contramap f = Nat $ \(ProfR pq) -> ProfR $ \p -> pq (fmap1 f p)
instance Post Functor q => Functor (ProfR p q a) where
fmap f (ProfR pq) = ProfR $ \p -> fmap1 f (pq p)
instance Post Contravariant p => Functor (ProfR p q) where
fmap f = Nat $ \(ProfR pq) -> ProfR $ \p -> pq (contramap1 f p)
instance Post Contravariant q => Contravariant (ProfR p q a) where
contramap f (ProfR pq) = ProfR $ \p -> contramap1 f (pq p)
type instance I ProfR = (~>)
iotaProf :: (Category p, p ~ (~>), Contravariant q') => Iso (ProfR p q) (ProfR (~>) q') q q'
iotaProf = dimap (nat2 $ \(ProfR f) -> f id) (nat2 $ \f -> ProfR $ \p -> lmap p f)
jotProf :: Post Functor p => (~>) ~> ProfR p p
jotProf = nat2 $ \f -> ProfR (fmap1 f)
instance Curried Prof ProfR where
curry k = nat2 $ \p -> ProfR $ \q -> runNat2 k (Prof p q)
uncurry k = nat2 $ \(Prof p q) -> runProfR (runNat2 k p) q