{-# LANGUAGE AllowAmbiguousTypes #-} module Proarrow.Profunctor.Cofree where import Data.Kind (Constraint) import Prelude (Int) import Proarrow.Adjunction (Adjunction (..)) import Proarrow.Category.Instance.Sub (SUBCAT (..), Sub (..)) import Proarrow.Core (CategoryOf (..), OB, Profunctor (..), Promonad (..), type (+->)) import Proarrow.Profunctor.Composition ((:.:) (..)) import Proarrow.Profunctor.Forget (Forget (..)) import Proarrow.Profunctor.Representable (Representable (..), repObj) import Proarrow.Profunctor.Star (Star (..)) type HasCofree :: forall {k}. (k -> Constraint) -> Constraint class (CategoryOf k, Representable (Cofree ob), forall b. (Ob b) => ob (Cofree ob % b)) => HasCofree (ob :: k -> Constraint) where type Cofree ob :: k +-> k lower' :: Cofree ob a b -> a ~> b section' :: (ob a) => a ~> b -> Cofree ob a b lower :: forall ob a. (HasCofree ob, Ob a) => Cofree ob % a ~> a lower :: forall {k} (ob :: k -> Constraint) (a :: k). (HasCofree ob, Ob a) => (Cofree ob % a) ~> a lower = forall {k} (ob :: k -> Constraint) (a :: k) (b :: k). HasCofree ob => Cofree ob a b -> a ~> b forall (ob :: k -> Constraint) (a :: k) (b :: k). HasCofree ob => Cofree ob a b -> a ~> b lower' @ob (forall {j} {k} (p :: j +-> k) (b :: j) (a :: k). (Representable p, Ob b) => (a ~> (p % b)) -> p a b forall (p :: k +-> k) (b :: k) (a :: k). (Representable p, Ob b) => (a ~> (p % b)) -> p a b tabulate @(Cofree ob) (forall {j} {k} (p :: j +-> k) (a :: j). (Representable p, Ob a) => Obj (p % a) forall (p :: k +-> k) (a :: k). (Representable p, Ob a) => Obj (p % a) repObj @(Cofree ob) @a)) section :: forall ob a. (HasCofree ob, ob a, Ob a) => a ~> Cofree ob % a section :: forall {j} (ob :: j -> Constraint) (a :: j). (HasCofree ob, ob a, Ob a) => a ~> (Cofree ob % a) section = forall {j} {k} (p :: j +-> k) (a :: k) (b :: j). Representable p => p a b -> a ~> (p % b) forall (p :: j +-> j) (a :: j) (b :: j). Representable p => p a b -> a ~> (p % b) index @(Cofree ob) (forall {k} (ob :: k -> Constraint) (a :: k) (b :: k). (HasCofree ob, ob a) => (a ~> b) -> Cofree ob a b forall (ob :: j -> Constraint) (a :: j) (b :: j). (HasCofree ob, ob a) => (a ~> b) -> Cofree ob a b section' @ob a ~> a forall (a :: j). Ob a => a ~> a forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a id) type CofreeSub :: forall (ob :: OB k) -> k +-> SUBCAT ob data CofreeSub ob a b where CofreeSub :: (ob a) => a ~> b -> CofreeSub ob (SUB a) b instance (CategoryOf k) => Profunctor (CofreeSub (ob :: OB k)) where dimap :: forall (c :: SUBCAT ob) (a :: SUBCAT ob) (b :: k) (d :: k). (c ~> a) -> (b ~> d) -> CofreeSub ob a b -> CofreeSub ob c d dimap (Sub a1 ~> b1 f) b ~> d g (CofreeSub a ~> b h) = (a1 ~> d) -> CofreeSub ob (SUB a1) d forall {k} (ob :: k -> Constraint) (a :: k) (b :: k). ob a => (a ~> b) -> CofreeSub ob (SUB a) b CofreeSub (b ~> d g (b ~> d) -> (a1 ~> b) -> a1 ~> d 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 . b1 ~> b a ~> b h (b1 ~> b) -> (a1 ~> b1) -> a1 ~> 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 . a1 ~> b1 f) (Ob a, Ob b) => r r \\ :: forall (a :: SUBCAT ob) (b :: k) r. ((Ob a, Ob b) => r) -> CofreeSub ob a b -> r \\ CofreeSub a ~> b p = 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 p instance (HasCofree ob) => Representable (CofreeSub ob) where type CofreeSub ob % a = SUB (Cofree ob % a) index :: forall (a :: SUBCAT ob) (b :: j). CofreeSub ob a b -> a ~> (CofreeSub ob % b) index (CofreeSub a ~> b f) = (a ~> (Cofree ob % b)) -> Sub (~>) (SUB a) (SUB (Cofree ob % b)) forall {k} (ob :: OB k) (a1 :: k) (b1 :: k) (p :: CAT k). (ob a1, ob b1) => p a1 b1 -> Sub p (SUB a1) (SUB b1) Sub (Cofree ob a b -> a ~> (Cofree ob % b) forall (a :: j) (b :: j). Cofree ob a b -> a ~> (Cofree ob % b) forall {j} {k} (p :: j +-> k) (a :: k) (b :: j). Representable p => p a b -> a ~> (p % b) index (forall {k} (ob :: k -> Constraint) (a :: k) (b :: k). (HasCofree ob, ob a) => (a ~> b) -> Cofree ob a b forall (ob :: j -> Constraint) (a :: j) (b :: j). (HasCofree ob, ob a) => (a ~> b) -> Cofree ob a b section' @ob a ~> b f)) ((Ob a, Ob b) => Sub (~>) (SUB a) (SUB (Cofree ob % b))) -> (a ~> b) -> Sub (~>) (SUB a) (SUB (Cofree ob % b)) forall (a :: j) (b :: j) 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 tabulate :: forall (b :: j) (a :: SUBCAT ob). Ob b => (a ~> (CofreeSub ob % b)) -> CofreeSub ob a b tabulate (Sub a1 ~> b1 f) = (a1 ~> b) -> CofreeSub ob (SUB a1) b forall {k} (ob :: k -> Constraint) (a :: k) (b :: k). ob a => (a ~> b) -> CofreeSub ob (SUB a) b CofreeSub (forall {k} (ob :: k -> Constraint) (a :: k) (b :: k). HasCofree ob => Cofree ob a b -> a ~> b forall (ob :: j -> Constraint) (a :: j) (b :: j). HasCofree ob => Cofree ob a b -> a ~> b lower' @ob ((a1 ~> (Cofree ob % b)) -> Cofree ob a1 b forall (b :: j) (a :: j). Ob b => (a ~> (Cofree ob % b)) -> Cofree ob a b forall {j} {k} (p :: j +-> k) (b :: j) (a :: k). (Representable p, Ob b) => (a ~> (p % b)) -> p a b tabulate a1 ~> b1 a1 ~> (Cofree ob % b) f)) repMap :: forall (a :: j) (b :: j). (a ~> b) -> (CofreeSub ob % a) ~> (CofreeSub ob % b) repMap a ~> b f = ((Cofree ob % a) ~> (Cofree ob % b)) -> Sub (~>) (SUB (Cofree ob % a)) (SUB (Cofree ob % b)) forall {k} (ob :: OB k) (a1 :: k) (b1 :: k) (p :: CAT k). (ob a1, ob b1) => p a1 b1 -> Sub p (SUB a1) (SUB b1) Sub (forall {j} {k} (p :: j +-> k) (a :: j) (b :: j). Representable p => (a ~> b) -> (p % a) ~> (p % b) forall (p :: j +-> j) (a :: j) (b :: j). Representable p => (a ~> b) -> (p % a) ~> (p % b) repMap @(Cofree ob) a ~> b f) ((Ob a, Ob b) => Sub (~>) (SUB (Cofree ob % a)) (SUB (Cofree ob % b))) -> (a ~> b) -> Sub (~>) (SUB (Cofree ob % a)) (SUB (Cofree ob % b)) forall (a :: j) (b :: j) 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 (HasCofree ob) => Adjunction (Forget ob) (CofreeSub ob) where unit :: forall (a :: SUBCAT ob). Ob a => (:.:) (CofreeSub ob) (Forget ob) a a unit = (UN SUB a ~> UN SUB a) -> CofreeSub ob (SUB (UN SUB a)) (UN SUB a) forall {k} (ob :: k -> Constraint) (a :: k) (b :: k). ob a => (a ~> b) -> CofreeSub ob (SUB a) b CofreeSub UN SUB a ~> UN SUB a forall (a :: k). Ob a => a ~> a forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a id CofreeSub ob a (UN SUB a) -> Forget ob (UN SUB a) a -> (:.:) (CofreeSub ob) (Forget ob) a a forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j) (c :: i). p a b -> q b c -> (:.:) p q a c :.: (UN SUB a ~> UN SUB a) -> Forget ob (UN SUB a) (SUB (UN SUB a)) forall {k} (ob :: OB k) (b1 :: k) (a :: k). ob b1 => (a ~> b1) -> Forget ob a (SUB b1) Forget UN SUB a ~> UN SUB a forall (a :: k). Ob a => a ~> a forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a id counit :: (Forget ob :.: CofreeSub ob) :~> (~>) counit (Forget a ~> b1 f :.: CofreeSub a ~> b g) = b1 ~> b a ~> b g (b1 ~> b) -> (a ~> b1) -> 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 ~> b1 f class Test a where test :: a -> Int instance HasCofree Test where type Cofree Test = Star ((,) Int) lower' :: forall a b. Cofree Test a b -> a ~> b lower' (Star a ~> (Int, b) f) a a = case a ~> (Int, b) a -> (Int, b) f a a of (Int _, b b) -> b b section' :: forall a b. Test a => (a ~> b) -> Cofree Test a b section' a ~> b f = (a ~> (Int, b)) -> Star ((,) Int) a b forall {k1} {k2} (b :: k1) (a :: k2) (f :: k1 -> k2). Ob b => (a ~> f b) -> Star f a b Star \a a -> (a -> Int forall a. Test a => a -> Int test a a, a ~> b a -> b f a a) instance Test (Int, a) where test :: (Int, a) -> Int test (Int i, a _) = Int i