{-# 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)