module Proarrow.Category.Monoidal.Rev where import Proarrow.Core (CAT, Profunctor(..), Promonad(..), CategoryOf(..), dimapDefault, UN, Is) import Proarrow.Category.Monoidal (Monoidal(..), SymMonoidal(..)) type data REV k = R k type instance UN R (R a) = a type Rev :: CAT k data Rev a b where Rev :: a ~> b -> Rev (R a) (R b) instance CategoryOf k => Profunctor (Rev :: CAT (REV k)) where dimap :: forall (c :: REV k) (a :: REV k) (b :: REV k) (d :: REV k). (c ~> a) -> (b ~> d) -> Rev a b -> Rev c d dimap = (c ~> a) -> (b ~> d) -> Rev a b -> Rev c d Rev c a -> Rev b d -> Rev a b -> Rev c d forall {k} (p :: PRO k k) (c :: k) (a :: k) (b :: k) (d :: k). Promonad p => p c a -> p b d -> p a b -> p c d dimapDefault (Ob a, Ob b) => r r \\ :: forall (a :: REV k) (b :: REV k) r. ((Ob a, Ob b) => r) -> Rev a b -> r \\ Rev a ~> b t = r (Ob a, Ob b) => r (Ob a, Ob b) => r r ((Ob a, Ob b) => r) -> (a ~> b) -> r forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r. Profunctor p => ((Ob a, Ob b) => r) -> p a b -> r \\ a ~> b a ~> b t instance CategoryOf k => Promonad (Rev :: CAT (REV k)) where id :: forall (a :: REV k). Ob a => Rev a a id = (UN R a ~> UN R a) -> Rev (R (UN R a)) (R (UN R a)) forall {k} (a :: k) (b :: k). (a ~> b) -> Rev (R a) (R b) Rev UN R a ~> UN R a forall (a :: k). Ob a => a ~> a forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a id Rev a ~> b f . :: forall (b :: REV k) (c :: REV k) (a :: REV k). Rev b c -> Rev a b -> Rev a c . Rev a ~> b g = (a ~> b) -> Rev (R a) (R b) forall {k} (a :: k) (b :: k). (a ~> b) -> Rev (R a) (R b) Rev (a ~> b a ~> b f (a ~> b) -> (a ~> a) -> a ~> b forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k). Promonad p => p b c -> p a b -> p a c . a ~> a a ~> b g) instance CategoryOf k => CategoryOf (REV k) where type (~>) = Rev type Ob a = (Is R a, Ob (UN R a)) instance Monoidal k => Monoidal (REV k) where type Unit = R Unit type (R a) ** (R b) = R (b ** a) Rev a ~> b f par :: forall (a :: REV k) (b :: REV k) (c :: REV k) (d :: REV k). (a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d) `par` Rev a ~> b g = ((a ** a) ~> (b ** b)) -> Rev (R (a ** a)) (R (b ** b)) forall {k} (a :: k) (b :: k). (a ~> b) -> Rev (R a) (R b) Rev (a ~> b a ~> b g (a ~> b) -> (a ~> b) -> (a ** a) ~> (b ** b) forall (a :: k) (b :: k) (c :: k) (d :: k). (a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d) forall k (a :: k) (b :: k) (c :: k) (d :: k). Monoidal k => (a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d) `par` a ~> b a ~> b f) leftUnitor :: forall (a :: REV k). Obj a -> (Unit ** a) ~> a leftUnitor (Rev a ~> b a) = ((a ** Unit) ~> a) -> Rev (R (a ** Unit)) (R a) forall {k} (a :: k) (b :: k). (a ~> b) -> Rev (R a) (R b) Rev (Obj a -> (a ** Unit) ~> a forall (a :: k). Obj a -> (a ** Unit) ~> a forall k (a :: k). Monoidal k => Obj a -> (a ** Unit) ~> a rightUnitor Obj a a ~> b a) leftUnitorInv :: forall (a :: REV k). Obj a -> a ~> (Unit ** a) leftUnitorInv (Rev a ~> b a) = (a ~> (a ** Unit)) -> Rev (R a) (R (a ** Unit)) forall {k} (a :: k) (b :: k). (a ~> b) -> Rev (R a) (R b) Rev (Obj a -> a ~> (a ** Unit) forall (a :: k). Obj a -> a ~> (a ** Unit) forall k (a :: k). Monoidal k => Obj a -> a ~> (a ** Unit) rightUnitorInv Obj a a ~> b a) rightUnitor :: forall (a :: REV k). Obj a -> (a ** Unit) ~> a rightUnitor (Rev a ~> b a) = ((Unit ** a) ~> a) -> Rev (R (Unit ** a)) (R a) forall {k} (a :: k) (b :: k). (a ~> b) -> Rev (R a) (R b) Rev (Obj a -> (Unit ** a) ~> a forall (a :: k). Obj a -> (Unit ** a) ~> a forall k (a :: k). Monoidal k => Obj a -> (Unit ** a) ~> a leftUnitor Obj a a ~> b a) rightUnitorInv :: forall (a :: REV k). Obj a -> a ~> (a ** Unit) rightUnitorInv (Rev a ~> b a) = (a ~> (Unit ** a)) -> Rev (R a) (R (Unit ** a)) forall {k} (a :: k) (b :: k). (a ~> b) -> Rev (R a) (R b) Rev (Obj a -> a ~> (Unit ** a) forall (a :: k). Obj a -> a ~> (Unit ** a) forall k (a :: k). Monoidal k => Obj a -> a ~> (Unit ** a) leftUnitorInv Obj a a ~> b a) associator :: forall (a :: REV k) (b :: REV k) (c :: REV k). Obj a -> Obj b -> Obj c -> ((a ** b) ** c) ~> (a ** (b ** c)) associator (Rev a ~> b a) (Rev a ~> b b) (Rev a ~> b c) = ((a ** (a ** a)) ~> ((a ** a) ** a)) -> Rev (R (a ** (a ** a))) (R ((a ** a) ** a)) forall {k} (a :: k) (b :: k). (a ~> b) -> Rev (R a) (R b) Rev (Obj a -> Obj a -> Obj a -> (a ** (a ** a)) ~> ((a ** a) ** a) forall (a :: k) (b :: k) (c :: k). Obj a -> Obj b -> Obj c -> (a ** (b ** c)) ~> ((a ** b) ** c) forall k (a :: k) (b :: k) (c :: k). Monoidal k => Obj a -> Obj b -> Obj c -> (a ** (b ** c)) ~> ((a ** b) ** c) associatorInv Obj a a ~> b c Obj a a ~> b b Obj a a ~> b a) associatorInv :: forall (a :: REV k) (b :: REV k) (c :: REV k). Obj a -> Obj b -> Obj c -> (a ** (b ** c)) ~> ((a ** b) ** c) associatorInv (Rev a ~> b a) (Rev a ~> b b) (Rev a ~> b c) = (((a ** a) ** a) ~> (a ** (a ** a))) -> Rev (R ((a ** a) ** a)) (R (a ** (a ** a))) forall {k} (a :: k) (b :: k). (a ~> b) -> Rev (R a) (R b) Rev (Obj a -> Obj a -> Obj a -> ((a ** a) ** a) ~> (a ** (a ** a)) forall (a :: k) (b :: k) (c :: k). Obj a -> Obj b -> Obj c -> ((a ** b) ** c) ~> (a ** (b ** c)) forall k (a :: k) (b :: k) (c :: k). Monoidal k => Obj a -> Obj b -> Obj c -> ((a ** b) ** c) ~> (a ** (b ** c)) associator Obj a a ~> b c Obj a a ~> b b Obj a a ~> b a) instance SymMonoidal k => SymMonoidal (REV k) where swap' :: forall (a :: REV k) (b :: REV k). Obj a -> Obj b -> (a ** b) ~> (b ** a) swap' (Rev a ~> b a) (Rev a ~> b b) = ((a ** a) ~> (a ** a)) -> Rev (R (a ** a)) (R (a ** a)) forall {k} (a :: k) (b :: k). (a ~> b) -> Rev (R a) (R b) Rev (Obj a -> Obj a -> (a ** a) ~> (a ** a) forall (a :: k) (b :: k). Obj a -> Obj b -> (a ** b) ~> (b ** a) forall k (a :: k) (b :: k). SymMonoidal k => Obj a -> Obj b -> (a ** b) ~> (b ** a) swap' Obj a a ~> b b Obj a a ~> b a)