{-# 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