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

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

import FFunctor
import FComonad
import FStrong
import FFunctor.FCompose
import FFunctor.Adjunction

newtype AdjointT ff uu ww g x = AdjointT { forall {k} {k} {k} {k} (ff :: k -> k -> *) (uu :: k -> k)
       (ww :: k -> k) (g :: k) (x :: k).
AdjointT ff uu ww g x -> ff (ww (uu g)) x
runAdjointT :: ff (ww (uu g)) x }
  deriving (forall a b.
 (a -> b) -> AdjointT ff uu ww g a -> AdjointT ff uu ww g b)
-> (forall a b.
    a -> AdjointT ff uu ww g b -> AdjointT ff uu ww g a)
-> Functor (AdjointT ff uu ww g)
forall a b. a -> AdjointT ff uu ww g b -> AdjointT ff uu ww g a
forall a b.
(a -> b) -> AdjointT ff uu ww g a -> AdjointT ff uu ww g b
forall k (ff :: k -> * -> *) k k (uu :: k -> k) (ww :: k -> k)
       (g :: k) a b.
Functor (ff (ww (uu g))) =>
a -> AdjointT ff uu ww g b -> AdjointT ff uu ww g a
forall k (ff :: k -> * -> *) k k (uu :: k -> k) (ww :: k -> k)
       (g :: k) a b.
Functor (ff (ww (uu g))) =>
(a -> b) -> AdjointT ff uu ww g a -> AdjointT ff uu ww g b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall k (ff :: k -> * -> *) k k (uu :: k -> k) (ww :: k -> k)
       (g :: k) a b.
Functor (ff (ww (uu g))) =>
(a -> b) -> AdjointT ff uu ww g a -> AdjointT ff uu ww g b
fmap :: forall a b.
(a -> b) -> AdjointT ff uu ww g a -> AdjointT ff uu ww g b
$c<$ :: forall k (ff :: k -> * -> *) k k (uu :: k -> k) (ww :: k -> k)
       (g :: k) a b.
Functor (ff (ww (uu g))) =>
a -> AdjointT ff uu ww g b -> AdjointT ff uu ww g a
<$ :: forall a b. a -> AdjointT ff uu ww g b -> AdjointT ff uu ww g a
Functor

type Adjoint ff uu = AdjointT ff uu IdentityT

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

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

instance (Adjunction ff uu, FComonad ww) => FComonad (AdjointT ff uu ww) where
    fextract :: forall (g :: * -> *). Functor g => AdjointT ff uu ww g ~> g
fextract = ff (uu g) x -> g x
ff (uu g) ~> g
forall (g :: * -> *). Functor g => ff (uu g) ~> g
forall (ff :: FF) (uu :: FF) (g :: * -> *).
(Adjunction ff uu, Functor g) =>
ff (uu g) ~> g
counit (ff (uu g) x -> g x)
-> (AdjointT ff uu ww g x -> ff (uu g) x)
-> AdjointT ff uu ww g x
-> g x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ww (uu g) ~> uu g) -> ff (ww (uu g)) x -> ff (uu g) x
forall (g :: * -> *) (h :: * -> *) x.
(Functor g, Functor h) =>
(g ~> h) -> ff g x -> ff h x
forall (ff :: FF) (g :: * -> *) (h :: * -> *) x.
(FFunctor ff, Functor g, Functor h) =>
(g ~> h) -> ff g x -> ff h x
ffmap ww (uu g) x -> uu g x
ww (uu g) ~> uu g
forall (g :: * -> *). Functor g => ww g ~> g
forall (ff :: FF) (g :: * -> *).
(FComonad ff, Functor g) =>
ff g ~> g
fextract (ff (ww (uu g)) x -> ff (uu g) x)
-> (AdjointT ff uu ww g x -> ff (ww (uu g)) x)
-> AdjointT ff uu ww g x
-> ff (uu g) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AdjointT ff uu ww g x -> ff (ww (uu g)) x
forall {k} {k} {k} {k} (ff :: k -> k -> *) (uu :: k -> k)
       (ww :: k -> k) (g :: k) (x :: k).
AdjointT ff uu ww g x -> ff (ww (uu g)) x
runAdjointT
    fextend :: forall (g :: * -> *) (h :: * -> *).
