{-# LANGUAGE AllowAmbiguousTypes #-}
{-# OPTIONS_GHC -Wno-orphans #-}

-- | Cofree constructions, dual to "Proarrow.Profunctor.Free": 'HasCofree' captures the object constraints
-- @ob@ whose forgetful functor has a right adjoint, with @Cofree ob@ the cofree object, 'lower' the counit
-- and 'unfoldMap' the universal property.
module Proarrow.Profunctor.Cofree where

import Data.Kind (Constraint)

import Proarrow.Category.Instance.Sub (Forget, SUBCAT (..), Sub (..))
import Proarrow.Core (CategoryOf (..), OB, Profunctor (..), Promonad (..))
import Proarrow.Profunctor.Corepresentable (Corep (..))
import Proarrow.Profunctor.Representable (Representable (..), repUniv)

type HasCofree :: forall {k}. OB k -> Constraint
class (CategoryOf k, forall a. (Ob a) => ob (Cofree ob a)) => HasCofree (ob :: k -> Constraint) where
  type Cofree ob (a :: k) :: k
  lower :: (Ob a) => Cofree ob a ~> a
  unfoldMap :: (ob a) => a ~> b -> a ~> Cofree ob b

section :: forall ob a. (HasCofree ob, ob a, Ob a) => a ~> Cofree ob a
section :: forall {k} (ob :: OB k) (a :: k).
(HasCofree ob, ob a, Ob a) =>
a ~> Cofree ob a
section = forall {k} (ob :: OB k) (a :: k) (b :: k).
(HasCofree ob, ob a) =>
(a ~> b) -> a ~> Cofree ob b
forall (ob :: OB k) (a :: k) (b :: k).
(HasCofree ob, ob a) =>
(a ~> b) -> a ~> Cofree ob b
unfoldMap @ob a ~> a
forall (a :: k). Ob a => a ~> a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id

cofreeMap :: (HasCofree ob) => (a ~> b) -> Cofree ob a ~> Cofree ob b
cofreeMap :: forall {k} (ob :: OB k) (a :: k) (b :: k).
HasCofree ob =>
(a ~> b) -> Cofree ob a ~> Cofree ob b
cofreeMap @ob a ~> b
f = forall {k} (ob :: OB k) (a :: k) (b :: k).
(HasCofree ob, ob a) =>
(a ~> b) -> a ~> Cofree ob b
forall (ob :: OB k) (a :: k) (b :: k).
(HasCofree ob, ob a) =>
(a ~> b) -> a ~> Cofree ob b
unfoldMap @ob (a ~> b
f (a ~> b) -> (Cofree ob a ~> a) -> Cofree ob a ~> b
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall {k} (ob :: OB k) (a :: k).
(HasCofree ob, Ob a) =>
Cofree ob a ~> a
forall (ob :: OB k) (a :: k).
(HasCofree ob, Ob a) =>
Cofree ob a ~> a
lower @ob) ((Ob a, Ob b) => Cofree ob a ~> Cofree ob b)
-> (a ~> b) -> Cofree ob a ~> Cofree ob 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
\\ a ~> b
f

cofreeComp :: (HasCofree ob, Ob a) => Cofree ob b ~> c -> Cofree ob a ~> b -> Cofree ob a ~> c
cofreeComp :: forall {k} (ob :: OB k) (a :: k) (b :: k) (c :: k).
(HasCofree ob, Ob a) =>
(Cofree ob b ~> c) -> (Cofree ob a ~> b) -> Cofree ob a ~> c
cofreeComp @ob Cofree ob b ~> c
l Cofree ob a ~> b
r = Cofree ob b ~> c
l (Cofree ob b ~> c)
-> (Cofree ob a ~> Cofree ob b) -> Cofree ob a ~> c
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall {k} (ob :: OB k) (a :: k) (b :: k).
(HasCofree ob, ob a) =>
(a ~> b) -> a ~> Cofree ob b
forall (ob :: OB k) (a :: k) (b :: k).
(HasCofree ob, ob a) =>
(a ~> b) -> a ~> Cofree ob b
unfoldMap @ob Cofree ob a ~> b
r

-- | By creating the right adjoint to the forgetful functor,
-- we obtain the forgetful-cofree adjunction.
instance (HasCofree ob) => Representable (Corep (Forget (ob :: OB k))) where
  type Corep (Forget ob) % a = SUB (Cofree ob a)
  index :: forall (a :: SUBCAT ob) (b :: k).
Corep (Forget ob) a b -> a ~> (Corep (Forget ob) % b)
index (Corep (Forget ob @ a) ~> b
f) = (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 {k} (ob :: OB k) (a :: k) (b :: k).
(HasCofree ob, ob a) =>
(a ~> b) -> a ~> Cofree ob b
forall (ob :: OB k) (a :: k) (b :: k).
(HasCofree ob, ob a) =>
(a ~> b) -> a ~> Cofree ob b
unfoldMap @ob UN SUB a ~> b
(Forget ob @ a) ~> b
f) ((Ob (UN SUB a), Ob b) =>
 Sub (~>) (SUB (UN SUB a)) (SUB (Cofree ob b)))
-> (UN SUB a ~> b) -> Sub (~>) (SUB (UN SUB a)) (SUB (Cofree ob 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
(Forget ob @ a) ~> b
f
  repUniv :: forall (a :: k).
Ob a =>
Corep (Forget ob) (Corep (Forget ob) % a) a
repUniv @a = let f :: Cofree ob a ~> a
f = forall {k} (ob :: OB k) (a :: k).
(HasCofree ob, Ob a) =>
Cofree ob a ~> a
forall (ob :: OB k) (a :: k).
(HasCofree ob, Ob a) =>
Cofree ob a ~> a
lower @ob @a in ((Forget ob @ SUB (Cofree ob a)) ~> a)
-> Corep (Forget ob) (SUB (Cofree ob a)) a
forall {j} {k} (a :: j) (f :: j +-> k) (b :: k).
Ob a =>
((f @ a) ~> b) -> Corep f a b
Corep (Forget ob @ SUB (Cofree ob a)) ~> a
Cofree ob a ~> a
f ((Ob (Cofree ob a), Ob a) =>
 Corep (Forget ob) (SUB (Cofree ob a)) a)
-> (Cofree ob a ~> a) -> Corep (Forget ob) (SUB (Cofree ob a)) a
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
\\ Cofree ob a ~> a
f