{-# LANGUAGE AllowAmbiguousTypes #-} module Proarrow.Profunctor.Representable where import Data.Kind (Constraint) import Proarrow.Core (PRO, CategoryOf(..), Profunctor(..), Promonad(..)) import Proarrow.Object (obj) infixl 8 % type Representable :: forall {j} {k}. PRO j k -> Constraint class Profunctor p => Representable (p :: PRO j k) where type p % (a :: k) :: j index :: p a b -> a ~> p % b tabulate :: Ob b => (a ~> p % b) -> p a b repMap :: (a ~> b) -> p % a ~> p % b withRepCod :: forall p a r. (Representable p, Ob a) => (Ob (p % a) => r) -> r withRepCod :: forall {k} {k} (p :: PRO k k) (a :: k) r. (Representable p, Ob a) => (Ob (p % a) => r) -> r withRepCod Ob (p % a) => r r = r Ob (p % a) => r (Ob (p % a), Ob (p % a)) => r r ((Ob (p % a), Ob (p % a)) => r) -> ((p % a) ~> (p % a)) -> 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 \\ forall {j} {k} (p :: PRO j k) (a :: k) (b :: k). Representable p => (a ~> b) -> (p % a) ~> (p % b) forall (p :: PRO k k) (a :: k) (b :: k). Representable p => (a ~> b) -> (p % a) ~> (p % b) repMap @p (forall (a :: k). (CategoryOf k, Ob a) => Obj a forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a obj @a) dimapRep :: forall p a b c d. Representable p => (c ~> a) -> (b ~> d) -> p a b -> p c d dimapRep :: forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) (c :: j) (d :: k). Representable p => (c ~> a) -> (b ~> d) -> p a b -> p c d dimapRep c ~> a l b ~> d r = forall {j} {k} (p :: PRO j k) (b :: k) (a :: j). (Representable p, Ob b) => (a ~> (p % b)) -> p a b forall (p :: PRO j k) (b :: k) (a :: j). (Representable p, Ob b) => (a ~> (p % b)) -> p a b tabulate @p ((c ~> (p % d)) -> p c d) -> (p a b -> c ~> (p % d)) -> p a b -> p c d forall b c a. (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 . (c ~> a) -> ((p % b) ~> (p % d)) -> (a ~> (p % b)) -> c ~> (p % d) forall (c :: j) (a :: j) (b :: j) (d :: j). (c ~> a) -> (b ~> d) -> (a ~> b) -> c ~> d forall {j} {k} (p :: PRO j k) (c :: j) (a :: j) (b :: k) (d :: k). Profunctor p => (c ~> a) -> (b ~> d) -> p a b -> p c d dimap c ~> a l (forall {j} {k} (p :: PRO j k) (a :: k) (b :: k). Representable p => (a ~> b) -> (p % a) ~> (p % b) forall (p :: PRO j k) (a :: k) (b :: k). Representable p => (a ~> b) -> (p % a) ~> (p % b) repMap @p b ~> d r) ((a ~> (p % b)) -> c ~> (p % d)) -> (p a b -> a ~> (p % b)) -> p a b -> c ~> (p % d) forall b c a. (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 . p a b -> a ~> (p % b) forall (a :: j) (b :: k). p a b -> a ~> (p % b) forall {j} {k} (p :: PRO j k) (a :: j) (b :: k). Representable p => p a b -> a ~> (p % b) index ((Ob b, Ob d) => p a b -> p c d) -> (b ~> d) -> p a b -> p c d 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 \\ b ~> d r