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

-- the identity laws compose with id on purpose
{- HLINT ignore "Redundant id" -}

-- | Promonads as effects: a 'Promonad' ("Proarrow.Core") that is 'Representable' is an ordinary 'Monad'
-- on objects ('return', 'bind'); a 'Promonad' that is 'Corepresentable' is a 'Comonad' ('extract',
-- 'extend'). Also 'Procomonad's and relative (co)monads ('RelativeMonad', 'RelativeComonad'). Concrete
-- promonads live in @Proarrow.Promonad.*@.
module Proarrow.Promonad
  ( Promonad (..)
  , Procomonad (..)
  , Monad
  , return
  , bind
  , Comonad
  , extract
  , extend
  , AsRelative (..)
  , RelativeMonad (..)
  , RelAlgebra
  , RelativeComonad (..)
  , RelCoalgebra
  ) where

import Data.Kind (Constraint)

import Proarrow.Core (CAT, CategoryOf (..), Profunctor (..), Promonad (..), src, (:~>), type (+->), type (~>))
import Proarrow.Profunctor.Corepresentable (Corepresentable (..))
import Proarrow.Profunctor.Instance.Composition ((:.:) (..))
import Proarrow.Profunctor.Instance.Identity (Id (..))
import Proarrow.Profunctor.Representable (Representable (..))
import Proarrow.Tools.Laws (ProLaw (..), ProLaws (..), (=:=), (===))

type Procomonad :: k +-> k -> Constraint
class (Profunctor p) => Procomonad p where
  proextract :: p :~> (~>)
  produplicate :: p :~> p :.: p

-- | 'id' is a unit for composition, which is associative, and both are natural. Elements that
-- start where another one ends are made from the drawn ones with 'lmap' and an arbitrary arrow.
instance ProLaws Promonad where
  proLaws :: [ProLaw Promonad]
proLaws =
    [ String -> ProLawBody Promonad -> ProLaw Promonad
forall {j} {k} (c :: (j +-> k) -> Constraint).
String -> ProLawBody c -> ProLaw c
ProLaw String
"left identity" \p a b
p forall (x :: j) (y :: j). (Ob x, Ob y) => String -> m (x ~> y)
_ forall (x :: j) (y :: j). (Ob x, Ob y) => String -> m (x ~> y)
_ -> p a b
p p a b -> p a b -> m (ProEquation p)
forall {j} {k} (m :: Type -> Type) (p :: j +-> k) (a :: k)
       (b :: j).
Applicative m =>
p a b -> p a b -> m (ProEquation p)
=:= p b b
forall (a :: j). Ob a => p a a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id p b b -> p a b -> p a b
forall (b :: j) (c :: j) (a :: j). p b c -> p a b -> p a c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. p a b
p
    , String -> ProLawBody Promonad -> ProLaw Promonad
forall {j} {k} (c :: (j +-> k) -> Constraint).
String -> ProLawBody c -> ProLaw c
ProLaw String
"right identity" \p a b
p forall (x :: j) (y :: j). (Ob x, Ob y) => String -> m (x ~> y)
_ forall (x :: j) (y :: j). (Ob x, Ob y) => String -> m (x ~> y)
_ -> p a b
p p a b -> p a b -> m (ProEquation p)
forall {j} {k} (m :: Type -> Type) (p :: j +-> k) (a :: k)
       (b :: j).
Applicative m =>
p a b -> p a b -> m (ProEquation p)
=:= p a b
p p a b -> p a a -> p a b
forall (b :: j) (c :: j) (a :: j). p b c -> p a b -> p a c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. p a a
forall (a :: j). Ob a => p a a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id
    , String -> ProLawBody3 Promonad -> ProLaw Promonad
forall {j} {k} (c :: (j +-> k) -> Constraint).
String -> ProLawBody3 c -> ProLaw c
ProLaw3 String
"associativity" \ @_ @_ @b @c @d @e p a b
p p c d
p' p e f
p'' forall (x :: j) (y :: j). (Ob x, Ob y) => String -> m (x ~> y)
mor forall (x :: j) (y :: j). (Ob x, Ob y) => String -> m (x ~> y)
_ -> do
        g <- forall (x :: j) (y :: j). (Ob x, Ob y) => String -> m (x ~> y)
mor @b @c String
"g"
        h <- mor @d @e "h"
        let q = (b ~> c) -> p c d -> p b d
forall (c :: j) (a :: j) (b :: j). (c ~> a) -> p a b -> p c b
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j).
Profunctor p =>
(c ~> a) -> p a b -> p c b
lmap b ~> c
g p c d
p'
            r = (d ~> e) -> p e f -> p d f
