{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE StandaloneDeriving #-}
module FMonad.Adjoint(Adjoint, adjoint, runAdjoint, AdjointT(..), fffmap, generalize) where

import Control.Monad.Trans.Identity ( IdentityT(..) )

import FFunctor
import FMonad
import FStrong
import FFunctor.FCompose
import FFunctor.Adjunction

newtype AdjointT ff uu mm g x = AdjointT { forall {k} {k} {k} {k} (ff :: k -> k) (uu :: k -> k -> *)
       (mm :: k -> k) (g :: k) (x :: k).
AdjointT ff uu mm g x -> uu (mm (ff g)) x
runAdjointT :: uu (mm (ff g)) x }

type Adjoint ff uu = AdjointT ff uu IdentityT

deriving
  via FCompose (FCompose uu mm) ff g
    instance (FFunctor ff, FFunctor mm, FFunctor uu, Functor g) => Functor (AdjointT ff uu mm g)

deriving
  via FCompose (FCompose uu mm) ff
    instance (FFunctor ff, FFunctor mm, FFunctor uu) => FFunctor (AdjointT ff uu mm)

deriving
  via FCompose (FCompose uu mm) ff
    instance (FStrong ff, FStrong mm, FStrong uu) => FStrong (AdjointT ff uu mm)

instance (Adjunction ff uu, FMonad mm) => FMonad (AdjointT ff uu mm) where
    fpure :: forall (g :: FUNCTOR). Functor g => g ~> AdjointT ff uu mm g
fpure = uu (mm (ff g)) x -> AdjointT ff uu mm g x
forall {k} {k} {k} {k} (ff :: k -> k) (uu :: k -> k -> *)
       (mm :: k -> k) (g :: k) (x :: k).
uu (mm (ff g)) x -> AdjointT ff uu mm g x
AdjointT (uu (mm (ff g)) x -> AdjointT ff uu mm g x)
-> (g x -> uu (mm (ff g)) x) -> g x -> AdjointT ff uu mm g x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ff g ~> mm (ff g)) -> uu (ff g) x -> uu (mm (ff g)) x
forall (g :: FUNCTOR) (h :: FUNCTOR) x.
(Functor g, Functor h) =>
(g ~> h) -> uu g x -> uu h x
forall (ff :: FF) (g :: FUNCTOR) (h :: FUNCTOR) x.
(FFunctor ff, Functor g, Functor h) =>
(g ~> h) -> ff g x -> ff h x
ffmap ff g x -> mm (ff g) x
ff g ~> mm (ff g)
forall (g :: FUNCTOR). Functor g => g ~> mm g
forall (ff :: FF) (g :: FUNCTOR).
(FMonad ff, Functor g) =>
g ~> ff g
fpure (uu (ff g) x -> uu (mm (ff g)) x)
-> (g x -> uu (ff g) x) -> g x -> uu (mm (ff g)) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. g x -> uu (ff g) x
g ~> uu (ff g)
forall (g :: FUNCTOR). Functor g => g ~> uu (ff g)
forall (ff :: FF) (uu :: FF) (g :: FUNCTOR).
(Adjunction ff uu, Functor g) =>
g ~> uu (ff g)
unit
    fbind :: forall (g :: FUNCTOR) (h :: FUNCTOR) a.
(Functor g, Functor h) =>
(g ~> AdjointT ff uu mm h)
-> AdjointT ff uu mm g a -> AdjointT ff uu mm h a
fbind g ~> AdjointT ff uu mm h
k = uu (mm (ff h)) a -> AdjointT ff uu mm h a
forall {k} {k} {k} {k} (ff :: k -> k) (uu :: k -> k -> *)
       (mm :: k -> k) (g :: k) (x :: k).
uu (mm (ff g)) x -> AdjointT ff uu mm g x
AdjointT (uu (mm (ff h)) a -> AdjointT ff uu mm h a)
-> (AdjointT ff uu mm g a -> uu (mm (ff h)) a)
-> AdjointT ff uu mm g a
-> AdjointT ff uu mm h a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (mm (ff (uu (mm (ff h)))) ~> mm (ff h))
-> uu (mm (ff (uu (mm (ff h))))) a -> uu (mm (ff h)) a
forall (g :: FUNCTOR) (h :: FUNCTOR) x.
(Functor g, Functor h) =>
(g ~> h) -> uu g x -> uu h x
forall (ff :: FF) (g :: FUNCTOR) (h :: FUNCTOR) x.
(FFunctor ff, Functor g, Functor h) =>
(g ~> h) -> ff g x -> ff h x
ffmap ((ff (uu (mm (ff h))) ~> mm (ff h))
-> mm (ff (uu (mm (ff h)))) x -> mm (ff h) x
forall (g :: FUNCTOR) (h :: FUNCTOR) a.
(Functor g, Functor h) =>
(g ~> mm h) -> mm g a -> mm h a
forall (ff :: FF) (g :: FUNCTOR) (h :: FUNCTOR) a.
(FMonad ff, Functor g, Functor h) =>
(g ~> ff h) -> ff g a -> ff h a
fbind ff (uu (mm (ff h))) x -> mm (ff h) x
ff (uu (mm (ff h))) ~> mm (ff h)
forall (g :: FUNCTOR). Functor g => ff (uu g) ~> g
forall (ff :: FF) (uu :: FF) (g :: FUNCTOR).
(Adjunction ff uu, Functor g) =>
ff (uu g) ~> g
counit) (uu (mm (ff (uu (mm (ff h))))) a -> uu (mm (ff h)) a)
-> (AdjointT ff uu mm g a -> uu (mm (ff (uu (mm (ff h))))) a)
-> AdjointT ff uu mm g a
-> uu (mm (ff h)) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AdjointT ff uu mm (uu (mm (ff h))) a
-> uu (mm (ff (uu (mm (ff h))))) a
forall {k} {k} {k} {k} (ff :: k -> k) (uu :: k -> k -> *)
       (mm :: k -> k) (g :: k) (x :: k).