(Functor g, Functor h) =>
(AdjointT ff uu ww g ~> h)
-> AdjointT ff uu ww g ~> AdjointT ff uu ww h
fextend AdjointT ff uu ww g ~> h
tr = (ff (ww (uu g)) ~> h)
-> AdjointT ff uu ww (ff (ww (uu g))) x -> AdjointT ff uu ww h x
forall (g :: * -> *) (h :: * -> *) x.
(Functor g, Functor h) =>
(g ~> h) -> AdjointT ff uu ww g x -> AdjointT ff uu ww h x
forall (ff :: FF) (g :: * -> *) (h :: * -> *) x.
(FFunctor ff, Functor g, Functor h) =>
(g ~> h) -> ff g x -> ff h x
ffmap (AdjointT ff uu ww g x -> h x
AdjointT ff uu ww g ~> h
tr (AdjointT ff uu ww g x -> h x)
-> (ff (ww (uu g)) x -> AdjointT ff uu ww g x)
-> ff (ww (uu g)) x
-> h x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ff (ww (uu g)) x -> AdjointT ff uu ww g x
forall {k} {k} {k} {k} (ff :: k -> k -> *) (uu :: k -> k)
       (ww :: k -> k) (g :: k) (x :: k).
ff (ww (uu g)) x -> AdjointT ff uu ww g x
AdjointT) (AdjointT ff uu ww (ff (ww (uu g))) x -> AdjointT ff uu ww h x)
-> (AdjointT ff uu ww g x -> AdjointT ff uu ww (ff (ww (uu g))) x)
-> AdjointT ff uu ww g x
-> AdjointT ff uu ww h x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ff (ww (uu (ff (ww (uu g))))) x
-> AdjointT ff uu ww (ff (ww (uu g))) x
forall {k} {k} {k} {k} (ff :: k -> k -> *) (uu :: k -> k)
       (ww :: k -> k) (g :: k) (x :: k).
ff (ww (uu g)) x -> AdjointT ff uu ww g x
AdjointT (ff (ww (uu (ff (ww (uu g))))) x
 -> AdjointT ff uu ww (ff (ww (uu g))) x)
-> (AdjointT ff uu ww g x -> ff (ww (uu (ff (ww (uu g))))) x)
-> AdjointT ff uu ww g x
-> AdjointT ff uu ww (ff (ww (uu g))) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ww (uu g) ~> ww (uu (ff (ww (uu g)))))
-> ff (ww (uu g)) x -> ff (ww (uu (ff (ww (uu g))))) x
forall (g :: * -> *) (h :: * -> *) x.
(Functor g, Functor h) =>
(g ~> h) -> ff g x -> ff h x
forall (ff :: FF) (g :: * -> *) (h :: * -> *) x.
(FFunctor ff, Functor g, Functor h) =>
(g ~> h) -> ff g x -> ff h x
ffmap ((ww (uu g) ~> uu (ff (ww (uu g))))
-> ww (uu g) ~> ww (uu (ff (ww (uu g))))
forall (g :: * -> *) (h :: * -> *).
(Functor g, Functor h) =>
(ww g ~> h) -> ww g ~> ww h
forall (ff :: FF) (g :: * -> *) (h :: * -> *).
(FComonad ff, Functor g, Functor h) =>
(ff g ~> h) -> ff g ~> ff h
fextend ww (uu g) x -> uu (ff (ww (uu g))) x
ww (uu g) ~> uu (ff (ww (uu g)))
forall (g :: * -> *). Functor g => g ~> uu (ff g)
forall (ff :: FF) (uu :: FF) (g :: * -> *).
(Adjunction ff uu, Functor g) =>
g ~> uu (ff g)
unit) (ff (ww (uu g)) x -> ff (ww (uu (ff (ww (uu g))))) x)
-> (AdjointT ff uu ww g x -> ff (ww (uu g)) x)
-> AdjointT ff uu ww g x
-> ff (ww (uu (ff (ww (uu g))))) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AdjointT ff uu ww g x -> ff (ww (uu g)) x
forall {k} {k} {k} {k} (ff :: k -> k -> *) (uu :: k -> k)
       (ww :: k -> k) (g :: k) (x :: k).
AdjointT ff uu ww g x -> ff (ww (uu g)) x
runAdjointT

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