forall (c :: j) (a :: j) (b :: j). (c ~> a) -> p a b -> p c b
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j).
Profunctor p =>
(c ~> a) -> p a b -> p c b
lmap d ~> e
h p e f
p''
        r . (q . p) =:= (r . q) . p
    , String -> ProLawBody Promonad -> ProLaw Promonad
forall {j} {k} (c :: (j +-> k) -> Constraint).
String -> ProLawBody c -> ProLaw c
ProLaw String
"id dinaturality" \ @_ @a @_ @c p a b
_ forall (x :: j) (y :: j). (Ob x, Ob y) => String -> m (x ~> y)
mor forall (x :: j) (y :: j). (Ob x, Ob y) => String -> m (x ~> y)
_ -> do
        g <- forall (x :: j) (y :: j). (Ob x, Ob y) => String -> m (x ~> y)
mor @c @a String
"g"
        rmap g id =:= lmap g id
    , String -> ProLawBody3 Promonad -> ProLaw Promonad
forall {j} {k} (c :: (j +-> k) -> Constraint).
String -> ProLawBody3 c -> ProLaw c
ProLaw3 String
"composition naturality" \ @_ @a @b @c @d @e @f p a b
p p c d
p' p e f
_ forall (x :: j) (y :: j). (Ob x, Ob y) => String -> m (x ~> y)
mor forall (x :: j) (y :: j). (Ob x, Ob y) => String -> m (x ~> y)
_ -> do
        k <- forall (x :: j) (y :: j). (Ob x, Ob y) => String -> m (x ~> y)
mor @b @c String
"k"
        g <- mor @e @a "g"
        h <- mor @d @f "h"
        let q = (b ~> c) -> p c d -> p b d
forall (c :: j) (a :: j) (b :: j). (c ~> a) -> p a b -> p c b
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j).
Profunctor p =>
(c ~> a) -> p a b -> p c b
lmap b ~> c
k p c d
p'
        dimap g h (q . p) =:= rmap h q . lmap g p
    , String -> ProLawBody3 Promonad -> ProLaw Promonad
forall {j} {k} (c :: (j +-> k) -> Constraint).
String -> ProLawBody3 c -> ProLaw c
ProLaw3 String
"composition dinaturality" \ @_ @_ @b @c p a b
p p c d
p' p e f
_ forall (x :: j) (y :: j). (Ob x, Ob y) => String -> m (x ~> y)
mor forall (x :: j) (y :: j). (Ob x, Ob y) => String -> m (x ~> y)
_ -> do
        g <- forall (x :: j) (y :: j). (Ob x, Ob y) => String -> m (x ~> y)
mor @b @c String
"g"
        p' . rmap g p =:= lmap g p' . p
    ]

-- | 'proextract' is natural, and extracting either half of 'produplicate' gives back the element.
-- Coassociativity is not an equation between elements: its two sides are composites whose middle
-- objects cannot be compared.
instance ProLaws Procomonad where
  proLaws :: [ProLaw Procomonad]
