    {-# LANGUAGE Rank2Types
               , MultiParamTypeClasses
               , FunctionalDependencies
               , TypeOperators
               , UndecidableInstances #-}

    {-# LANGUAGE Trustworthy #-}
    {-# LANGUAGE EmptyCase #-}

    -------------------------------------------------------------------------------------------
    -- |
    -- Copyright 	: 2008-2013 Edward Kmett
    -- License	: BSD
    --
    -- Maintainer	: Edward Kmett <ekmett@gmail.com>
    -- Stability	: experimental
    -- Portability	: rank 2 types, MPTCs, fundeps
    --
    -------------------------------------------------------------------------------------------
    module Data.Functor.Adjunction
      ( Adjunction(..)
      , adjuncted
      , tabulateAdjunction
      , indexAdjunction
      , zapWithAdjunction
      , zipR, unzipR
      , unabsurdL, absurdL
      , cozipL, uncozipL
      , extractL, duplicateL
      , splitL, unsplitL
      ) where

    import Control.Arrow ((&&&), (|||))
    import Control.Monad.Free
    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

    -- | An adjunction between Hask and Hask.
    --
    -- Minimal definition: both 'unit' and 'counit' or both 'leftAdjunct'
    -- and 'rightAdjunct', subject to the constraints imposed by the
    -- default definitions that the following laws should hold.
    --
    -- > unit = leftAdjunct id
    -- > counit = rightAdjunct id
    -- > leftAdjunct f = fmap f . unit
    -- > rightAdjunct f = counit . fmap f
    --
    -- Any implementation is required to ensure that 'leftAdjunct' and
    -- 'rightAdjunct' witness an isomorphism from @Nat (f a, b)@ to
    -- @Nat (a, g b)@
    --
    -- > rightAdjunct unit = id
    -- > leftAdjunct counit = id
    class (Functor f, Representable u) =>
          Adjunction f u | f -> u, u -> f where
      {-# MINIMAL (unit, counit) | (leftAdjunct, rightAdjunct) #-}
      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 a b. (f a -> b) -> a -> u b
    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 a b. (a -> u b) -> f a -> b
    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 a b. (a -> b) -> u 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 a. 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 a. f (u a) -> a
    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 a b. (a -> b) -> f a -> f b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap a -> u b
    f

    -- | 'leftAdjunct' and 'rightAdjunct' form two halves of an isomorphism.
    --
    -- This can be used with the combinators from the @lens@ package.
    --
    -- @'adjuncted' :: 'Adjunction' f u => 'Iso'' (f a -> b) (a -> u b)@
    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 :: forall (f :: * -> *) (u :: * -> *) (p :: * -> * -> *) (g :: * -> *)
           a b c d.
    (Adjunction f u, Profunctor p, Functor g) =>
    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 a b c d. (a -> b) -> (c -> d) -> p b c -> p a 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 a b. (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 a b. (a -> b) -> g a -> g b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (c -> u d) -> f c -> d
    forall a b. (a -> u b) -> f a -> b
    forall (f :: * -> *) (u :: * -> *) a b.
    Adjunction f u =>
    (a -> u b) -> f a -> b
    rightAdjunct)
    {-# INLINE adjuncted #-}

    -- | Every right adjoint is representable by its left adjoint
    -- applied to a unit element
    --
    -- Use this definition and the primitives in
    -- Data.Functor.Representable to meet the requirements of the
    -- superclasses of Representable.
    tabulateAdjunction :: Adjunction f u => (f () -> b) -> u b
    tabulateAdjunction :: forall (f :: * -> *) (u :: * -> *) b.
    Adjunction f u =>
    (f () -> b) -> u b
    tabulateAdjunction f () -> b
    f = (f () -> b) -> () -> u b
    forall a b. (f a -> b) -> a -> u b
    forall (f :: * -> *) (u :: * -> *) a b.
    Adjunction f u =>
    (f a -> b) -> a -> u b
    leftAdjunct f () -> b
    f ()

    -- | This definition admits a default definition for the
    -- 'index' method of 'Index", one of the superclasses of
    -- Representable.
    indexAdjunction :: Adjunction f u => u b -> f a -> b
    indexAdjunction :: forall (f :: * -> *) (u :: * -> *) b a.
    Adjunction f u =>
    u b -> f a -> b
    indexAdjunction = (a -> u b) -> f a -> b
    forall a b. (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 :: forall (f :: * -> *) (u :: * -> *) a b c.
    Adjunction f u =>
    (a -> b -> c) -> u a -> f b -> c
    zapWithAdjunction a -> b -> c
    f u a
    ua = (b -> u c) -> f b -> c
    forall a b. (a -> u b) -> f a -> b
    forall (f :: * -> *) (u :: * -> *) a b.
    Adjunction f u =>
    (a -> u b) -> f a -> b
    rightAdjunct (\b
    b -> (a -> c) -> u a -> u c
    forall a b. (a -> b) -> u a -> u b
    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 :: forall (f :: * -> *) (u :: * -> *) a.
    Adjunction f u =>
    f a -> (a, f ())
    splitL = (a -> u (a, f ())) -> f a -> (a, f ())
    forall a b. (a -> u b) -> f a -> b
    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 a b. (f a -> b) -> a -> u b
    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 :: forall (f :: * -> *) a. Functor f => a -> f () -> f a
    unsplitL = a -> f () -> f a
    forall a b. a -> f b -> f a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    (<$)

    extractL :: Adjunction f u => f a -> a
    extractL :: forall (f :: * -> *) (u :: * -> *) a. Adjunction f u => f a -> a
    extractL = (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 :: forall (f :: * -> *) (u :: * -> *) a.
    Adjunction f u =>
    f a -> f (f a)
    duplicateL f a
    as = f a
    as f a -> f a -> f (f a)
    forall a b. a -> f b -> f a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ f a
    as

    -- | A right adjoint functor admits an intrinsic
    -- notion of zipping
    zipR :: Adjunction f u => (u a, u b) -> u (a, b)
    zipR :: forall (f :: * -> *) (u :: * -> *) a b.
    Adjunction f u =>
    (u a, u b) -> u (a, b)
    zipR = (f (u a, u b) -> (a, b)) -> (u a, u b) -> u (a, b)
    forall a b. (f a -> b) -> a -> u 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 a b. (a -> u b) -> f a -> b
    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 b c c'. (b -> c) -> (b -> c') -> b -> (c, c')
    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 a b. (a -> u b) -> f a -> 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)

    -- | Every functor in Haskell permits unzipping
    unzipR :: Functor u => u (a, b) -> (u a, u b)
    unzipR :: forall (u :: * -> *) a b. Functor u => u (a, b) -> (u a, u b)
    unzipR = ((a, b) -> a) -> u (a, b) -> u a
    forall a b. (a -> b) -> u a -> u b
    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 b c c'. (b -> c) -> (b -> c') -> b -> (c, c')
    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 a b. (a -> b) -> u a -> 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 :: forall (f :: * -> *). Void -> f Void
    absurdL = Void -> f Void
    forall a. Void -> a
    absurd

    -- | A left adjoint must be inhabited, or we can derive bottom.
    unabsurdL :: Adjunction f u => f Void -> Void
    unabsurdL :: forall (f :: * -> *) (u :: * -> *).
    Adjunction f u =>
    f Void -> Void
    unabsurdL = (Void -> u Void) -> f Void -> Void
    forall a b. (a -> u b) -> f a -> b
    forall (f :: * -> *) (u :: * -> *) a b.
    Adjunction f u =>
    (a -> u b) -> f a -> b
    rightAdjunct Void -> u Void
    forall a. Void -> a
    absurd

    -- | And a left adjoint must be inhabited by exactly one element
    cozipL :: Adjunction f u => f (Either a b) -> Either (f a) (f b)
    cozipL :: forall (f :: * -> *) (u :: * -> *) a b.
    Adjunction f u =>
    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 a b. (a -> u b) -> f a -> 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 a b. (f a -> b) -> a -> u 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 b d c. (b -> d) -> (c -> d) -> Either b c -> d
    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 a b. (f a -> b) -> a -> u 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)

    -- | Every functor in Haskell permits 'uncozipping'
    uncozipL :: Functor f => Either (f a) (f b) -> f (Either a b)
    uncozipL :: forall (f :: * -> *) a b.
    Functor f =>
    Either (f a) (f b) -> f (Either a b)
    uncozipL = (a -> Either a b) -> f a -> f (Either a b)
    forall a b. (a -> b) -> f a -> f 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 b d c. (b -> d) -> (c -> d) -> Either b c -> d
    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 a b. (a -> b) -> f a -> f 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

    -- Requires deprecated Impredicative types
    -- limitR :: Adjunction f u => (forall a. u a) -> u (forall a. a)
    -- limitR = leftAdjunct (rightAdjunct (\(x :: forall a. a) -> x))

    instance Adjunction ((,) e) ((->) e) where
      leftAdjunct :: forall a b. ((e, a) -> b) -> a -> e -> b
    leftAdjunct (e, a) -> b
    f a
    a e
    e      = (e, a) -> b
    f (e
    e, a
    a)
      rightAdjunct :: forall a b. (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 :: forall a b. (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 :: forall a b. (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 :: forall a. 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 a b. (f a -> b) -> a -> g b
    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 :: forall a. IdentityT f (IdentityT g a) -> a
    counit = (IdentityT g a -> g a) -> f (IdentityT g a) -> a
    forall a b. (a -> g b) -> f a -> b
    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 :: forall a. 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 a b. (a -> b) -> (e -> a) -> e -> b
    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 a b. (w a -> b) -> a -> m b
    forall (f :: * -> *) (u :: * -> *) a b.
    Adjunction f u =>
    (f a -> b) -> a -> u b
    leftAdjunct
      counit :: forall a. 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 a b. (a -> m b) -> w a -> b
    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 :: forall a. 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 a b. (m a -> b) -> a -> w b
    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 a b. (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (\a
    a -> (a
    a, s
    s)) m a
    ma))
      counit :: forall a. WriterT s m (TracedT s w a) -> a
    counit = ((TracedT s w a, s) -> w a) -> m (TracedT s w a, s) -> a
    forall a b. (a -> w b) -> m a -> b
    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 :: forall a. 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 a b. (f a -> b) -> a -> g b
    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 a b. (f' a -> b) -> a -> g' b
    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 :: forall a. Compose f' f (Compose g g' a) -> a
    counit = (f (Compose g g' a) -> g' a) -> f' (f (Compose g g' a)) -> a
    forall a b. (a -> g' b) -> f' a -> b
    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 a b. (a -> g b) -> f a -> b
    forall (f :: * -> *) (u :: * -> *) a b.
    Adjunction f u =>
    (a -> u b) -> f a -> b
    rightAdjunct Compose g g' a -> g (g' a)
    forall {k1} {k2} (f :: k1 -> *) (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} {k2} (f :: k1 -> *) (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 :: forall a. 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 a b. (f a -> b) -> a -> g b
    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 a b. (f' a -> b) -> a -> g' b
    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 :: forall a. 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 a b. (a -> g b) -> f a -> b
    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 a b. (a -> g' b) -> f' a -> b
    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 :: forall a. a -> Cofree u (Free f a)
    unit a
    a = a -> Free f a
    forall 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 a b. (Free f a -> b) -> a -> Cofree u b
    forall (f :: * -> *) (u :: * -> *) a b.
    Adjunction f u =>
    (f a -> b) -> a -> u b
    leftAdjunct (f (Free f a) -> Free f a
    forall a. 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 :: forall a. Free f (Cofree u a) -> a
    counit (Pure Cofree u a
    a) = Cofree u a -> a
    forall 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 a b. (a -> Cofree u b) -> Free f a -> b
    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 a. 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 :: forall a. a -> U1 (V1 a)
    unit a
    _ = U1 (V1 a)
    forall k (p :: k). U1 p
    U1
      counit :: forall a. V1 (U1 a) -> a
    counit = V1 (U1 a) -> a
    forall a b. V1 a -> b
    absurdV1

    absurdV1 :: V1 a -> b
    absurdV1 :: forall a b. V1 a -> b
    absurdV1 V1 a
    x = case V1 a
    x of {}

    instance Adjunction Par1 Par1 where
      leftAdjunct :: forall a b. (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 :: forall a b. (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 :: forall a. 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 a b. (f a -> b) -> a -> g b
    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 :: forall a. Rec1 f (Rec1 g a) -> a
    counit = (Rec1 g a -> g a) -> f (Rec1 g a) -> a
    forall a b. (a -> g b) -> f a -> b
    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

    -- @i@ and @c@ indexes have to be the same due functional dependency.
    -- But we want them to be different, therefore we rather not define this instance
    {-
    instance Adjunction f g => Adjunction (M1 i c f) (M1 i c g) where
      unit   = M1 . leftAdjunct M1
      counit = rightAdjunct unM1 . unM1
    -}

    instance (Adjunction f g, Adjunction f' g') => Adjunction (f' :.: f) (g :.: g') where
      unit :: forall a. 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 a b. (f a -> b) -> a -> g b
    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 a b. (f' a -> b) -> a -> g' b
    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 :: forall a. (:.:) f' f ((:.:) g g' a) -> a
    counit = (f ((:.:) g g' a) -> g' a) -> f' (f ((:.:) g g' a)) -> a
    forall a b. (a -> g' b) -> f' a -> b
    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 a b. (a -> g b) -> f a -> b
    forall (f :: * -> *) (u :: * -> *) a b.
    Adjunction f u =>
    (a -> u b) -> f a -> b
    rightAdjunct (:.:) g g' a -> g (g' a)
    forall k2 k1 (f :: k2 -> *) (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 k1 (f :: k2 -> *) (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 :: forall a. a -> (:*:) g g' ((:+:) f f' a)
    unit a
    a = (f a -> (:+:) f f' a) -> a -> g ((:+:) f f' a)
    forall a b. (f a -> b) -> a -> g b
    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 a b. (f' a -> b) -> a -> g' b
    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 :: forall a. (:+:) f f' ((:*:) g g' a) -> a
    counit (L1 f ((:*:) g g' a)
    l) = ((:*:) g g' a -> g a) -> f ((:*:) g g' a) -> a
    forall a b. (a -> g b) -> f a -> b
    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 a b. (a -> g' b) -> f' a -> b
    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