AdjointT ff uu mm g x -> uu (mm (ff g)) x
runAdjointT (AdjointT ff uu mm (uu (mm (ff h))) a
 -> uu (mm (ff (uu (mm (ff h))))) a)
-> (AdjointT ff uu mm g a -> AdjointT ff uu mm (uu (mm (ff h))) a)
-> AdjointT ff uu mm g a
-> uu (mm (ff (uu (mm (ff h))))) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (g ~> uu (mm (ff h)))
-> AdjointT ff uu mm g a -> AdjointT ff uu mm (uu (mm (ff h))) a
forall (g :: FUNCTOR) (h :: FUNCTOR) x.
(Functor g, Functor h) =>
(g ~> h) -> AdjointT ff uu mm g x -> AdjointT ff uu mm h x
forall (ff :: FF) (g :: FUNCTOR) (h :: FUNCTOR) x.
(FFunctor ff, Functor g, Functor h) =>
(g ~> h) -> ff g x -> ff h x
ffmap (AdjointT ff uu mm h x -> uu (mm (ff h)) x
forall {k} {k} {k} {k} (ff :: k -> k) (uu :: k -> k -> *)
       (mm :: k -> k) (g :: k) (x :: k).
AdjointT ff uu mm g x -> uu (mm (ff g)) x
runAdjointT (AdjointT ff uu mm h x -> uu (mm (ff h)) x)
-> (g x -> AdjointT ff uu mm h x) -> g x -> uu (mm (ff h)) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. g x -> AdjointT ff uu mm h x
g ~> AdjointT ff uu mm h
k)

adjoint :: (FFunctor ff, FFunctor uu, Functor x) => uu (ff x) ~> Adjoint ff uu x
adjoint :: forall (ff :: FF) (uu :: FF) (x :: FUNCTOR).
(FFunctor ff, FFunctor uu, Functor x) =>
uu (ff x) ~> Adjoint ff uu x
adjoint = uu (IdentityT (ff x)) x -> AdjointT ff uu IdentityT x x
forall {k} {k} {k} {k} (ff :: k -> k) (uu :: k -> k -> *)
       (mm :: k -> k) (g :: k) (x :: k).
uu (mm (ff g)) x -> AdjointT ff uu mm g x
AdjointT (uu (IdentityT (ff x)) x -> AdjointT ff uu IdentityT x x)
-> (uu (ff x) x -> uu (IdentityT (ff x)) x)
-> uu (ff x) x
-> AdjointT ff uu IdentityT x x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ff x ~> IdentityT (ff x))
-> uu (ff x) x -> uu (IdentityT (ff x)) x
forall (g :: FUNCTOR) (h :: FUNCTOR) x.
(Functor g, Functor h) =>
(g ~> h) -> uu g x -> uu h x
forall (ff :: FF) (g :: FUNCTOR) (h :: FUNCTOR) x.
(FFunctor ff, Functor g, Functor h) =>
(g ~> h) -> ff g x -> ff h x
ffmap ff x x -> IdentityT (ff x) x
ff x ~> IdentityT (ff x)
forall {k} (f :: k -> *) (a :: k). f a -> IdentityT f a
IdentityT

