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

    module Data.Functor.Contravariant.Adjunction
      ( Adjunction(..)
      , adjuncted
      , contrarepAdjunction
      , coindexAdjunction
      ) where

    import Data.Functor.Contravariant
    import Data.Functor.Contravariant.Rep
    import Data.Profunctor

    -- | An adjunction from @Hask^op@ to @Hask@
    --
    -- @'Op' (f a) b ~ 'Hask' a (g b)@
    --
    -- @
    -- 'rightAdjunct' 'unit' = 'id'
    -- 'leftAdjunct' 'counit' = 'id'
    -- @
    --
    -- Any adjunction from @Hask@ to @Hask^op@ would indirectly
    -- permit @unsafePerformIO@, and therefore does not exist.

    class (Contravariant f, Representable g) => Adjunction f g | f -> g, g -> f where
      {-# MINIMAL (unit, counit) | (leftAdjunct, rightAdjunct) #-}
      unit :: a -> g (f a) -- monad in Hask
      counit :: a -> f (g a) -- comonad in Hask^op
      leftAdjunct  :: (b -> f a) -> a -> g b
      rightAdjunct :: (a -> g b) -> b -> f a

      unit = (f a -> f a) -> a -> g (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 f a -> f a
    forall a. a -> a
    id
      counit = (g a -> g a) -> a -> f (g 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 g a -> g a
    forall a. a -> a
    id
      leftAdjunct b -> f a
    f = (b -> f a) -> g (f a) -> g b
    forall a' a. (a' -> a) -> g a -> g a'
    forall (f :: * -> *) a' a.
    Contravariant f =>
    (a' -> a) -> f a -> f a'
    contramap b -> f a
    f (g (f a) -> g b) -> (a -> g (f a)) -> a -> g b
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> g (f a)
    forall a. a -> g (f a)
    forall (f :: * -> *) (g :: * -> *) a.
    Adjunction f g =>
    a -> g (f a)
    unit
      rightAdjunct a -> g b
    f = (a -> g b) -> f (g 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 -> g b
    f (f (g b) -> f a) -> (b -> f (g b)) -> b -> f a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . b -> f (g b)
    forall a. a -> f (g a)
    forall (f :: * -> *) (g :: * -> *) a.
    Adjunction f g =>
    a -> f (g a)
    counit

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

    -- | This 'Adjunction' gives rise to the @Cont@ 'Monad'
    instance Adjunction (Op r) (Op r) where
      unit :: forall a. a -> Op r (Op r a)
    unit a
    a = (Op r a -> r) -> Op r (Op r a)
    forall a b. (b -> a) -> Op a b
    Op (\Op r a
    k -> Op r a -> a -> r
    forall a b. Op a b -> b -> a
    getOp Op r a
    k a
    a)
      counit :: forall a. a -> Op r (Op r a)
    counit = a -> Op r (Op r a)
    forall a. a -> Op r (Op r a)
    forall (f :: * -> *) (g :: * -> *) a.
    Adjunction f g =>
    a -> g (f a)
    unit

    -- | This gives rise to the @Cont Bool@ 'Monad'
    instance Adjunction Predicate Predicate where
      unit :: forall a. a -> Predicate (Predicate a)
    unit a
    a = (Predicate a -> Bool) -> Predicate (Predicate a)
    forall a. (a -> Bool) -> Predicate a
    Predicate (\Predicate a
    k -> Predicate a -> a -> Bool
    forall a. Predicate a -> a -> Bool
    getPredicate Predicate a
    k a
    a)
      counit :: forall a. a -> Predicate (Predicate a)
    counit = a -> Predicate (Predicate a)
    forall a. a -> Predicate (Predicate a)
    forall (f :: * -> *) (g :: * -> *) a.
    Adjunction f g =>
    a -> g (f a)
    unit

    -- | Represent a 'Contravariant' functor that has a left adjoint
    contrarepAdjunction :: Adjunction f g => (a -> f ()) -> g a
    contrarepAdjunction :: forall (f :: * -> *) (g :: * -> *) a.
    Adjunction f g =>
    (a -> f ()) -> g a
    contrarepAdjunction = ((a -> f ()) -> () -> g a) -> () -> (a -> f ()) -> g a
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip (a -> f ()) -> () -> g 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 ()

    coindexAdjunction :: Adjunction f g => g a -> a -> f ()
    coindexAdjunction :: forall (f :: * -> *) (g :: * -> *) a.
    Adjunction f g =>
    g a -> a -> f ()
    coindexAdjunction = (() -> g a) -> a -> f ()
    forall a b. (a -> g b) -> b -> f a
    forall (f :: * -> *) (g :: * -> *) a b.
    Adjunction f g =>
    (a -> g b) -> b -> f a
    rightAdjunct ((() -> g a) -> a -> f ())
    -> (g a -> () -> g a) -> g a -> a -> f ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . g a -> () -> g a
    forall a b. a -> b -> a
    const