module Proarrow.Profunctor.Fix where

import Data.Functor.Const (Const (..))

import Proarrow.Category.Instance.Nat (Nat (..))
import Proarrow.Category.Instance.Prof (Prof (..))
import Proarrow.Core (PRO, Profunctor (..), Promonad (..), (:~>))
import Proarrow.Functor (Functor (..))
import Proarrow.Profunctor.Composition ((:.:) (..))
import Proarrow.Profunctor.Star (Star (..))

type Fix :: PRO k k -> PRO k k
newtype Fix p a b where
  In :: {forall {i} (p :: PRO i i) (a :: i) (b :: i).
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 {i} (p :: PRO i i) (a :: i) (b :: i).
(:.:) 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 {i} (p :: PRO i i) (a :: i) (b :: i).
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 {k} {j} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof ((:.:) b (Fix b) a b -> Fix b a b
forall {i} (p :: PRO i i) (a :: i) (b :: i).
(:.:) 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
unProf (Nat ((:.:) a) ((:.:) b) -> (:.:) a .~> (:.:) b
forall {k} {k1} (f :: k -> k1) (g :: k -> k1). Nat f g -> f .~> g
unNat ((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 {i} (p :: PRO i i) (a :: i) (b :: i).
Fix p a b -> (:.:) p (Fix p) a b
out)

hylo :: (Profunctor p, Profunctor a, Profunctor b) => (p :.: b :~> b) -> (a :~> p :.: a) -> a :~> b
hylo :: forall {k} {k1} (p :: PRO k k) (a :: PRO k k1) (b :: PRO k k1).
(Profunctor p, Profunctor a, Profunctor b) =>
((p :.: b) :~> b) -> (a :~> (p :.: a)) -> a :~> b
hylo (p :.: b) :~> b
alg a :~> (p :.: a)
coalg = Prof a b -> a :~> b
forall {k} {k1} (p :: PRO k k1) (q :: PRO k k1).
Prof p q -> p :~> q
unProf Prof a b
go where go :: Prof a b
go = ((p :.: b) :~> b) -> Prof (p :.: b) b
forall {k} {j} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof (:.:) p b a b -> b a b
(p :.: b) :~> b
alg Prof (p :.: b) b -> Prof a (p :.: b) -> Prof a 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 :: k1 +-> k) (c :: k1 +-> k) (a :: k1 +-> k).
Prof b c -> Prof a b -> Prof a c
. (a ~> b) -> (p :.: a) ~> (p :.: b)
forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
forall (a :: k1 +-> k) (b :: k1 +-> k).
(a ~> b) -> (p :.: a) ~> (p :.: b)
map a ~> b
Prof a b
go Prof (p :.: a) (p :.: b) -> Prof a (p :.: a) -> Prof a (p :.: 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 :: k1 +-> k) (c :: k1 +-> k) (a :: k1 +-> k).
Prof b c -> Prof a b -> Prof a c
. (a :~> (p :.: a)) -> Prof a (p :.: a)
forall {k} {j} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof a a b -> (:.:) p a a b
a :~> (p :.: a)
coalg

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 = ((p :.: r) :~> r) -> (Fix p :~> (p :.: Fix p)) -> Fix p :~> r
forall {k} {k1} (p :: PRO k k) (a :: PRO k k1) (b :: PRO k k1).
(Profunctor p, Profunctor a, Profunctor b) =>
((p :.: b) :~> b) -> (a :~> (p :.: a)) -> a :~> b
hylo (:.:) p r a b -> r a b
(p :.: r) :~> r
alg Fix p a b -> (:.:) p (Fix p) a b
Fix p :~> (p :.: Fix p)
forall {i} (p :: PRO i i) (a :: i) (b :: i).
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 = ((p :.: Fix p) :~> Fix p) -> (r :~> (p :.: r)) -> r :~> Fix p
forall {k} {k1} (p :: PRO k k) (a :: PRO k k1) (b :: PRO k k1).
(Profunctor p, Profunctor a, Profunctor b) =>
((p :.: b) :~> b) -> (a :~> (p :.: a)) -> a :~> b
hylo (:.:) p (Fix p) a b -> Fix p a b
(p :.: Fix p) :~> Fix p
forall {i} (p :: PRO i i) (a :: i) (b :: i).
(:.:) p (Fix p) a b -> Fix p a b
In 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
x x -> [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 {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
:.: ([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'