runAdjoint :: (FFunctor ff, FFunctor uu, Functor x) => Adjoint ff uu x ~> uu (ff x)
runAdjoint :: forall (ff :: FF) (uu :: FF) (x :: FUNCTOR).
(FFunctor ff, FFunctor uu, Functor x) =>
Adjoint ff uu x ~> uu (ff x)
runAdjoint = (IdentityT (ff x) ~> ff x)
-> uu (IdentityT (ff x)) x -> uu (ff x) x
forall (g :: FUNCTOR) (h :: FUNCTOR) x.
(Functor g, Functor h) =>
(g ~> h) -> uu g x -> uu h x
forall (ff :: FF) (g :: FUNCTOR) (h :: FUNCTOR) x.
(FFunctor ff, Functor g, Functor h) =>
(g ~> h) -> ff g x -> ff h x
ffmap IdentityT (ff x) x -> ff x x
IdentityT (ff x) ~> ff x
forall {k} (f :: k -> *) (a :: k). IdentityT f a -> f a
runIdentityT (uu (IdentityT (ff x)) x -> uu (ff x) x)
-> (Adjoint ff uu x x -> uu (IdentityT (ff x)) x)
-> Adjoint ff uu x x
-> uu (ff x) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Adjoint ff uu x x -> uu (IdentityT (ff x)) x
forall {k} {k} {k} {k} (ff :: k -> k) (uu :: k -> k -> *)
       (mm :: k -> k) (g :: k) (x :: k).
AdjointT ff uu mm g x -> uu (mm (ff g)) x
runAdjointT

fffmap :: forall mm nn ff uu x.
     (FFunctor mm, FFunctor nn, FFunctor ff, FFunctor uu, Functor x)
  => (forall y. (Functor y) => mm y ~> nn y)
  -> (AdjointT ff uu mm x ~> AdjointT ff uu nn x)
fffmap :: forall (mm :: FF) (nn :: FF) (ff :: FF) (uu :: FF) (x :: FUNCTOR).
(FFunctor mm, FFunctor nn, FFunctor ff, FFunctor uu, Functor x) =>
(forall (y :: FUNCTOR). Functor y => mm y ~> nn y)
-> AdjointT ff uu mm x ~> AdjointT ff uu nn x
fffmap forall (y :: FUNCTOR). Functor y => mm y ~> nn y
trans = uu (nn (ff x)) x -> AdjointT ff uu nn x x
forall {k} {k} {k} {k} (ff :: k -> k) (uu :: k -> k -> *)
       (mm :: k -> k) (g :: k) (x :: k).
uu (mm (ff g)) x -> AdjointT ff uu mm g x
AdjointT (uu (nn (ff x)) x -> AdjointT ff uu nn x x)
-> (AdjointT ff uu mm x x -> uu (nn (ff x)) x)
-> AdjointT ff uu mm x x
-> AdjointT ff uu nn x x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (mm (ff x) ~> nn (ff x)) -> uu (mm (ff x)) x -> uu (nn (ff x)) x
forall (g :: FUNCTOR) (h :: FUNCTOR) x.
(Functor g, Functor h) =>
(g ~> h) -> uu g x -> uu h x
forall (ff :: FF) (g :: FUNCTOR) (h :: FUNCTOR) x.
(FFunctor ff, Functor g, Functor h) =>
(g ~> h) -> ff g x -> ff h x
ffmap mm (ff x) x -> nn (ff x) x
mm (ff x) ~> nn (ff x)
forall (y :: FUNCTOR). Functor y => mm y ~> nn y
trans (uu (mm (ff x)) x -> uu (nn (ff x)) x)
-> (AdjointT ff uu mm x x -> uu (mm (ff x)) x)
-> AdjointT ff uu mm x x
-> uu (nn (ff x)) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AdjointT ff uu mm x x -> uu (mm (ff x)) x
forall {k} {k} {k} {k} (ff :: k -> k) (uu :: k -> k -> *)
       (mm :: k -> k) (g :: k) (x :: k).
AdjointT ff uu mm g x -> uu (mm (ff g)) x
runAdjointT

generalize :: (FMonad mm, FFunctor ff, FFunctor uu, Functor x) => Adjoint ff uu x ~> AdjointT ff uu mm x
generalize :: forall (mm :: FF) (ff :: FF) (uu :: FF) (x :: FUNCTOR).
(FMonad mm, FFunctor ff, FFunctor uu, Functor x) =>
Adjoint ff uu x ~> AdjointT ff uu mm x
generalize = (forall (y :: FUNCTOR). Functor y => IdentityT y ~> mm y)
-> AdjointT ff uu IdentityT x ~> AdjointT ff uu mm x
forall (mm :: FF) (nn :: FF) (ff :: FF) (uu :: FF) (x :: FUNCTOR).
(FFunctor mm, FFunctor nn, FFunctor ff, FFunctor uu, Functor x) =>
(forall (y :: FUNCTOR). Functor y => mm y ~> nn y)
-> AdjointT ff uu mm x ~> AdjointT ff uu nn x
fffmap (y x -> mm y x
y ~> mm y
forall (g :: FUNCTOR). Functor g => g ~> mm g
forall (ff :: FF) (g :: FUNCTOR).
(FMonad ff, Functor g) =>
g ~> ff g
fpure (y x -> mm y x)
-> (IdentityT y x -> y x) -> IdentityT y x -> mm y x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IdentityT y x -> y x
forall {k} (f :: k -> *) (a :: k). IdentityT f a -> f a
runIdentityT)