{-# LANGUAGE AllowAmbiguousTypes #-}

module Proarrow.Profunctor.Cofree where

import Data.Kind (Constraint)
import Prelude (Int)

import Proarrow.Category.Instance.Sub (SUBCAT (..), Sub (..))
import Proarrow.Core (CategoryOf (..), OB, Profunctor (..), Promonad (..), UN, type (+->))
import Proarrow.Functor (FunctorForRep (..))
import Proarrow.Profunctor.Corepresentable (Corepresentable (..))
import Proarrow.Profunctor.Representable (Rep (..), Representable (..), trivialRep)
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 Cofree ob (Cofree ob % a) a
forall {j} {k} (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
p (p % a) a
trivialRep

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 :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id)

data family CofreeSub :: forall (ob :: OB k) -> k +-> SUBCAT ob
instance (HasCofree ob) => FunctorForRep (CofreeSub ob) where
  type CofreeSub ob @ a = SUB (Cofree ob % a)
  fmap :: forall (a :: j) (b :: j).
(a ~> b) -> (CofreeSub ob @ a) ~> (CofreeSub ob @ b)
fmap 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 :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a ~> b
f
instance (HasCofree ob) => Corepresentable (Rep (CofreeSub (ob :: OB k))) where
  type Rep (CofreeSub ob) %% a = UN SUB a
  coindex :: forall (a :: SUBCAT ob) (b :: k).
Rep (CofreeSub ob) a b -> (Rep (CofreeSub ob) %% a) ~> b
coindex (Rep (Sub a1 ~> b1
f)) = forall {k} (ob :: k -> Constraint) (a :: k).
(HasCofree ob, Ob a) =>
(Cofree ob % a) ~> a
forall (ob :: k -> Constraint) (a :: k).
(HasCofree ob, Ob a) =>
(Cofree ob % a) ~> a
lower @ob (b1 ~> b) -> (a1 ~> b1) -> a1 ~> b
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a1 ~> b1
f
  cotabulate :: forall (a :: SUBCAT ob) (b :: k).
Ob a =>
((Rep (CofreeSub ob) %% a) ~> b) -> Rep (CofreeSub ob) a b
cotabulate (Rep (CofreeSub ob) %% a) ~> b
f = (a ~> (CofreeSub ob @ b)) -> Rep (CofreeSub ob) a b
forall {j} {k} (f :: j +-> k) (a :: k) (b :: j).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep ((UN SUB a ~> (Cofree ob % b))
-> Sub (~>) (SUB (UN 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 (forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: k +-> k) (a :: k) (b :: k).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @(Cofree ob) UN SUB a ~> b
(Rep (CofreeSub ob) %% a) ~> b
f ((Cofree ob % UN SUB a) ~> (Cofree ob % b))
-> (UN SUB a ~> (Cofree ob % UN SUB a))
-> UN SUB a ~> (Cofree ob % b)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall {j} (ob :: j -> Constraint) (a :: j).
(HasCofree ob, ob a, Ob a) =>
a ~> (Cofree ob % a)
forall (ob :: k -> Constraint) (a :: k).
(HasCofree ob, ob a, Ob a) =>
a ~> (Cofree ob % a)
section @ob)) ((Ob (UN SUB a), Ob b) => Rep (CofreeSub ob) a b)
-> (UN SUB a ~> b) -> Rep (CofreeSub ob) a b
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ UN SUB a ~> b
(Rep (CofreeSub ob) %% a) ~> b
f
  corepMap :: forall (a :: SUBCAT ob) (b :: SUBCAT ob).
(a ~> b) -> (Rep (CofreeSub ob) %% a) ~> (Rep (CofreeSub ob) %% b)
corepMap (Sub a1 ~> b1
f) = a1 ~> b1
(Rep (CofreeSub ob) %% a) ~> (Rep (CofreeSub ob) %% b)
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