module Proarrow.Profunctor.Fix where import Data.Functor.Const (Const (..)) import Proarrow.Core (Profunctor(..), PRO, Promonad (..), (:~>)) import Proarrow.Functor (Functor(..)) import Proarrow.Category.Instance.Prof (Prof(..)) import Proarrow.Profunctor.Star (Star(..)) import Proarrow.Category.Instance.Nat (Nat(..)) import Proarrow.Profunctor.Composition ((:.:)(..)) type Fix :: PRO k k -> PRO k k newtype Fix p a b where In :: { forall {k} (p :: PRO k k) (a :: k) (b :: k). Fix p a b -> (:.:) p (Fix p) a b out :: (p :.: Fix p) a b } -> Fix p a b instance Profunctor p => Profunctor (Fix p) where dimap :: forall (c :: k) (a :: k) (b :: k) (d :: k). (c ~> a) -> (b ~> d) -> Fix p a b -> Fix p c d dimap c ~> a l b ~> d r = (:.:) p (Fix p) c d -> Fix p c d forall {k} (p :: PRO k k) (a :: k) (b :: k). (:.:) p (Fix p) a b -> Fix p a b In ((:.:) p (Fix p) c d -> Fix p c d) -> (Fix p a b -> (:.:) p (Fix p) c d) -> Fix p a b -> Fix 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) -> (b ~> d) -> (:.:) p (Fix p) a b -> (:.:) p (Fix p) c d forall (c :: k) (a :: k) (b :: k) (d :: k). (c ~> a) -> (b ~> d) -> (:.:) p (Fix p) a b -> (:.:) p (Fix p) 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 b ~> d r ((:.:) p (Fix p) a b -> (:.:) p (Fix p) c d) -> (Fix p a b -> (:.:) p (Fix p) a b) -> Fix p a b -> (:.:) p (Fix 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 . Fix p a b -> (:.:) p (Fix p) a b forall {k} (p :: PRO k k) (a :: k) (b :: k). Fix p a b -> (:.:) p (Fix p) a b out ((Ob c, Ob a) => Fix p a b -> Fix p c d) -> (c ~> a) -> Fix p a b -> Fix 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 \\ c ~> a l ((Ob b, Ob d) => Fix p a b -> Fix p c d) -> (b ~> d) -> Fix p a b -> Fix 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 (Ob a, Ob b) => r r \\ :: forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> Fix p a b -> r \\ In (:.:) p (Fix p) a b p = r (Ob a, Ob b) => r r ((Ob a, Ob b) => r) -> (:.:) p (Fix p) a b -> r forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (:.:) p (Fix p) 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 \\ (:.:) p (Fix p) a b p instance Functor Fix where map :: forall (a :: k -> k -> Type) (b :: k -> k -> Type). (a ~> b) -> Fix a ~> Fix b map n :: a ~> b n@Prof{} = (Fix a :~> Fix b) -> Prof (Fix a) (Fix b) forall {j} {k} (p :: PRO j k) (q :: PRO j k). (Profunctor p, Profunctor q) => (p :~> q) -> Prof p q Prof ((:.:) b (Fix b) a b -> Fix b a b forall {k} (p :: PRO k k) (a :: k) (b :: k). (:.:) p (Fix p) a b -> Fix p a b In ((:.:) b (Fix b) a b -> Fix b a b) -> (Fix a a b -> (:.:) b (Fix b) a b) -> Fix a a b -> Fix 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 . Prof (a :.: Fix a) (b :.: Fix b) -> (a :.: Fix a) :~> (b :.: Fix b) forall {k} {k1} (p :: PRO k k1) (q :: PRO k k1). Prof p q -> p :~> q getProf (Nat ((:.:) a) ((:.:) b) -> (:.:) a .~> (:.:) b forall {k} {k1} (f :: k -> k1) (g :: k -> k1). Nat f g -> f .~> g getNat ((a ~> b) -> (:.:) a ~> (:.:) b forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1). Functor f => (a ~> b) -> f a ~> f b forall (a :: k -> k -> Type) (b :: k -> k -> Type). (a ~> b) -> (:.:) a ~> (:.:) b map a ~> b n) Prof (a :.: Fix b) (b :.: Fix b) -> Prof (a :.: Fix a) (a :.: Fix b) -> Prof (a :.: Fix a) (b :.: Fix b) forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k). Promonad p => p b c -> p a b -> p a c forall (b :: k -> k -> Type) (c :: k -> k -> Type) (a :: k -> k -> Type). Prof b c -> Prof a b -> Prof a c . (Fix a ~> Fix b) -> (a :.: Fix a) ~> (a :.: Fix b) forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1). Functor f => (a ~> b) -> f a ~> f b forall (a :: k -> k -> Type) (b :: k -> k -> Type). (a ~> b) -> (a :.: a) ~> (a :.: b) map ((a ~> b) -> Fix a ~> Fix b forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1). Functor f => (a ~> b) -> f a ~> f b forall (a :: k -> k -> Type) (b :: k -> k -> Type). (a ~> b) -> Fix a ~> Fix b map a ~> b n)) ((:.:) a (Fix a) a b -> (:.:) b (Fix b) a b) -> (Fix a a b -> (:.:) a (Fix a) a b) -> Fix a a b -> (:.:) b (Fix 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 . Fix a a b -> (:.:) a (Fix a) a b forall {k} (p :: PRO k k) (a :: k) (b :: k). Fix p a b -> (:.:) p (Fix p) a b out) cata :: (Profunctor p, Profunctor r) => (p :.: r :~> r) -> Fix p :~> r cata :: forall {k1} (p :: PRO k1 k1) (r :: PRO k1 k1). (Profunctor p, Profunctor r) => ((p :.: r) :~> r) -> Fix p :~> r cata (p :.: r) :~> r alg = Prof (Fix p) r -> Fix p :~> r forall {k} {k1} (p :: PRO k k1) (q :: PRO k k1). Prof p q -> p :~> q getProf Prof (Fix p) r go where go :: Prof (Fix p) r go = ((p :.: r) :~> r) -> Prof (p :.: r) r forall {j} {k} (p :: PRO j k) (q :: PRO j k). (Profunctor p, Profunctor q) => (p :~> q) -> Prof p q Prof (:.:) p r a b -> r a b (p :.: r) :~> r alg Prof (p :.: r) r -> Prof (Fix p) (p :.: r) -> Prof (Fix p) r forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k). Promonad p => p b c -> p a b -> p a c forall (b :: PRO k1 k1) (c :: PRO k1 k1) (a :: PRO k1 k1). Prof b c -> Prof a b -> Prof a c . (Fix p ~> r) -> (p :.: Fix p) ~> (p :.: r) forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1). Functor f => (a ~> b) -> f a ~> f b forall (a :: PRO k1 k1) (b :: PRO k1 k1). (a ~> b) -> (p :.: a) ~> (p :.: b) map Fix p ~> r Prof (Fix p) r go Prof (p :.: Fix p) (p :.: r) -> Prof (Fix p) (p :.: Fix p) -> Prof (Fix p) (p :.: r) forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k). Promonad p => p b c -> p a b -> p a c forall (b :: PRO k1 k1) (c :: PRO k1 k1) (a :: PRO k1 k1). Prof b c -> Prof a b -> Prof a c . (Fix p :~> (p :.: Fix p)) -> Prof (Fix p) (p :.: Fix p) forall {j} {k} (p :: PRO j k) (q :: PRO j k). (Profunctor p, Profunctor q) => (p :~> q) -> Prof p q Prof Fix p a b -> (:.:) p (Fix p) a b Fix p :~> (p :.: Fix p) forall {k} (p :: PRO k k) (a :: k) (b :: k). Fix p a b -> (:.:) p (Fix p) a b out ana :: (Profunctor p, Profunctor r) => (r :~> p :.: r) -> r :~> Fix p ana :: forall {k1} (p :: PRO k1 k1) (r :: PRO k1 k1). (Profunctor p, Profunctor r) => (r :~> (p :.: r)) -> r :~> Fix p ana r :~> (p :.: r) coalg = Prof r (Fix p) -> r :~> Fix p forall {k} {k1} (p :: PRO k k1) (q :: PRO k k1). Prof p q -> p :~> q getProf Prof r (Fix p) go where go :: Prof r (Fix p) go = ((p :.: Fix p) :~> Fix p) -> Prof (p :.: Fix p) (Fix p) forall {j} {k} (p :: PRO j k) (q :: PRO j k). (Profunctor p, Profunctor q) => (p :~> q) -> Prof p q Prof (:.:) p (Fix p) a b -> Fix p a b (p :.: Fix p) :~> Fix p forall {k} (p :: PRO k k) (a :: k) (b :: k). (:.:) p (Fix p) a b -> Fix p a b In Prof (p :.: Fix p) (Fix p) -> Prof r (p :.: Fix p) -> Prof r (Fix p) forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k). Promonad p => p b c -> p a b -> p a c forall (b :: PRO k1 k1) (c :: PRO k1 k1) (a :: PRO k1 k1). Prof b c -> Prof a b -> Prof a c . (r ~> Fix p) -> (p :.: r) ~> (p :.: Fix p) forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1). Functor f => (a ~> b) -> f a ~> f b forall (a :: PRO k1 k1) (b :: PRO k1 k1). (a ~> b) -> (p :.: a) ~> (p :.: b) map r ~> Fix p Prof r (Fix p) go Prof (p :.: r) (p :.: Fix p) -> Prof r (p :.: r) -> Prof r (p :.: Fix p) forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k). Promonad p => p b c -> p a b -> p a c forall (b :: PRO k1 k1) (c :: PRO k1 k1) (a :: PRO k1 k1). Prof b c -> Prof a b -> Prof a c . (r :~> (p :.: r)) -> Prof r (p :.: r) forall {j} {k} (p :: PRO j k) (q :: PRO j k). (Profunctor p, Profunctor q) => (p :~> q) -> Prof p q Prof r a b -> (:.:) p r a b r :~> (p :.: r) coalg data ListF x l = Nil | Cons x l instance Functor (ListF x) where map :: forall a b. (a ~> b) -> ListF x a ~> ListF x b map a ~> b _ ListF x a Nil = ListF x b forall x l. ListF x l Nil map a ~> b f (Cons x x a l) = x -> b -> ListF x b forall x l. x -> l -> ListF x l Cons x x (a ~> b a -> b f a l) embed :: ListF x [x] -> [x] embed :: forall x. ListF x [x] -> [x] embed ListF x [x] Nil = [] embed (Cons x x [x] xs) = x xx -> [x] -> [x] forall a. a -> [a] -> [a] :[x] xs project :: [x] -> ListF x [x] project :: forall x. [x] -> ListF x [x] project [] = ListF x [x] forall x l. ListF x l Nil project (x x:[x] xs) = x -> [x] -> ListF x [x] forall x l. x -> l -> ListF x l Cons x x [x] xs embed' :: Star (ListF x) :.: Star (Const [x]) :~> Star (Const [x]) embed' :: forall {k1} x a (b :: k1). (:.:) (Star (ListF x)) (Star (Const [x])) a b -> Star (Const [x]) a b embed' (Star a ~> ListF x b f :.: Star b ~> Const [x] b g) = (a ~> Const [x] b) -> Star (Const [x]) a b forall {k1} {k2} (b :: k1) (a :: k2) (f :: k1 -> k2). Ob b => (a ~> f b) -> Star f a b Star ([x] -> Const [x] b forall {k} a (b :: k). a -> Const a b Const ([x] -> Const [x] b) -> (a -> [x]) -> a -> Const [x] 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 . ListF x [x] -> [x] forall x. ListF x [x] -> [x] embed (ListF x [x] -> [x]) -> (a -> ListF x [x]) -> a -> [x] 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 . (b ~> [x]) -> ListF x b ~> ListF x [x] forall a b. (a ~> b) -> ListF x a ~> ListF x b forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1). Functor f => (a ~> b) -> f a ~> f b map (Const [x] b -> [x] forall {k} a (b :: k). Const a b -> a getConst (Const [x] b -> [x]) -> (b -> Const [x] b) -> b -> [x] 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 . b ~> Const [x] b b -> Const [x] b g) (ListF x b -> ListF x [x]) -> (a -> ListF x b) -> a -> ListF x [x] 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 ~> ListF x b a -> ListF x b f) project' :: Star (Const [x]) :~> Star (ListF x) :.: Star (Const [x]) project' :: forall {k1} x a (b :: k1). Star (Const [x]) a b -> (:.:) (Star (ListF x)) (Star (Const [x])) a b project' (Star a ~> Const [x] b f) = (a ~> ListF x [x]) -> Star (ListF x) a [x] forall {k1} {k2} (b :: k1) (a :: k2) (f :: k1 -> k2). Ob b => (a ~> f b) -> Star f a b Star ([x] -> ListF x [x] forall x. [x] -> ListF x [x] project ([x] -> ListF x [x]) -> (a -> [x]) -> a -> ListF x [x] 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 . Const [x] b -> [x] forall {k} a (b :: k). Const a b -> a getConst (Const [x] b -> [x]) -> (a -> Const [x] b) -> a -> [x] 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 ~> Const [x] b a -> Const [x] b f) Star (ListF x) a [x] -> Star (Const [x]) [x] b -> (:.:) (Star (ListF x)) (Star (Const [x])) a b 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 :.: ([x] ~> Const [x] b) -> Star (Const [x]) [x] b forall {k1} {k2} (b :: k1) (a :: k2) (f :: k1 -> k2). Ob b => (a ~> f b) -> Star f a b Star [x] ~> Const [x] b [x] -> Const [x] b forall {k} a (b :: k). a -> Const a b Const toList :: Fix (Star (ListF x)) :~> Star (Const [x]) toList :: forall x a b. Fix (Star (ListF x)) a b -> Star (Const [x]) a b toList = ((Star (ListF x) :.: Star (Const [x])) :~> Star (Const [x])) -> Fix (Star (ListF x)) :~> Star (Const [x]) forall {k1} (p :: PRO k1 k1) (r :: PRO k1 k1). (Profunctor p, Profunctor r) => ((p :.: r) :~> r) -> Fix p :~> r cata (:.:) (Star (ListF x)) (Star (Const [x])) a b -> Star (Const [x]) a b (Star (ListF x) :.: Star (Const [x])) :~> Star (Const [x]) forall {k1} x a (b :: k1). (:.:) (Star (ListF x)) (Star (Const [x])) a b -> Star (Const [x]) a b embed' fromList :: Star (Const [x]) :~> Fix (Star (ListF x)) fromList :: forall x a b. Star (Const [x]) a b -> Fix (Star (ListF x)) a b fromList = (Star (Const [x]) :~> (Star (ListF x) :.: Star (Const [x]))) -> Star (Const [x]) :~> Fix (Star (ListF x)) forall {k1} (p :: PRO k1 k1) (r :: PRO k1 k1). (Profunctor p, Profunctor r) => (r :~> (p :.: r)) -> r :~> Fix p ana Star (Const [x]) a b -> (:.:) (Star (ListF x)) (Star (Const [x])) a b Star (Const [x]) :~> (Star (ListF x) :.: Star (Const [x])) forall {k1} x a (b :: k1). Star (Const [x]) a b -> (:.:) (Star (ListF x)) (Star (Const [x])) a b project'