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

module Proarrow.Profunctor.Cofree where

import Data.Kind (Constraint)
import Prelude (Int, fst, snd)

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 (..), trivialRep)
import Proarrow.Profunctor.Costar (Costar, pattern Costar)

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 :: k +-> 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 :: k +-> 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 :: k +-> 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
  trivialRep :: forall (a :: k).
Ob a =>
Corep (Forget ob) (Corep (Forget ob) % a) a
trivialRep @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} (f :: j +-> k) (a :: j) (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

class Test a where
  test :: a -> Int
instance HasCofree Test where
  type Cofree Test a = (Int, a)
  lower :: forall a. Ob a => Cofree Test a ~> a
lower = Cofree Test a ~> a
(Int, a) -> a
forall a b. (a, b) -> b
snd
  unfoldMap :: forall a b. Test a => (a ~> b) -> a ~> Cofree Test b
unfoldMap a ~> b
f a
a = (a -> Int
forall a. Test a => a -> Int
test a
a, a ~> b
a -> b
f a
a)
instance Promonad (Costar ((,) Int)) where
  id :: forall a. Ob a => Costar ((,) Int) a a
id = ((Int, a) ~> a) -> Costar ((,) Int) a a
forall {j} {k} (a :: j) (f :: j -> k) (b :: k).
Ob a =>
(f a ~> b) -> Costar f a b
Costar (forall {k} (ob :: OB k) (a :: k).
(HasCofree ob, Ob a) =>
Cofree ob a ~> a
forall (ob :: OB Type) a. (HasCofree ob, Ob a) => Cofree ob a ~> a
lower @Test)
  Costar (Int, b) ~> c
l . :: forall b c a.
Costar ((,) Int) b c
-> Costar ((,) Int) a b -> Costar ((,) Int) a c
. Costar (Int, a) ~> b
r = ((Int, a) ~> c) -> Costar ((,) Int) a c
forall {j} {k} (a :: j) (f :: j -> k) (b :: k).
Ob a =>
(f a ~> b) -> Costar f a b
Costar (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
forall (ob :: OB Type) a b c.
(HasCofree ob, Ob a) =>
(Cofree ob b ~> c) -> (Cofree ob a ~> b) -> Cofree ob a ~> c
cofreeComp @Test (Int, b) ~> c
Cofree Test b ~> c
l (Int, a) ~> b
Cofree Test a ~> b
r)
instance Test (Int, a) where
  test :: (Int, a) -> Int
test = (Int, a) -> Int
forall a b. (a, b) -> a
fst