    {-# LANGUAGE MultiParamTypeClasses #-}
    -----------------------------------------------------------------------------
    -- |
    -- Copyright   :  (C) 2011-2013 Edward Kmett
    -- License     :  BSD-style (see the file LICENSE)
    --
    -- Maintainer  :  Edward Kmett <ekmett@gmail.com>
    -- Stability   :  provisional
    -- Portability :  MPTCs, fundeps
    --
    ----------------------------------------------------------------------------

    module Control.Comonad.Trans.Adjoint
      ( Adjoint
      , runAdjoint
      , adjoint
      , AdjointT(..)
      ) where

    import Prelude hiding (sequence)
    import Control.Comonad
    import Control.Comonad.Trans.Class
    import Data.Functor.Adjunction
    import Data.Functor.Extend
    import Data.Functor.Identity
    import Data.Distributive

    type Adjoint f g = AdjointT f g Identity

    newtype AdjointT f g w a = AdjointT { forall (f :: * -> *) (g :: * -> *) (w :: * -> *) a.
    AdjointT f g w a -> f (w (g a))
    runAdjointT :: f (w (g a)) }

    adjoint :: Functor f => f (g a) -> Adjoint f g a
    adjoint :: forall (f :: * -> *) (g :: * -> *) a.
    Functor f =>
    f (g a) -> Adjoint f g a
    adjoint = f (Identity (g a)) -> AdjointT f g Identity a
    forall (f :: * -> *) (g :: * -> *) (w :: * -> *) a.
    f (w (g a)) -> AdjointT f g w a
    AdjointT (f (Identity (g a)) -> AdjointT f g Identity a)
    -> (f (g a) -> f (Identity (g a)))
    -> f (g a)
    -> AdjointT f g Identity a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (g a -> Identity (g a)) -> f (g a) -> f (Identity (g a))
    forall a b. (a -> b) -> f a -> f b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap g a -> Identity (g a)
    forall a. a -> Identity a
    Identity

    runAdjoint :: Functor f => Adjoint f g a -> f (g a)
    runAdjoint :: forall (f :: * -> *) (g :: * -> *) a.
    Functor f =>
    Adjoint f g a -> f (g a)
    runAdjoint = (Identity (g a) -> g a) -> f (Identity (g a)) -> f (g a)
    forall a b. (a -> b) -> f a -> f b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Identity (g a) -> g a
    forall a. Identity a -> a
    runIdentity (f (Identity (g a)) -> f (g a))
    -> (Adjoint f g a -> f (Identity (g a)))
    -> Adjoint f g a
    -> f (g a)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Adjoint f g a -> f (Identity (g a))
    forall (f :: * -> *) (g :: * -> *) (w :: * -> *) a.
    AdjointT f g w a -> f (w (g a))
    runAdjointT

    instance (Adjunction f g, Functor w) => Functor (AdjointT f g w) where
      fmap :: forall a b. (a -> b) -> AdjointT f g w a -> AdjointT f g w b
    fmap a -> b
    f (AdjointT f (w (g a))
    g) = f (w (g b)) -> AdjointT f g w b
    forall (f :: * -> *) (g :: * -> *) (w :: * -> *) a.
    f (w (g a)) -> AdjointT f g w a
    AdjointT (f (w (g b)) -> AdjointT f g w b)
    -> f (w (g b)) -> AdjointT f g w b
    forall a b. (a -> b) -> a -> b
    $ (w (g a) -> w (g b)) -> f (w (g a)) -> f (w (g b))
    forall a b. (a -> b) -> f a -> f b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((g a -> g b) -> w (g a) -> w (g b)
    forall a b. (a -> b) -> w a -> w b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((a -> b) -> g a -> g b
    forall a b. (a -> b) -> g a -> g b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap a -> b
    f)) f (w (g a))
    g
      a
    b <$ :: forall a b. a -> AdjointT f g w b -> AdjointT f g w a
    <$ (AdjointT f (w (g b))
    g) = f (w (g a)) -> AdjointT f g w a
    forall (f :: * -> *) (g :: * -> *) (w :: * -> *) a.
    f (w (g a)) -> AdjointT f g w a
    AdjointT (f (w (g a)) -> AdjointT f g w a)
    -> f (w (g a)) -> AdjointT f g w a
    forall a b. (a -> b) -> a -> b
    $ (w (g b) -> w (g a)) -> f (w (g b)) -> f (w (g a))
    forall a b. (a -> b) -> f a -> f b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((g b -> g a) -> w (g b) -> w (g a)
    forall a b. (a -> b) -> w a -> w b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (a
    b a -> g b -> g a
    forall a b. a -> g b -> g a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$)) f (w (g b))
    g

    instance (Adjunction f g, Extend w) => Extend (AdjointT f g w) where
      extended :: forall a b.
    (AdjointT f g w a -> b) -> AdjointT f g w a -> AdjointT f g w b
    extended AdjointT f g w a -> b
    f (AdjointT f (w (g a))
    m) = f (w (g b)) -> AdjointT f g w b
    forall (f :: * -> *) (g :: * -> *) (w :: * -> *) a.
    f (w (g a)) -> AdjointT f g w a
    AdjointT (f (w (g b)) -> AdjointT f g w b)
    -> f (w (g b)) -> AdjointT f g w b
    forall a b. (a -> b) -> a -> b
    $ (w (g a) -> w (g b)) -> f (w (g a)) -> f (w (g b))
    forall a b. (a -> b) -> f a -> f b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((w (g a) -> g b) -> w (g a) -> w (g b)
    forall a b. (w a -> b) -> w a -> w b
    forall (w :: * -> *) a b. Extend w => (w a -> b) -> w a -> w b
    extended ((w (g a) -> g b) -> w (g a) -> w (g b))
    -> (w (g a) -> g b) -> w (g a) -> w (g b)
    forall a b. (a -> b) -> a -> b
    $ (f (w (g a)) -> b) -> w (g a) -> g b
    forall a b. (f a -> b) -> a -> g b
    forall (f :: * -> *) (u :: * -> *) a b.
    Adjunction f u =>
    (f a -> b) -> a -> u b
    leftAdjunct (AdjointT f g w a -> b
    f (AdjointT f g w a -> b)
    -> (f (w (g a)) -> AdjointT f g w a) -> f (w (g a)) -> b
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . f (w (g a)) -> AdjointT f g w a
    forall (f :: * -> *) (g :: * -> *) (w :: * -> *) a.
    f (w (g a)) -> AdjointT f g w a
    AdjointT)) f (w (g a))
    m

    instance (Adjunction f g, Comonad w) => Comonad (AdjointT f g w) where
      extend :: forall a b.
    (AdjointT f g w a -> b) -> AdjointT f g w a -> AdjointT f g w b
    extend AdjointT f g w a -> b
    f (AdjointT f (w (g a))
    m) = f (w (g b)) -> AdjointT f g w b
    forall (f :: * -> *) (g :: * -> *) (w :: * -> *) a.
    f (w (g a)) -> AdjointT f g w a
    AdjointT (f (w (g b)) -> AdjointT f g w b)
    -> f (w (g b)) -> AdjointT f g w b
    forall a b. (a -> b) -> a -> b
    $ (w (g a) -> w (g b)) -> f (w (g a)) -> f (w (g b))
    forall a b. (a -> b) -> f a -> f b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((w (g a) -> g b) -> w (g a) -> w (g b)
    forall a b. (w a -> b) -> w a -> w b
    forall (w :: * -> *) a b. Comonad w => (w a -> b) -> w a -> w b
    extend ((w (g a) -> g b) -> w (g a) -> w (g b))
    -> (w (g a) -> g b) -> w (g a) -> w (g b)
    forall a b. (a -> b) -> a -> b
    $ (f (w (g a)) -> b) -> w (g a) -> g b
    forall a b. (f a -> b) -> a -> g b
    forall (f :: * -> *) (u :: * -> *) a b.
    Adjunction f u =>
    (f a -> b) -> a -> u b
    leftAdjunct (AdjointT f g w a -> b
    f (AdjointT f g w a -> b)
    -> (f (w (g a)) -> AdjointT f g w a) -> f (w (g a)) -> b
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . f (w (g a)) -> AdjointT f g w a
    forall (f :: * -> *) (g :: * -> *) (w :: * -> *) a.
    f (w (g a)) -> AdjointT f g w a
    AdjointT)) f (w (g a))
    m
      extract :: forall a. AdjointT f g w a -> a
    extract = (w (g a) -> g a) -> f (w (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 w (g a) -> g a
    forall a. w a -> a
    forall (w :: * -> *) a. Comonad w => w a -> a
    extract (f (w (g a)) -> a)
    -> (AdjointT f g w a -> f (w (g a))) -> AdjointT f g w a -> a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . AdjointT f g w a -> f (w (g a))
    forall (f :: * -> *) (g :: * -> *) (w :: * -> *) a.
    AdjointT f g w a -> f (w (g a))
    runAdjointT

    {-
    instance (Adjunction f g, Monad m) => Applicative (AdjointT f g m) where
      pure = AdjointT . leftAdjunct return
      (<*>) = ap
    -}

    instance (Adjunction f g, Distributive g) => ComonadTrans (AdjointT f g) where
      lower :: forall (w :: * -> *) a. Comonad w => AdjointT f g w a -> w a
    lower = f (g (w a)) -> w a
    forall a. f (g a) -> a
    forall (f :: * -> *) (u :: * -> *) a.
    Adjunction f u =>
    f (u a) -> a
    counit (f (g (w a)) -> w a)
    -> (AdjointT f g w a -> f (g (w a))) -> AdjointT f g w a -> w a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (w (g a) -> g (w a)) -> f (w (g a)) -> f (g (w a))
    forall a b. (a -> b) -> f a -> f b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap w (g a) -> g (w a)
    forall (g :: * -> *) (f :: * -> *) a.
    (Distributive g, Functor f) =>
    f (g a) -> g (f a)
    forall (f :: * -> *) a. Functor f => f (g a) -> g (f a)
    distribute (f (w (g a)) -> f (g (w a)))
    -> (AdjointT f g w a -> f (w (g a)))
    -> AdjointT f g w a
    -> f (g (w a))
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . AdjointT f g w a -> f (w (g a))
    forall (f :: * -> *) (g :: * -> *) (w :: * -> *) a.
    AdjointT f g w a -> f (w (g a))
    runAdjointT