runAdjoint :: (FFunctor ff, FFunctor uu, Functor x) => Adjoint ff uu x ~> ff (uu x)
runAdjoint :: forall (ff :: FF) (uu :: FF) (x :: * -> *).
(FFunctor ff, FFunctor uu, Functor x) =>
Adjoint ff uu x ~> ff (uu x)
runAdjoint = (IdentityT (uu x) ~> uu x)
-> ff (IdentityT (uu x)) x -> ff (uu x) x
forall (g :: * -> *) (h :: * -> *) x.
(Functor g, Functor h) =>
(g ~> h) -> ff g x -> ff h x
forall (ff :: FF) (g :: * -> *) (h :: * -> *) x.
(FFunctor ff, Functor g, Functor h) =>
(g ~> h) -> ff g x -> ff h x
ffmap IdentityT (uu x) x -> uu x x
IdentityT (uu x) ~> uu x
forall {k} (f :: k -> *) (a :: k). IdentityT f a -> f a
runIdentityT (ff (IdentityT (uu x)) x -> ff (uu x) x)
-> (Adjoint ff uu x x -> ff (IdentityT (uu x)) x)
-> Adjoint ff uu x x
-> ff (uu x) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Adjoint ff uu x x -> ff (IdentityT (uu x)) x
forall {k} {k} {k} {k} (ff :: k -> k -> *) (uu :: k -> k)
       (ww :: k -> k) (g :: k) (x :: k).
AdjointT ff uu ww g x -> ff (ww (uu 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 :: * -> *).
(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 (y :: * -> *). Functor y => mm y ~> nn y
trans = ff (nn (uu x)) x -> AdjointT ff uu nn x x
forall {k} {k} {k} {k} (ff :: k -> k -> *) (uu :: k -> k)
       (ww :: k -> k) (g :: k) (x :: k).
ff (ww (uu g)) x -> AdjointT ff uu ww g x
AdjointT (ff (nn (uu x)) x -> AdjointT ff uu nn x x)
-> (AdjointT ff uu mm x x -> ff (nn (uu 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 (uu x) ~> nn (uu x)) -> ff (mm (uu x)) x -> ff (nn (uu x)) x
forall (g :: * -> *) (h :: * -> *) x.
(Functor g, Functor h) =>
(g ~> h) -> ff g x -> ff h x
forall (ff :: FF) (g :: * -> *) (h :: * -> *) x.
(FFunctor ff, Functor g, Functor h) =>
(g ~> h) -> ff g x -> ff h x
ffmap mm (uu x) x -> nn (uu x) x
mm (uu x) ~> nn (uu x)
forall (y :: * -> *). Functor y => mm y ~> nn y
trans (ff (mm (uu x)) x -> ff (nn (uu x)) x)
-> (AdjointT ff uu mm x x -> ff (mm (uu x)) x)
-> AdjointT ff uu mm x x
-> ff (nn (uu x)) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AdjointT ff uu mm x x -> ff (mm (uu x)) x
forall {k} {k} {k} {k} (ff :: k -> k -> *) (uu :: k -> k)
       (ww :: k -> k) (g :: k) (x :: k).
AdjointT ff uu ww g x -> ff (ww (uu g)) x
runAdjointT

ungeneralize :: (FComonad ww, FFunctor ff, FFunctor uu, Functor x) => AdjointT ff uu ww x ~> Adjoint ff uu x
ungeneralize :: forall (ww :: FF) (ff :: FF) (uu :: FF) (x :: * -> *).
(FComonad ww, FFunctor ff, FFunctor uu, Functor x) =>
AdjointT ff uu ww x ~> Adjoint ff uu x
ungeneralize = (forall (y :: * -> *). Functor y => ww y ~> IdentityT y)
-> AdjointT ff uu ww x ~> AdjointT ff uu IdentityT x
forall (mm :: FF) (nn :: FF) (ff :: FF) (uu :: FF) (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 (y x -> IdentityT y x
forall {k} (f :: k -> *) (a :: k). f a -> IdentityT f a
IdentityT (y x -> IdentityT y x)
-> (ww y x -> y x) -> ww y x -> IdentityT y x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ww y x -> y x
ww y ~> y
forall (g :: * -> *). Functor g => ww g ~> g
forall (ff :: FF) (g :: * -> *).
(FComonad ff, Functor g) =>
ff g ~> g
fextract)