    {-# LANGUAGE MultiParamTypeClasses #-}
    -----------------------------------------------------------------------------
    -- |
    -- Module      :  Control.Monad.Trans.Contravariant.Adjoint
    -- Copyright   :  (C) 2011 Edward Kmett
    -- License     :  BSD-style (see the file LICENSE)
    --
    -- Maintainer  :  Edward Kmett <ekmett@gmail.com>
    -- Stability   :  provisional
    -- Portability :  MPTCs, fundeps
    --
    -- Uses a contravariant adjunction:
    --
    -- f -| g : Hask^op -> Hask
    --
    -- to build a 'Comonad' to 'Monad' transformer. Sadly, the dual construction,
    -- which builds a 'Comonad' out of a 'Monad', is uninhabited, because any
    -- 'Adjunction' of the form
    --
    -- > f -| g : Hask -> Hask^op
    --
    -- would trivially admit unsafePerformIO.
    --
    ----------------------------------------------------------------------------

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

    import Prelude hiding (sequence)
    import Control.Comonad
    import Control.Monad (ap)
    import Data.Functor.Identity
    import Data.Functor.Contravariant
    import Data.Functor.Contravariant.Adjunction

    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 -> g (w (f a))
    runAdjointT :: g (w (f a)) }

    adjoint :: Contravariant g => g (f a) -> Adjoint f g a
    adjoint :: forall (g :: * -> *) (f :: * -> *) a.
    Contravariant g =>
    g (f a) -> Adjoint f g a
    adjoint = g (Identity (f a)) -> AdjointT f g Identity a
    forall (f :: * -> *) (g :: * -> *) (w :: * -> *) a.
    g (w (f a)) -> AdjointT f g w a
    AdjointT (g (Identity (f a)) -> AdjointT f g Identity a)
    -> (g (f a) -> g (Identity (f a)))
    -> g (f a)
    -> AdjointT f g Identity a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Identity (f a) -> f a) -> g (f a) -> g (Identity (f a))
    forall a' a. (a' -> a) -> g a -> g a'
    forall (f :: * -> *) a' a.
    Contravariant f =>
    (a' -> a) -> f a -> f a'
    contramap Identity (f a) -> f a
    forall a. Identity a -> a
    runIdentity

    runAdjoint :: Contravariant g => Adjoint f g a -> g (f a)
    runAdjoint :: forall (g :: * -> *) (f :: * -> *) a.
    Contravariant g =>
    Adjoint f g a -> g (f a)
    runAdjoint = (f a -> Identity (f a)) -> g (Identity (f a)) -> g (f a)
    forall a' a. (a' -> a) -> g a -> g a'
    forall (f :: * -> *) a' a.
    Contravariant f =>
    (a' -> a) -> f a -> f a'
    contramap f a -> Identity (f a)
    forall a. a -> Identity a
    Identity (g (Identity (f a)) -> g (f a))
    -> (Adjoint f g a -> g (Identity (f a)))
    -> Adjoint f g a
    -> g (f a)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Adjoint f g a -> g (Identity (f a))
    forall (f :: * -> *) (g :: * -> *) (w :: * -> *) a.
    AdjointT f g w a -> g (w (f 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 g (w (f a))
    g) = g (w (f b)) -> AdjointT f g w b
    forall (f :: * -> *) (g :: * -> *) (w :: * -> *) a.
    g (w (f a)) -> AdjointT f g w a
    AdjointT (g (w (f b)) -> AdjointT f g w b)
    -> g (w (f b)) -> AdjointT f g w b
    forall a b. (a -> b) -> a -> b
    $ (w (f b) -> w (f a)) -> g (w (f a)) -> g (w (f b))
    forall a' a. (a' -> a) -> g a -> g a'
    forall (f :: * -> *) a' a.
    Contravariant f =>
    (a' -> a) -> f a -> f a'
    contramap ((f b -> f a) -> w (f b) -> w (f 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) -> f b -> f a
    forall a' a. (a' -> a) -> f a -> f a'
    forall (f :: * -> *) a' a.
    Contravariant f =>
    (a' -> a) -> f a -> f a'
    contramap a -> b
    f)) g (w (f a))
    g

    instance (Adjunction f g, Comonad w) => Applicative (AdjointT f g w) where
      pure :: forall a. a -> AdjointT f g w a
    pure = g (w (f a)) -> AdjointT f g w a
    forall (f :: * -> *) (g :: * -> *) (w :: * -> *) a.
    g (w (f a)) -> AdjointT f g w a
    AdjointT (g (w (f a)) -> AdjointT f g w a)
    -> (a -> g (w (f a))) -> a -> AdjointT f g w a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (w (f a) -> f a) -> a -> g (w (f a))
    forall b a. (b -> f a) -> a -> g b
    forall (f :: * -> *) (g :: * -> *) b a.
    Adjunction f g =>
    (b -> f a) -> a -> g b
    leftAdjunct w (f a) -> f a
    forall a. w a -> a
    forall (w :: * -> *) a. Comonad w => w a -> a
    extract
      <*> :: forall a b.
    AdjointT f g w (a -> b) -> AdjointT f g w a -> AdjointT f g w b
    (<*>) = AdjointT f g w (a -> b) -> AdjointT f g w a -> AdjointT f g w b
    forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
    ap

    instance (Adjunction f g, Comonad w) => Monad (AdjointT f g w) where
      return :: forall a. a -> AdjointT f g w a
    return = a -> AdjointT f g w a
    forall a. a -> AdjointT f g w a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure
      AdjointT g (w (f a))
    m >>= :: forall a b.
    AdjointT f g w a -> (a -> AdjointT f g w b) -> AdjointT f g w b
    >>= a -> AdjointT f g w b
    f = g (w (f b)) -> AdjointT f g w b
    forall (f :: * -> *) (g :: * -> *) (w :: * -> *) a.
    g (w (f a)) -> AdjointT f g w a
    AdjointT (g (w (f b)) -> AdjointT f g w b)
    -> g (w (f b)) -> AdjointT f g w b
    forall a b. (a -> b) -> a -> b
    $ (w (f b) -> w (f a)) -> g (w (f a)) -> g (w (f b))
    forall a' a. (a' -> a) -> g a -> g a'
    forall (f :: * -> *) a' a.
    Contravariant f =>
    (a' -> a) -> f a -> f a'
    contramap ((w (f b) -> f a) -> w (f b) -> w (f a)
    forall a b. (w a -> b) -> w a -> w b
    forall (w :: * -> *) a b. Comonad w => (w a -> b) -> w a -> w b
    extend ((a -> g (w (f b))) -> w (f b) -> f a
    forall a b. (a -> g b) -> b -> f a
    forall (f :: * -> *) (g :: * -> *) a b.
    Adjunction f g =>
    (a -> g b) -> b -> f a
    rightAdjunct (AdjointT f g w b -> g (w (f b))
    forall (f :: * -> *) (g :: * -> *) (w :: * -> *) a.
    AdjointT f g w a -> g (w (f a))
    runAdjointT (AdjointT f g w b -> g (w (f b)))
    -> (a -> AdjointT f g w b) -> a -> g (w (f b))
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> AdjointT f g w b
    f))) g (w (f a))
    m