module Proarrow.Profunctor.Forget where import Prelude (Monoid(..), map, foldMap) import Data.Kind (Type) import Proarrow.Category.Instance.Sub (SUBCAT(..), Sub (..)) import Proarrow.Core (OB, PRO, Profunctor(..), CategoryOf(..), Promonad(..)) import Proarrow.Adjunction (Adjunction(..)) import Proarrow.Profunctor.Composition ((:.:)(..)) import Proarrow.Profunctor.Representable (Representable(..), dimapRep) type Forget :: forall (ob :: OB k) -> PRO k (SUBCAT ob) data Forget ob a b where Forget :: ob b => a ~> b -> Forget ob a (SUB b) instance CategoryOf k => Profunctor (Forget (ob :: OB k)) where dimap :: forall (c :: k) (a :: k) (b :: SUBCAT ob) (d :: SUBCAT ob). (c ~> a) -> (b ~> d) -> Forget ob a b -> Forget ob c d dimap c ~> a l (Sub a1 ~> b1 r) (Forget a ~> b f) = (c ~> b1) -> Forget ob c (SUB b1) forall {k} (ob :: k -> Constraint) (a :: k) (a :: k). ob a => (a ~> a) -> Forget ob a (SUB a) Forget (a1 ~> b1 r (a1 ~> b1) -> (c ~> a1) -> c ~> b1 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 ~> a1 a ~> b f (a ~> a1) -> (c ~> a) -> c ~> a1 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 . c ~> a l) (Ob a, Ob b) => r r \\ :: forall (a :: k) (b :: SUBCAT ob) r. ((Ob a, Ob b) => r) -> Forget ob a b -> r \\ Forget a ~> b f = 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 f instance CategoryOf k => Representable (Forget (ob :: OB k)) where type Forget ob % (SUB a) = a index :: forall (a :: k) (b :: SUBCAT ob). Forget ob a b -> a ~> (Forget ob % b) index (Forget a ~> b f) = a ~> b a ~> (Forget ob % b) f tabulate :: forall (b :: SUBCAT ob) (a :: k). Ob b => (a ~> (Forget ob % b)) -> Forget ob a b tabulate = (a ~> UN SUB b) -> Forget ob a (SUB (UN SUB b)) (a ~> (Forget ob % b)) -> Forget ob a b forall {k} (ob :: k -> Constraint) (a :: k) (a :: k). ob a => (a ~> a) -> Forget ob a (SUB a) Forget repMap :: forall (a :: SUBCAT ob) (b :: SUBCAT ob). (a ~> b) -> (Forget ob % a) ~> (Forget ob % b) repMap (Sub a1 ~> b1 f) = a1 ~> b1 (Forget ob % a) ~> (Forget ob % b) f type List :: PRO (SUBCAT Monoid) Type data List a b where List :: Monoid a => (a -> [b]) -> List (SUB a) b instance Profunctor List where dimap :: forall (c :: SUBCAT Monoid) (a :: SUBCAT Monoid) b d. (c ~> a) -> (b ~> d) -> List a b -> List c d dimap = (c ~> a) -> (b ~> d) -> List a b -> List c d 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 (Ob a, Ob b) => r r \\ :: forall (a :: SUBCAT Monoid) b r. ((Ob a, Ob b) => r) -> List a b -> r \\ List{} = r (Ob a, Ob b) => r r instance Representable List where type List % a = SUB [a] index :: forall (a :: SUBCAT Monoid) b. List a b -> a ~> (List % b) index (List a -> [b] f) = (a ~> [b]) -> Sub (SUB a) (SUB [b]) forall {k} (ob :: OB k) (a1 :: k) (b1 :: k). (ob a1, ob b1) => (a1 ~> b1) -> Sub (SUB a1) (SUB b1) Sub a ~> [b] a -> [b] f tabulate :: forall b (a :: SUBCAT Monoid). Ob b => (a ~> (List % b)) -> List a b tabulate (Sub a1 ~> b1 f) = (a1 -> [b]) -> List (SUB a1) b forall a b. Monoid a => (a -> [b]) -> List (SUB a) b List a1 ~> b1 a1 -> [b] f repMap :: forall a b. (a ~> b) -> (List % a) ~> (List % b) repMap a ~> b f = ([a] ~> [b]) -> Sub (SUB [a]) (SUB [b]) forall {k} (ob :: OB k) (a1 :: k) (b1 :: k). (ob a1, ob b1) => (a1 ~> b1) -> Sub (SUB a1) (SUB b1) Sub ((a -> b) -> [a] -> [b] forall a b. (a -> b) -> [a] -> [b] map a ~> b a -> b f) instance Adjunction List (Forget Monoid) where unit :: forall a. Ob a => (:.:) (Forget Monoid) List a a unit = (a ~> [a]) -> Forget Monoid a (SUB [a]) forall {k} (ob :: k -> Constraint) (a :: k) (a :: k). ob a => (a ~> a) -> Forget ob a (SUB a) Forget (a -> [a] -> [a] forall a. a -> [a] -> [a] :[]) Forget Monoid a (SUB [a]) -> List (SUB [a]) a -> (:.:) (Forget Monoid) List a a forall {i} {j} {k} (p :: PRO i j) (a :: i) (b :: j) (q :: PRO j k) (c :: k). p a b -> q b c -> (:.:) p q a c :.: ([a] -> [a]) -> List (SUB [a]) a forall a b. Monoid a => (a -> [b]) -> List (SUB a) b List [a] -> [a] forall a. Ob a => a -> a forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a id counit :: (List :.: Forget Monoid) :~> (~>) counit (List a -> [b] g :.: Forget b ~> b f) = (a ~> b) -> Sub (SUB a) (SUB b) forall {k} (ob :: OB k) (a1 :: k) (b1 :: k). (ob a1, ob b1) => (a1 ~> b1) -> Sub (SUB a1) (SUB b1) Sub ((b -> b) -> [b] -> b forall m a. Monoid m => (a -> m) -> [a] -> m forall (t :: Type -> Type) m a. (Foldable t, Monoid m) => (a -> m) -> t a -> m foldMap b ~> b b -> b f ([b] -> b) -> (a -> [b]) -> a -> b 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 . a -> [b] g)