{-# LANGUAGE Rank2Types
, MultiParamTypeClasses
, FunctionalDependencies
, TypeOperators
, UndecidableInstances #-}
{-# LANGUAGE CPP #-}
#if __GLASGOW_HASKELL__ >= 702
{-# LANGUAGE Trustworthy #-}
#endif
#if __GLASGOW_HASKELL__ >= 708
{-# LANGUAGE EmptyCase #-}
#endif
module Data.Functor.Adjunction
( Adjunction(..)
, adjuncted
, tabulateAdjunction
, indexAdjunction
, zapWithAdjunction
, zipR, unzipR
, unabsurdL, absurdL
, cozipL, uncozipL
, extractL, duplicateL
, splitL, unsplitL
) where
#if __GLASGOW_HASKELL__ < 710
import Control.Applicative
#endif
import Control.Arrow ((&&&), (|||))
import Control.Monad.Free
#if __GLASGOW_HASKELL__ < 707
import Control.Monad.Instances ()
#endif
import Control.Monad.Trans.Identity
import Control.Monad.Trans.Reader
import Control.Monad.Trans.Writer
import Control.Comonad
import Control.Comonad.Cofree
import Control.Comonad.Trans.Env
import Control.Comonad.Trans.Traced
import Data.Functor.Identity
import Data.Functor.Compose
import Data.Functor.Product
import Data.Functor.Rep
import Data.Functor.Sum
import Data.Profunctor
import Data.Void
import GHC.Generics
class (Functor f, Representable u) =>
Adjunction f u | f -> u, u -> f where
#if __GLASGOW_HASKELL__ >= 708
{-# MINIMAL (unit, counit) | (leftAdjunct, rightAdjunct) #-}
#endif
unit :: a -> u (f a)
counit :: f (u a) -> a
leftAdjunct :: (f a -> b) -> a -> u b
rightAdjunct :: (a -> u b) -> f a -> b
unit = (f a -> f a) -> a -> u (f a)
forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(f a -> b) -> a -> u b
leftAdjunct f a -> f a
forall a. a -> a
id
counit = (u a -> u a) -> f (u a) -> a
forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(a -> u b) -> f a -> b
rightAdjunct u a -> u a
forall a. a -> a
id
leftAdjunct f a -> b
f = (f a -> b) -> u (f a) -> u b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f a -> b
f (u (f a) -> u b) -> (a -> u (f a)) -> a -> u b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> u (f a)
forall (f :: * -> *) (u :: * -> *) a.
Adjunction f u =>
a -> u (f a)
unit
rightAdjunct a -> u b
f = f (u b) -> b
forall (f :: * -> *) (u :: * -> *) a.
Adjunction f u =>
f (u a) -> a
counit (f (u b) -> b) -> (f a -> f (u b)) -> f a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> u b) -> f a -> f (u b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> u b
f
adjuncted :: (Adjunction f u, Profunctor p, Functor g)
=> p (a -> u b) (g (c -> u d)) -> p (f a -> b) (g (f c -> d))
adjuncted :: p (a -> u b) (g (c -> u d)) -> p (f a -> b) (g (f c -> d))
adjuncted = ((f a -> b) -> a -> u b)
-> (g (c -> u d) -> g (f c -> d))
-> p (a -> u b) (g (c -> u d))
-> p (f a -> b) (g (f c -> d))
forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap (f a -> b) -> a -> u b
forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(f a -> b) -> a -> u b
leftAdjunct (((c -> u d) -> f c -> d) -> g (c -> u d) -> g (f c -> d)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (c -> u d) -> f c -> d
forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(a -> u b) -> f a -> b
rightAdjunct)
{-# INLINE adjuncted #-}
tabulateAdjunction :: Adjunction f u => (f () -> b) -> u b
tabulateAdjunction :: (f () -> b) -> u b
tabulateAdjunction f () -> b
f = (f () -> b) -> () -> u b
forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(f a -> b) -> a -> u b
leftAdjunct f () -> b
f ()
indexAdjunction :: Adjunction f u => u b -> f a -> b
indexAdjunction :: u b -> f a -> b
indexAdjunction = (a -> u b) -> f a -> b
forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(a -> u b) -> f a -> b
rightAdjunct ((a -> u b) -> f a -> b) -> (u b -> a -> u b) -> u b -> f a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. u b -> a -> u b
forall a b. a -> b -> a
const
zapWithAdjunction :: Adjunction f u => (a -> b -> c) -> u a -> f b -> c
zapWithAdjunction :: (a -> b -> c) -> u a -> f b -> c
zapWithAdjunction a -> b -> c
f u a
ua = (b -> u c) -> f b -> c
forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(a -> u b) -> f a -> b
rightAdjunct (\b
b -> (a -> c) -> u a -> u c
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> b -> c) -> b -> a -> c
forall a b c. (a -> b -> c) -> b -> a -> c
flip a -> b -> c
f b
b) u a
ua)
splitL :: Adjunction f u => f a -> (a, f ())
splitL :: f a -> (a, f ())
splitL = (a -> u (a, f ())) -> f a -> (a, f ())
forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(a -> u b) -> f a -> b
rightAdjunct (((f () -> (a, f ())) -> () -> u (a, f ()))
-> () -> (f () -> (a, f ())) -> u (a, f ())
forall a b c. (a -> b -> c) -> b -> a -> c
flip (f () -> (a, f ())) -> () -> u (a, f ())
forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(f a -> b) -> a -> u b
leftAdjunct () ((f () -> (a, f ())) -> u (a, f ()))
-> (a -> f () -> (a, f ())) -> a -> u (a, f ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (,))
unsplitL :: Functor f => a -> f () -> f a
unsplitL :: a -> f () -> f a
unsplitL = a -> f () -> f a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
(<$)
extractL :: Adjunction f u => f a -> a
= (a, f ()) -> a
forall a b. (a, b) -> a
fst ((a, f ()) -> a) -> (f a -> (a, f ())) -> f a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f a -> (a, f ())
forall (f :: * -> *) (u :: * -> *) a.
Adjunction f u =>
f a -> (a, f ())
splitL
duplicateL :: Adjunction f u => f a -> f (f a)
duplicateL :: f a -> f (f a)
duplicateL f a
as = f a
as f a -> f a -> f (f a)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f a
as
zipR :: Adjunction f u => (u a, u b) -> u (a, b)
zipR :: (u a, u b) -> u (a, b)
zipR = (f (u a, u b) -> (a, b)) -> (u a, u b) -> u (a, b)
forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(f a -> b) -> a -> u b
leftAdjunct (((u a, u b) -> u a) -> f (u a, u b) -> a
forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(a -> u b) -> f a -> b
rightAdjunct (u a, u b) -> u a
forall a b. (a, b) -> a
fst (f (u a, u b) -> a)
-> (f (u a, u b) -> b) -> f (u a, u b) -> (a, b)
forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& ((u a, u b) -> u b) -> f (u a, u b) -> b
forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(a -> u b) -> f a -> b
rightAdjunct (u a, u b) -> u b
forall a b. (a, b) -> b
snd)
unzipR :: Functor u => u (a, b) -> (u a, u b)
unzipR :: u (a, b) -> (u a, u b)
unzipR = ((a, b) -> a) -> u (a, b) -> u a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (a, b) -> a
forall a b. (a, b) -> a
fst (u (a, b) -> u a) -> (u (a, b) -> u b) -> u (a, b) -> (u a, u b)
forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& ((a, b) -> b) -> u (a, b) -> u b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (a, b) -> b
forall a b. (a, b) -> b
snd
absurdL :: Void -> f Void
absurdL :: Void -> f Void
absurdL = Void -> f Void
forall a. Void -> a
absurd
unabsurdL :: Adjunction f u => f Void -> Void
unabsurdL :: f Void -> Void
unabsurdL = (Void -> u Void) -> f Void -> Void
forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(a -> u b) -> f a -> b
rightAdjunct Void -> u Void
forall a. Void -> a
absurd
cozipL :: Adjunction f u => f (Either a b) -> Either (f a) (f b)
cozipL :: f (Either a b) -> Either (f a) (f b)
cozipL = (Either a b -> u (Either (f a) (f b)))
-> f (Either a b) -> Either (f a) (f b)
forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(a -> u b) -> f a -> b
rightAdjunct ((f a -> Either (f a) (f b)) -> a -> u (Either (f a) (f b))
forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(f a -> b) -> a -> u b
leftAdjunct f a -> Either (f a) (f b)
forall a b. a -> Either a b
Left (a -> u (Either (f a) (f b)))
-> (b -> u (Either (f a) (f b)))
-> Either a b
-> u (Either (f a) (f b))
forall (a :: * -> * -> *) b d c.
ArrowChoice a =>
a b d -> a c d -> a (Either b c) d
||| (f b -> Either (f a) (f b)) -> b -> u (Either (f a) (f b))
forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(f a -> b) -> a -> u b
leftAdjunct f b -> Either (f a) (f b)
forall a b. b -> Either a b
Right)
uncozipL :: Functor f => Either (f a) (f b) -> f (Either a b)
uncozipL :: Either (f a) (f b) -> f (Either a b)
uncozipL = (a -> Either a b) -> f a -> f (Either a b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Either a b
forall a b. a -> Either a b
Left (f a -> f (Either a b))
-> (f b -> f (Either a b)) -> Either (f a) (f b) -> f (Either a b)
forall (a :: * -> * -> *) b d c.
ArrowChoice a =>
a b d -> a c d -> a (Either b c) d
||| (b -> Either a b) -> f b -> f (Either a b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap b -> Either a b
forall a b. b -> Either a b
Right
instance Adjunction ((,) e) ((->) e) where
leftAdjunct :: ((e, a) -> b) -> a -> e -> b
leftAdjunct (e, a) -> b
f a
a e
e = (e, a) -> b
f (e
e, a
a)
rightAdjunct :: (a -> e -> b) -> (e, a) -> b
rightAdjunct a -> e -> b
f ~(e
e, a
a) = a -> e -> b
f a
a e
e
instance Adjunction Identity Identity where
leftAdjunct :: (Identity a -> b) -> a -> Identity b
leftAdjunct Identity a -> b
f = b -> Identity b
forall a. a -> Identity a
Identity (b -> Identity b) -> (a -> b) -> a -> Identity b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Identity a -> b
f (Identity a -> b) -> (a -> Identity a) -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Identity a
forall a. a -> Identity a
Identity
rightAdjunct :: (a -> Identity b) -> Identity a -> b
rightAdjunct a -> Identity b
f = Identity b -> b
forall a. Identity a -> a
runIdentity (Identity b -> b) -> (Identity a -> Identity b) -> Identity a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Identity b
f (a -> Identity b) -> (Identity a -> a) -> Identity a -> Identity b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Identity a -> a
forall a. Identity a -> a
runIdentity
instance Adjunction f g =>
Adjunction (IdentityT f) (IdentityT g) where
unit :: a -> IdentityT g (IdentityT f a)
unit = g (IdentityT f a) -> IdentityT g (IdentityT f a)
forall k (f :: k -> *) (a :: k). f a -> IdentityT f a
IdentityT (g (IdentityT f a) -> IdentityT g (IdentityT f a))
-> (a -> g (IdentityT f a)) -> a -> IdentityT g (IdentityT f a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f a -> IdentityT f a) -> a -> g (IdentityT f a)
forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(f a -> b) -> a -> u b
leftAdjunct f a -> IdentityT f a
forall k (f :: k -> *) (a :: k). f a -> IdentityT f a
IdentityT
counit :: IdentityT f (IdentityT g a) -> a
counit = (IdentityT g a -> g a) -> f (IdentityT g a) -> a
forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(a -> u b) -> f a -> b
rightAdjunct IdentityT g a -> g a
forall k (f :: k -> *) (a :: k). IdentityT f a -> f a
runIdentityT (f (IdentityT g a) -> a)
-> (IdentityT f (IdentityT g a) -> f (IdentityT g a))
-> IdentityT f (IdentityT g a)
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IdentityT f (IdentityT g a) -> f (IdentityT g a)
forall k (f :: k -> *) (a :: k). IdentityT f a -> f a
runIdentityT
instance Adjunction w m =>
Adjunction (EnvT e w) (ReaderT e m) where
unit :: a -> ReaderT e m (EnvT e w a)
unit = (e -> m (EnvT e w a)) -> ReaderT e m (EnvT e w a)
forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
ReaderT ((e -> m (EnvT e w a)) -> ReaderT e m (EnvT e w a))
-> (a -> e -> m (EnvT e w a)) -> a -> ReaderT e m (EnvT e w a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (((w a -> EnvT e w a) -> m (EnvT e w a))
-> (e -> w a -> EnvT e w a) -> e -> m (EnvT e w a))
-> (e -> w a -> EnvT e w a)
-> ((w a -> EnvT e w a) -> m (EnvT e w a))
-> e
-> m (EnvT e w a)
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((w a -> EnvT e w a) -> m (EnvT e w a))
-> (e -> w a -> EnvT e w a) -> e -> m (EnvT e w a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap e -> w a -> EnvT e w a
forall e (w :: * -> *) a. e -> w a -> EnvT e w a
EnvT (((w a -> EnvT e w a) -> m (EnvT e w a)) -> e -> m (EnvT e w a))
-> (a -> (w a -> EnvT e w a) -> m (EnvT e w a))
-> a
-> e
-> m (EnvT e w a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((w a -> EnvT e w a) -> a -> m (EnvT e w a))
-> a -> (w a -> EnvT e w a) -> m (EnvT e w a)
forall a b c. (a -> b -> c) -> b -> a -> c
flip (w a -> EnvT e w a) -> a -> m (EnvT e w a)
forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(f a -> b) -> a -> u b
leftAdjunct
counit :: EnvT e w (ReaderT e m a) -> a
counit (EnvT e
e w (ReaderT e m a)
w) = (ReaderT e m a -> m a) -> w (ReaderT e m a) -> a
forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(a -> u b) -> f a -> b
rightAdjunct ((ReaderT e m a -> e -> m a) -> e -> ReaderT e m a -> m a
forall a b c. (a -> b -> c) -> b -> a -> c
flip ReaderT e m a -> e -> m a
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT e
e) w (ReaderT e m a)
w
instance Adjunction m w =>
Adjunction (WriterT s m) (TracedT s w) where
unit :: a -> TracedT s w (WriterT s m a)
unit = w (s -> WriterT s m a) -> TracedT s w (WriterT s m a)
forall m (w :: * -> *) a. w (m -> a) -> TracedT m w a
TracedT (w (s -> WriterT s m a) -> TracedT s w (WriterT s m a))
-> (a -> w (s -> WriterT s m a))
-> a
-> TracedT s w (WriterT s m a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (m a -> s -> WriterT s m a) -> a -> w (s -> WriterT s m a)
forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(f a -> b) -> a -> u b
leftAdjunct (\m a
ma s
s -> m (a, s) -> WriterT s m a
forall w (m :: * -> *) a. m (a, w) -> WriterT w m a
WriterT ((a -> (a, s)) -> m a -> m (a, s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\a
a -> (a
a, s
s)) m a
ma))
counit :: WriterT s m (TracedT s w a) -> a
counit = ((TracedT s w a, s) -> w a) -> m (TracedT s w a, s) -> a
forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(a -> u b) -> f a -> b
rightAdjunct (\(TracedT s w a
t, s
s) -> ((s -> a) -> s -> a
forall a b. (a -> b) -> a -> b
$ s
s) ((s -> a) -> a) -> w (s -> a) -> w a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TracedT s w a -> w (s -> a)
forall m (w :: * -> *) a. TracedT m w a -> w (m -> a)
runTracedT TracedT s w a
t) (m (TracedT s w a, s) -> a)
-> (WriterT s m (TracedT s w a) -> m (TracedT s w a, s))
-> WriterT s m (TracedT s w a)
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WriterT s m (TracedT s w a) -> m (TracedT s w a, s)
forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT
instance (Adjunction f g, Adjunction f' g') =>
Adjunction (Compose f' f) (Compose g g') where
unit :: a -> Compose g g' (Compose f' f a)
unit = g (g' (Compose f' f a)) -> Compose g g' (Compose f' f a)
forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (g (g' (Compose f' f a)) -> Compose g g' (Compose f' f a))
-> (a -> g (g' (Compose f' f a)))
-> a
-> Compose g g' (Compose f' f a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f a -> g' (Compose f' f a)) -> a -> g (g' (Compose f' f a))
forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(f a -> b) -> a -> u b
leftAdjunct ((f' (f a) -> Compose f' f a) -> f a -> g' (Compose f' f a)
forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(f a -> b) -> a -> u b
leftAdjunct f' (f a) -> Compose f' f a
forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose)
counit :: Compose f' f (Compose g g' a) -> a
counit = (f (Compose g g' a) -> g' a) -> f' (f (Compose g g' a)) -> a
forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(a -> u b) -> f a -> b
rightAdjunct ((Compose g g' a -> g (g' a)) -> f (Compose g g' a) -> g' a
forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(a -> u b) -> f a -> b
rightAdjunct Compose g g' a -> g (g' a)
forall k1 (f :: k1 -> *) k2 (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose) (f' (f (Compose g g' a)) -> a)
-> (Compose f' f (Compose g g' a) -> f' (f (Compose g g' a)))
-> Compose f' f (Compose g g' a)
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Compose f' f (Compose g g' a) -> f' (f (Compose g g' a))
forall k1 (f :: k1 -> *) k2 (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose
instance (Adjunction f g, Adjunction f' g') =>
Adjunction (Sum f f') (Product g g') where
unit :: a -> Product g g' (Sum f f' a)
unit a
a = g (Sum f f' a) -> g' (Sum f f' a) -> Product g g' (Sum f f' a)
forall k (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> Product f g a
Pair ((f a -> Sum f f' a) -> a -> g (Sum f f' a)
forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(f a -> b) -> a -> u b
leftAdjunct f a -> Sum f f' a
forall k (f :: k -> *) (g :: k -> *) (a :: k). f a -> Sum f g a
InL a
a) ((f' a -> Sum f f' a) -> a -> g' (Sum f f' a)
forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(f a -> b) -> a -> u b
leftAdjunct f' a -> Sum f f' a
forall k (f :: k -> *) (g :: k -> *) (a :: k). g a -> Sum f g a
InR a
a)
counit :: Sum f f' (Product g g' a) -> a
counit (InL f (Product g g' a)
l) = (Product g g' a -> g a) -> f (Product g g' a) -> a
forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(a -> u b) -> f a -> b
rightAdjunct (\(Pair g a
x g' a
_) -> g a
x) f (Product g g' a)
l
counit (InR f' (Product g g' a)
r) = (Product g g' a -> g' a) -> f' (Product g g' a) -> a
forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(a -> u b) -> f a -> b
rightAdjunct (\(Pair g a
_ g' a
x) -> g' a
x) f' (Product g g' a)
r
instance Adjunction f u =>
Adjunction (Free f) (Cofree u) where
unit :: a -> Cofree u (Free f a)
unit a
a = a -> Free f a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a Free f a -> u (Cofree u (Free f a)) -> Cofree u (Free f a)
forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< (f () -> Cofree u (Free f a)) -> u (Cofree u (Free f a))
forall (f :: * -> *) (u :: * -> *) b.
Adjunction f u =>
(f () -> b) -> u b
tabulateAdjunction (\f ()
k -> (Free f a -> Free f a) -> a -> Cofree u (Free f a)
forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(f a -> b) -> a -> u b
leftAdjunct (f (Free f a) -> Free f a
forall (f :: * -> *) (m :: * -> *) a.
MonadFree f m =>
f (m a) -> m a
wrap (f (Free f a) -> Free f a)
-> (Free f a -> f (Free f a)) -> Free f a -> Free f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Free f a -> f () -> f (Free f a))
-> f () -> Free f a -> f (Free f a)
forall a b c. (a -> b -> c) -> b -> a -> c
flip Free f a -> f () -> f (Free f a)
forall (f :: * -> *) a. Functor f => a -> f () -> f a
unsplitL f ()
k) a
a)
counit :: Free f (Cofree u a) -> a
counit (Pure Cofree u a
a) = Cofree u a -> a
forall (w :: * -> *) a. Comonad w => w a -> a
extract Cofree u a
a
counit (Free f (Free f (Cofree u a))
k) = (Cofree u a -> Cofree u a) -> Free f (Cofree u a) -> a
forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(a -> u b) -> f a -> b
rightAdjunct ((u (Cofree u a) -> f (Free f (Cofree u a)) -> Cofree u a)
-> f (Free f (Cofree u a)) -> u (Cofree u a) -> Cofree u a
forall a b c. (a -> b -> c) -> b -> a -> c
flip u (Cofree u a) -> f (Free f (Cofree u a)) -> Cofree u a
forall (f :: * -> *) (u :: * -> *) b a.
Adjunction f u =>
u b -> f a -> b
indexAdjunction f (Free f (Cofree u a))
k (u (Cofree u a) -> Cofree u a)
-> (Cofree u a -> u (Cofree u a)) -> Cofree u a -> Cofree u a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Cofree u a -> u (Cofree u a)
forall (f :: * -> *) (w :: * -> *) a.
ComonadCofree f w =>
w a -> f (w a)
unwrap) (f (Free f (Cofree u a)) -> Free f (Cofree u a)
forall (f :: * -> *) (u :: * -> *) a. Adjunction f u => f a -> a
extractL f (Free f (Cofree u a))
k)
instance Adjunction V1 U1 where
unit :: a -> U1 (V1 a)
unit a
_ = U1 (V1 a)
forall k (p :: k). U1 p
U1
counit :: V1 (U1 a) -> a
counit = V1 (U1 a) -> a
forall a b. V1 a -> b
absurdV1
absurdV1 :: V1 a -> b
#if __GLASGOW_HASKELL__ >= 708
absurdV1 :: V1 a -> b
absurdV1 V1 a
x = case V1 a
x of {}
#else
absurdV1 x = x `seq` undefined
#endif
instance Adjunction Par1 Par1 where
leftAdjunct :: (Par1 a -> b) -> a -> Par1 b
leftAdjunct Par1 a -> b
f = b -> Par1 b
forall p. p -> Par1 p
Par1 (b -> Par1 b) -> (a -> b) -> a -> Par1 b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Par1 a -> b
f (Par1 a -> b) -> (a -> Par1 a) -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Par1 a
forall p. p -> Par1 p
Par1
rightAdjunct :: (a -> Par1 b) -> Par1 a -> b
rightAdjunct a -> Par1 b
f = Par1 b -> b
forall p. Par1 p -> p
unPar1 (Par1 b -> b) -> (Par1 a -> Par1 b) -> Par1 a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Par1 b
f (a -> Par1 b) -> (Par1 a -> a) -> Par1 a -> Par1 b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Par1 a -> a
forall p. Par1 p -> p
unPar1
instance Adjunction f g => Adjunction (Rec1 f) (Rec1 g) where
unit :: a -> Rec1 g (Rec1 f a)
unit = g (Rec1 f a) -> Rec1 g (Rec1 f a)
forall k (f :: k -> *) (p :: k). f p -> Rec1 f p
Rec1 (g (Rec1 f a) -> Rec1 g (Rec1 f a))
-> (a -> g (Rec1 f a)) -> a -> Rec1 g (Rec1 f a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f a -> Rec1 f a) -> a -> g (Rec1 f a)
forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(f a -> b) -> a -> u b
leftAdjunct f a -> Rec1 f a
forall k (f :: k -> *) (p :: k). f p -> Rec1 f p
Rec1
counit :: Rec1 f (Rec1 g a) -> a
counit = (Rec1 g a -> g a) -> f (Rec1 g a) -> a
forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(a -> u b) -> f a -> b
rightAdjunct Rec1 g a -> g a
forall k (f :: k -> *) (p :: k). Rec1 f p -> f p
unRec1 (f (Rec1 g a) -> a)
-> (Rec1 f (Rec1 g a) -> f (Rec1 g a)) -> Rec1 f (Rec1 g a) -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rec1 f (Rec1 g a) -> f (Rec1 g a)
forall k (f :: k -> *) (p :: k). Rec1 f p -> f p
unRec1
instance (Adjunction f g, Adjunction f' g') => Adjunction (f' :.: f) (g :.: g') where
unit :: a -> (:.:) g g' ((:.:) f' f a)
unit = g (g' ((:.:) f' f a)) -> (:.:) g g' ((:.:) f' f a)
forall k2 k1 (f :: k2 -> *) (g :: k1 -> k2) (p :: k1).
f (g p) -> (:.:) f g p
Comp1 (g (g' ((:.:) f' f a)) -> (:.:) g g' ((:.:) f' f a))
-> (a -> g (g' ((:.:) f' f a))) -> a -> (:.:) g g' ((:.:) f' f a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f a -> g' ((:.:) f' f a)) -> a -> g (g' ((:.:) f' f a))
forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(f a -> b) -> a -> u b
leftAdjunct ((f' (f a) -> (:.:) f' f a) -> f a -> g' ((:.:) f' f a)
forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(f a -> b) -> a -> u b
leftAdjunct f' (f a) -> (:.:) f' f a
forall k2 k1 (f :: k2 -> *) (g :: k1 -> k2) (p :: k1).
f (g p) -> (:.:) f g p
Comp1)
counit :: (:.:) f' f ((:.:) g g' a) -> a
counit = (f ((:.:) g g' a) -> g' a) -> f' (f ((:.:) g g' a)) -> a
forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(a -> u b) -> f a -> b
rightAdjunct (((:.:) g g' a -> g (g' a)) -> f ((:.:) g g' a) -> g' a
forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(a -> u b) -> f a -> b
rightAdjunct (:.:) g g' a -> g (g' a)
forall k2 (f :: k2 -> *) k1 (g :: k1 -> k2) (p :: k1).
(:.:) f g p -> f (g p)
unComp1) (f' (f ((:.:) g g' a)) -> a)
-> ((:.:) f' f ((:.:) g g' a) -> f' (f ((:.:) g g' a)))
-> (:.:) f' f ((:.:) g g' a)
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (:.:) f' f ((:.:) g g' a) -> f' (f ((:.:) g g' a))
forall k2 (f :: k2 -> *) k1 (g :: k1 -> k2) (p :: k1).
(:.:) f g p -> f (g p)
unComp1
instance (Adjunction f g, Adjunction f' g') => Adjunction (f :+: f') (g :*: g') where
unit :: a -> (:*:) g g' ((:+:) f f' a)
unit a
a = (f a -> (:+:) f f' a) -> a -> g ((:+:) f f' a)
forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(f a -> b) -> a -> u b
leftAdjunct f a -> (:+:) f f' a
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 a
a g ((:+:) f f' a) -> g' ((:+:) f f' a) -> (:*:) g g' ((:+:) f f' a)
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: (f' a -> (:+:) f f' a) -> a -> g' ((:+:) f f' a)
forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(f a -> b) -> a -> u b
leftAdjunct f' a -> (:+:) f f' a
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 a
a
counit :: (:+:) f f' ((:*:) g g' a) -> a
counit (L1 f ((:*:) g g' a)
l) = ((:*:) g g' a -> g a) -> f ((:*:) g g' a) -> a
forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(a -> u b) -> f a -> b
rightAdjunct (\(g a
x :*: g' a
_) -> g a
x) f ((:*:) g g' a)
l
counit (R1 f' ((:*:) g g' a)
r) = ((:*:) g g' a -> g' a) -> f' ((:*:) g g' a) -> a
forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(a -> u b) -> f a -> b
rightAdjunct (\(g a
_ :*: g' a
x) -> g' a
x) f' ((:*:) g g' a)
r