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

module Proarrow.Promonad
  ( Promonad (..)
  , Procomonad (..)
  , Monad
  , return
  , bind
  , Comonad
  , extract
  , extend
  , 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 (..))

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

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

type Monad m = (Promonad m, Representable m)

return :: forall m a. (Monad m, Ob a) => a ~> m % a
return :: forall {j} (m :: j +-> 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 :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id

bind :: forall m b a. (Monad m, Ob b) => a ~> m % b -> m % a ~> m % b
bind :: forall {j} (m :: j +-> 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 :: k +-> 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))

type Comonad w = (Promonad w, Corepresentable w)

extract :: forall w a. (Comonad w, Ob a) => w %% a ~> a
extract :: forall {k} (w :: k +-> 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 :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id

extend :: forall w a b. (Comonad w, Ob a) => w %% a ~> b -> w %% a ~> w %% b
extend :: forall {j} (w :: j +-> 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 :: k +-> 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

instance (Monad m) => RelativeMonad Id m where
  relReturn :: forall (a :: i). Ob a => Id a (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 :: j +-> j) (a :: j). (Monad m, Ob a) => a ~> (m % a)
forall (m :: i +-> i) (a :: i). (Monad m, Ob a) => a ~> (m % a)
return @m)
  relBind :: forall (b :: i) (a :: i).
Ob b =>
Id a (m % b) -> (m % a) ~> (m % b)
relBind @b (Id a ~> (m % b)
f) = forall {j} (m :: j +-> j) (b :: j) (a :: j).
(Monad m, Ob b) =>
(a ~> (m % b)) -> (m % a) ~> (m % b)
forall (m :: i +-> i) (b :: i) (a :: i).
(Monad m, Ob b) =>
(a ~> (m % b)) -> (m % a) ~> (m % b)
bind @m @b a ~> (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 w where
  relExtract :: forall (a :: i). Ob a => Id (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 :: k +-> k) (a :: k).
(Comonad w, Ob a) =>
(w %% a) ~> a
forall (w :: i +-> i) (a :: i). (Comonad w, Ob a) => (w %% a) ~> a
extract @w)
  relExtend :: forall (a :: i) (b :: i).
Ob a =>
Id (w %% a) b -> (w %% a) ~> (w %% b)
relExtend @a (Id (w %% a) ~> b
f) = forall {j} (w :: j +-> j) (a :: j) (b :: j).
(Comonad w, Ob a) =>
((w %% a) ~> b) -> (w %% a) ~> (w %% b)
forall (w :: i +-> i) (a :: i) (b :: i).
(Comonad w, Ob a) =>
((w %% a) ~> b) -> (w %% a) ~> (w %% b)
extend @w @a (w %% a) ~> b
f