proLaws =
    [ String -> ProLawBody Procomonad -> ProLaw Procomonad
forall {j} {k} (c :: (j +-> k) -> Constraint).
String -> ProLawBody c -> ProLaw c
ProLaw String
"proextract naturality" \ @_ @a @b @c @d p a b
p forall (x :: j) (y :: j). (Ob x, Ob y) => String -> m (x ~> y)
morK forall (x :: j) (y :: j). (Ob x, Ob y) => String -> m (x ~> y)
morJ -> do
        g <- forall (x :: j) (y :: j). (Ob x, Ob y) => String -> m (x ~> y)
morK @c @a String
"g"
        h <- morJ @b @d "h"
        proextract (dimap g h p) === h . proextract p . g
    , String -> ProLawBody Procomonad -> ProLaw Procomonad
forall {j} {k} (c :: (j +-> k) -> Constraint).
String -> ProLawBody c -> ProLaw c
ProLaw String
"left counit" \p a b
p forall (x :: j) (y :: j). (Ob x, Ob y) => String -> m (x ~> y)
_ forall (x :: j) (y :: j). (Ob x, Ob y) => String -> m (x ~> y)
_ -> case p a b -> (:.:) p p a b
p :~> (p :.: p)
forall k (p :: k +-> k). Procomonad p => p :~> (p :.: p)
produplicate p a b
p of p a b
q :.: p b b
r -> p a b
p p a b -> p a b -> m (ProEquation p)
forall {j} {k} (m :: Type -> Type) (p :: j +-> k) (a :: k)
       (b :: j).
Applicative m =>
p a b -> p a b -> m (ProEquation p)
=:= (a ~> b) -> p b b -> p a b
forall (c :: j) (a :: j) (b :: j). (c ~> a) -> p a b -> p c b
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j).
Profunctor p =>
(c ~> a) -> p a b -> p c b
lmap (p a b -> a ~> b
p :~> (~>)
forall k (p :: k +-> k). Procomonad p => p :~> (~>)
proextract p a b
q) p b b
r
    , String -> ProLawBody Procomonad -> ProLaw Procomonad
forall {j} {k} (c :: (j +-> k) -> Constraint).
String -> ProLawBody c -> ProLaw c
ProLaw String
"right counit" \p a b
p forall (x :: j) (y :: j). (Ob x, Ob y) => String -> m (x ~> y)
_ forall (x :: j) (y :: j). (Ob x, Ob y) => String -> m (x ~> y)
_ -> case p a b -> (:.:) p p a b
p :~> (p :.: p)
forall k (p :: k +-> k). Procomonad p => p :~> (p :.: p)
produplicate p a b
p of p a b
q :.: p b b
r -> p a b
p p a b -> p a b -> m (ProEquation p)
forall {j} {k} (m :: Type -> Type) (p :: j +-> k) (a :: k)
       (b :: j).
Applicative m =>
p a b -> p a b -> m (ProEquation p)
=:= (b ~> b) -> p a b -> p a b
forall (b :: j) (d :: j) (a :: j). (b ~> d) -> p a b -> p a d
forall {j} {k} (p :: j +-> k) (b :: j) (d :: j) (a :: k).
Profunctor p =>
(b ~> d) -> p a b -> p a d
rmap (p b b -> b ~> b
p :~> (~>)
forall k (p :: k +-> k). Procomonad p => p :~> (~>)
proextract p b b
r) p a b
q
    ]

instance (CategoryOf k) => Procomonad (Id :: CAT k) where
  proextract :: Id :~> (~>)
proextract (Id a ~> b
f) = a ~> b
f
  produplicate :: Id :~> (Id :.: Id)
produplicate (Id a ~> b
f) = (a ~> a) -> Id a a
forall k (a :: k) (b :: k). (a ~> b) -> Id a b
Id ((a ~> b) -> a ~> a
forall {j} {k} (a :: k) (b :: j) (p :: j +-> k).
Profunctor p =>
p a b -> Obj a
src a ~> b
f) Id a a -> Id a b -> (:.:) Id Id a b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: (a ~> b) -> Id a b
forall k (a :: k) (b :: k). (a ~> b) -> Id a b
Id a ~> b
f

-- | A representable promonad is a monad on objects: it acts as the functor @m '%' -@, with
-- 'return' and 'bind'.
type Monad m = (Promonad m, Representable m)

-- | The unit of the monad @m@.
return :: forall m a. (Monad m, Ob a) => a ~> m % a
return :: forall {j} (m :: CAT j) (a :: j). (Monad m, Ob a) => a ~> (m % a)
return = 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 @m m a a
forall (a :: j). Ob a => m a a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id

-- | Kleisli extension: run a Kleisli arrow under @m@.
bind :: forall m b a. (Monad m, Ob b) => a ~> m % b -> m % a ~> m % b
bind :: forall {j} (m :: CAT j) (b :: j) (a :: j).
(Monad m, Ob b) =>
(a ~> (m % b)) -> (m % a) ~> (m % b)
bind a ~> (m % b)
f = m (m % a) b -> (m % a) ~> (m % b)
forall (a :: j) (b :: j). m a b -> a ~> (m % b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
index (forall {j} {k} (p :: j +-> k) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
forall (p :: j +-> j) (b :: j) (a :: j).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
tabulate @m @b a ~> (m % b)
f m a b -> m (m % a) a -> m (m % a) b
forall (b :: j) (c :: j) (a :: j). m b c -> m a b -> m a c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (m (m % a) a
(Ob a, Ob (m % b)) => m (m % a) a
forall (a :: j). Ob a => m (m % a) a
forall {j} {k} (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
p (p % a) a
repUniv ((Ob a, Ob (m % b)) => m (m % a) a)
-> (a ~> (m % b)) -> m (m % a) a
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 ~> (m % b)
f))

-- | Dually, a corepresentable promonad is a comonad on objects, acting as @w '%%' -@, with
-- 'extract' and 'extend'.
type Comonad w = (Promonad w, Corepresentable w)

-- | The counit of the comonad @w@.
extract :: forall w a. (Comonad w, Ob a) => w %% a ~> a
extract :: forall {k} (w :: CAT k) (a :: k).
(Comonad w, Ob a) =>
(w %% a) ~> a
extract = forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Corepresentable p =>
p a b -> (p %% a) ~> b
forall (p :: k +-> k) (a :: k) (b :: k).
Corepresentable p =>
p a b -> (p %% a) ~> b
coindex @w w a a
forall (a :: k). Ob a => w a a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id

-- | CoKleisli extension: run a coKleisli arrow under @w@.
extend :: forall w a b. (Comonad w, Ob a) => w %% a ~> b -> w %% a ~> w %% b
extend :: forall {j} (w :: CAT j) (a :: j) (b :: j).
(Comonad w, Ob a) =>
((w %% a) ~> b) -> (w %% a) ~> (w %% b)
extend (w %% a) ~> b
f = w a (w %% b) -> (w %% a) ~> (w %% b)
forall (a :: j) (b :: j). w a b -> (w %% a) ~> b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Corepresentable p =>
p a b -> (p %% a) ~> b
coindex ((w b (w %% b)
(Ob (w %% a), Ob b) => w b (w %% b)
forall (a :: j). Ob a => w a (w %% a)
forall {j} {k} (p :: j +-> k) (a :: k).
(Corepresentable p, Ob a) =>
p a (p %% a)
corepUniv ((Ob (w %% a), Ob b) => w b (w %% b))
-> ((w %% a) ~> b) -> w b (w %% 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
\\ (w %% a) ~> b
f) w b (w %% b) -> w a b -> w a (w %% b)
forall (b :: j) (c :: j) (a :: j). w b c -> w a b -> w 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 {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Corepresentable p, Ob a) =>
((p %% a) ~> b) -> p a b
forall (p :: j +-> j) (a :: j) (b :: j).
(Corepresentable p, Ob a) =>
((p %% a) ~> b) -> p a b
cotabulate @w @a (w %% a) ~> b
f)

type RelativeMonad :: i +-> k -> k +-> i -> Constraint
class (Representable m, Profunctor j) => RelativeMonad j m where
  relReturn :: (Ob a) => j a (m % a)
  relBind :: (Ob b) => j a (m % b) -> m % a ~> m % b

type RelAlgebra j m a b = j a b -> m % a ~> b

-- | A 'Monad' or 'Comonad' seen as a relative (co)monad along 'Id'.
--
-- The wrapper is needed: a direct @'RelativeMonad' 'Id' m@ instance would unify at @j = 'Id'@ with
-- carrier-specific ones such as the codensity monad's, with neither more specific, so no overlap
-- pragma could order them.
type AsRelative :: (k +-> i) -> k +-> i
newtype AsRelative m a b = AsRelative {forall k i (m :: k +-> i) (a :: i) (b :: k).
AsRelative m a b -> m a b
unAsRelative :: m a b}
  deriving newtype (CategoryOf j
CategoryOf k
(CategoryOf j, CategoryOf k) =>
(forall (c :: k) (a :: k) (b :: j) (d :: j).
 (c ~> a) -> (b ~> d) -> AsRelative m a b -> AsRelative m c d)
-> (forall (c :: k) (a :: k) (b :: j).
    (c ~> a) -> AsRelative m a b -> AsRelative m c b)
-> (forall (b :: j) (d :: j) (a :: k).
    (b ~> d) -> AsRelative m a b -> AsRelative m a d)
-> (forall (a :: k) (b :: j) r.
    ((Ob a, Ob b) => r) -> AsRelative m a b -> r)
-> Profunctor (AsRelative m)
forall (b :: j) (d :: j) (a :: k).
(b ~> d) -> AsRelative m a b -> AsRelative m a d
forall (a :: k) (b :: j) r.
((Ob a, Ob b) => r) -> AsRelative m a b -> r
forall (c :: k) (a :: k) (b :: j).
(c ~> a) -> AsRelative m a b -> AsRelative m c b
forall (c :: k) (a :: k) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> AsRelative m a b -> AsRelative m c d
forall {j} {k} (p :: j +-> k).
(CategoryOf j, CategoryOf k) =>
(forall (c :: k) (a :: k) (b :: j) (d :: j).
 (c ~> a) -> (b ~> d) -> p a b -> p c d)
-> (forall (c :: k) (a :: k) (b :: j). (c ~> a) -> p a b -> p c b)
-> (forall (b :: j) (d :: j) (a :: k). (b ~> d) -> p a b -> p a d)
-> (forall (a :: k) (b :: j) r. ((Ob a, Ob b) => r) -> p a b -> r)
-> Profunctor p
forall {j} {k} (p :: j +-> k). Profunctor p => CategoryOf j
forall j k (m :: j +-> k). Profunctor m => CategoryOf k
forall j k (m :: j +-> k) (b :: j) (d :: j) (a :: k).
Profunctor m =>
(b ~> d) -> AsRelative m a b -> AsRelative m a d
forall j k (m :: j +-> k) (a :: k) (b :: j) r.
Profunctor m =>
((Ob a, Ob b) => r) -> AsRelative m a b -> r
forall j k (m :: j +-> k) (c :: k) (a :: k) (b :: j).
Profunctor m =>
(c ~> a) -> AsRelative m a b -> AsRelative m c b
forall j k (m :: j +-> k) (c :: k) (a :: k) (b :: j) (d :: j).
Profunctor m =>
(c ~> a) -> (b ~> d) -> AsRelative m a b -> AsRelative m c d
$cdimap :: forall j k (m :: j +-> k) (c :: k) (a :: k) (b :: j) (d :: j).
Profunctor m =>
(c ~> a) -> (b ~> d) -> AsRelative m a b -> AsRelative m c d
dimap :: forall (c :: k) (a :: k) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> AsRelative m a b -> AsRelative m c d
$clmap :: forall j k (m :: j +-> k) (c :: k) (a :: k) (b :: j).
Profunctor m =>
(c ~> a) -> AsRelative m a b -> AsRelative m c b
lmap :: forall (c :: k) (a :: k) (b :: j).
(c ~> a) -> AsRelative m a b -> AsRelative m c b
$crmap :: forall j k (m :: j +-> k) (b :: j) (d :: j) (a :: k).
Profunctor m =>
(b ~> d) -> AsRelative m a b -> AsRelative m a d
rmap :: forall (b :: j) (d :: j) (a :: k).
(b ~> d) -> AsRelative m a b -> AsRelative m a d
$c\\ :: forall j k (m :: j +-> k) (a :: k) (b :: j) r.
Profunctor m =>
((Ob a, Ob b) => r) -> AsRelative m a b -> r
\\ :: forall (a :: k) (b :: j) r.
((Ob a, Ob b) => r) -> AsRelative m a b -> r
Profunctor, Profunctor (AsRelative m)
Profunctor (AsRelative m) =>
(forall (a :: k). Ob a => AsRelative m a a)
-> (forall (b :: k) (c :: k) (a :: k).
    AsRelative m b c -> AsRelative m a b -> AsRelative m a c)
-> Promonad (AsRelative m)
forall (a :: k). Ob a => AsRelative m a a
forall (b :: k) (c :: k) (a :: k).
AsRelative m b c -> AsRelative m a b -> AsRelative m a c
forall {k} (p :: CAT k).
Profunctor p =>
(forall (a :: k). Ob a => p a a)
-> (forall (b :: k) (c :: k) (a :: k). p b c -> p a b -> p a c)
-> Promonad p
forall k (m :: k +-> k). Promonad m => Profunctor (AsRelative m)
forall k (m :: k +-> k) (a :: k).
(Promonad m, Ob a) =>
AsRelative m a a
forall k (m :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad m =>
AsRelative m b c -> AsRelative m a b -> AsRelative m a c
$cid :: forall k (m :: k +-> k) (a :: k).
(Promonad m, Ob a) =>
AsRelative m a a
id :: forall (a :: k). Ob a => AsRelative m a a
$c. :: forall k (m :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad m =>
AsRelative m b c -> AsRelative m a b -> AsRelative m a c
. :: forall (b :: k) (c :: k) (a :: k).
AsRelative m b c -> AsRelative m a b -> AsRelative m a c
Promonad, Profunctor (AsRelative m)
Profunctor (AsRelative m) =>
(forall (a :: k) (b :: j).
 AsRelative m a b -> a ~> (AsRelative m % b))
-> (forall (b :: j) (a :: k).
    Ob b =>
    (a ~> (AsRelative m % b)) -> AsRelative m a b)
-> (forall (a :: j) (b :: j).
    (a ~> b) -> (AsRelative m % a) ~> (AsRelative m % b))
-> (forall (a :: j). Ob a => AsRelative m (AsRelative m % a) a)
-> Representable (AsRelative m)
forall (a :: j). Ob a => AsRelative m (AsRelative m % a) a
forall (a :: j) (b :: j).
(a ~> b) -> (AsRelative m % a) ~> (AsRelative m % b)
forall (b :: j) (a :: k).
Ob b =>
(a ~> (AsRelative m % b)) -> AsRelative m a b
forall (a :: k) (b :: j).
AsRelative m a b -> a ~> (AsRelative m % b)
forall {j} {k} (p :: j +-> k).
Profunctor p =>
(forall (a :: k) (b :: j). p a b -> a ~> (p % b))
-> (forall (b :: j) (a :: k). Ob b => (a ~> (p % b)) -> p a b)
-> (forall (a :: j) (b :: j). (a ~> b) -> (p % a) ~> (p % b))
-> (forall (a :: j). Ob a => p (p % a) a)
-> Representable p
forall j k (m :: j +-> k).
Representable m =>
Profunctor (AsRelative m)
forall j k (m :: j +-> k) (a :: j).
(Representable m, Ob a) =>
AsRelative m (AsRelative m % a) a
forall j k (m :: j +-> k) (a :: j) (b :: j).
Representable m =>
(a ~> b) -> (AsRelative m % a) ~> (AsRelative m % b)
forall j k (m :: j +-> k) (b :: j) (a :: k).
(Representable m, Ob b) =>
(a ~> (AsRelative m % b)) -> AsRelative m a b
forall j k (m :: j +-> k) (a :: k) (b :: j).
Representable m =>
AsRelative m a b -> a ~> (AsRelative m % b)
$cindex :: forall j k (m :: j +-> k) (a :: k) (b :: j).
Representable m =>
AsRelative m a b -> a ~> (AsRelative m % b)
index :: forall (a :: k) (b :: j).
AsRelative m a b -> a ~> (AsRelative m % b)
$ctabulate :: forall j k (m :: j +-> k) (b :: j) (a :: k).
(Representable m, Ob b) =>
(a ~> (AsRelative m % b)) -> AsRelative m a b
tabulate :: forall (b :: j) (a :: k).
Ob b =>
(a ~> (AsRelative m % b)) -> AsRelative m a b
$crepMap :: forall j k (m :: j +-> k) (a :: j) (b :: j).
Representable m =>
(a ~> b) -> (AsRelative m % a) ~> (AsRelative m % b)
repMap :: forall (a :: j) (b :: j).
(a ~> b) -> (AsRelative m % a) ~> (AsRelative m % b)
$crepUniv :: forall j k (m :: j +-> k) (a :: j).
(Representable m, Ob a) =>
AsRelative m (AsRelative m % a) a
repUniv :: forall (a :: j). Ob a => AsRelative m (AsRelative m % a) a
Representable, Profunctor (AsRelative m)
Profunctor (AsRelative m) =>
(forall (a :: k) (b :: j).
 AsRelative m a b -> (AsRelative m %% a) ~> b)
-> (forall (a :: k) (b :: j).
    Ob a =>
    ((AsRelative m %% a) ~> b) -> AsRelative m a b)
-> (forall (a :: k) (b :: k).
    (a ~> b) -> (AsRelative m %% a) ~> (AsRelative m %% b))
-> (forall (a :: k). Ob a => AsRelative m a (AsRelative m %% a))
-> Corepresentable (AsRelative m)
forall (a :: k). Ob a => AsRelative m a (AsRelative m %% a)
forall (a :: k) (b :: j).
Ob a =>
((AsRelative m %% a) ~> b) -> AsRelative m a b
forall (a :: k) (b :: j).
AsRelative m a b -> (AsRelative m %% a) ~> b
forall (a :: k) (b :: k).
(a ~> b) -> (AsRelative m %% a) ~> (AsRelative m %% b)
forall {j} {k} (p :: j +-> k).
Profunctor p =>
(forall (a :: k) (b :: j). p a b -> (p %% a) ~> b)
-> (forall (a :: k) (b :: j). Ob a => ((p %% a) ~> b) -> p a b)
-> (forall (a :: k) (b :: k). (a ~> b) -> (p %% a) ~> (p %% b))
-> (forall (a :: k). Ob a => p a (p %% a))
-> Corepresentable p
forall j k (m :: j +-> k).
Corepresentable m =>
Profunctor (AsRelative m)
forall j k (m :: j +-> k) (a :: k).
(Corepresentable m, Ob a) =>
AsRelative m a (AsRelative m %% a)
forall j k (m :: j +-> k) (a :: k) (b :: j).
(Corepresentable m, Ob a) =>
((AsRelative m %% a) ~> b) -> AsRelative m a b
forall j k (m :: j +-> k) (a :: k) (b :: j).
Corepresentable m =>
AsRelative m a b -> (AsRelative m %% a) ~> b
forall j k (m :: j +-> k) (a :: k) (b :: k).
Corepresentable m =>
(a ~> b) -> (AsRelative m %% a) ~> (AsRelative m %% b)
$ccoindex :: forall j k (m :: j +-> k) (a :: k) (b :: j).
Corepresentable m =>
AsRelative m a b -> (AsRelative m %% a) ~> b
coindex :: forall (a :: k) (b :: j).
AsRelative m a b -> (AsRelative m %% a) ~> b
$ccotabulate :: forall j k (m :: j +-> k) (a :: k) (b :: j).
(Corepresentable m, Ob a) =>
((AsRelative m %% a) ~> b) -> AsRelative m a b
cotabulate :: forall (a :: k) (b :: j).
Ob a =>
((AsRelative m %% a) ~> b) -> AsRelative m a b
$ccorepMap :: forall j k (m :: j +-> k) (a :: k) (b :: k).
Corepresentable m =>
(a ~> b) -> (AsRelative m %% a) ~> (AsRelative m %% b)
corepMap :: forall (a :: k) (b :: k).
(a ~> b) -> (AsRelative m %% a) ~> (AsRelative m %% b)
$ccorepUniv :: forall j k (m :: j +-> k) (a :: k).
(Corepresentable m, Ob a) =>
AsRelative m a (AsRelative m %% a)
corepUniv :: forall (a :: k). Ob a => AsRelative m a (AsRelative m %% a)
Corepresentable)

instance (Monad m) => RelativeMonad Id (AsRelative m) where
  relReturn :: forall (a :: i). Ob a => Id a (AsRelative m % a)
relReturn = (a ~> (m % a)) -> Id a (m % a)
forall k (a :: k) (b :: k). (a ~> b) -> Id a b
Id (forall {j} (m :: CAT j) (a :: j). (Monad m, Ob a) => a ~> (m % a)
forall (m :: CAT i) (a :: i). (Monad m, Ob a) => a ~> (m % a)
return @m)
  relBind :: forall (b :: i) (a :: i).
Ob b =>
Id a (AsRelative m % b) -> (AsRelative m % a) ~> (AsRelative m % b)
relBind @b (Id a ~> (AsRelative m % b)
f) = forall {j} (m :: CAT j) (b :: j) (a :: j).
(Monad m, Ob b) =>
(a ~> (m % b)) -> (m % a) ~> (m % b)
forall (m :: CAT i) (b :: i) (a :: i).
(Monad m, Ob b) =>
(a ~> (m % b)) -> (m % a) ~> (m % b)
bind @m @b a ~> (m % b)
a ~> (AsRelative m % b)
f

type RelativeComonad :: i +-> k -> k +-> i -> Constraint
class (Corepresentable w, Profunctor j) => RelativeComonad j w where
  relExtract :: (Ob a) => j (w %% a) a
  relExtend :: (Ob a) => j (w %% a) b -> w %% a ~> w %% b

type RelCoalgebra j w a b = j a b -> a ~> w %% b

instance (Comonad w) => RelativeComonad Id (AsRelative w) where
  relExtract :: forall (a :: i). Ob a => Id (AsRelative w %% a) a
relExtract = ((w %% a) ~> a) -> Id (w %% a) a
forall k (a :: k) (b :: k). (a ~> b) -> Id a b
Id (forall {k} (w :: CAT k) (a :: k).
(Comonad w, Ob a) =>
(w %% a) ~> a
forall (w :: CAT i) (a :: i). (Comonad w, Ob a) => (w %% a) ~> a
extract @w)
  relExtend :: forall (a :: i) (b :: i).
Ob a =>
Id (AsRelative w %% a) b
-> (AsRelative w %% a) ~> (AsRelative w %% b)
relExtend @a (Id (AsRelative w %% a) ~> b
f) = forall {j} (w :: CAT j) (a :: j) (b :: j).
(Comonad w, Ob a) =>
((w %% a) ~> b) -> (w %% a) ~> (w %% b)
forall (w :: CAT i) (a :: i) (b :: i).
(Comonad w, Ob a) =>
((w %% a) ~> b) -> (w %% a) ~> (w %% b)
extend @w @a (w %% a) ~> b
(AsRelative w %% a) ~> b
f