{-# LANGUAGE Rank2Types, MultiParamTypeClasses, FunctionalDependencies, UndecidableInstances #-}
{-# LANGUAGE CPP #-}
#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 702
{-# LANGUAGE Trustworthy #-}
#endif
-----------------------------------------------------------------------------
-- |
-- Copyright   :  (C) 2011-2013 Edward Kmett
-- License     :  BSD-style (see the file LICENSE)
--
-- Maintainer  :  Edward Kmett <[email protected]>
-- Stability   :  provisional
-- Portability :  MPTCs
--
----------------------------------------------------------------------------

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

#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 707
import Control.Monad.Instances ()
#endif
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
#if __GLASGOW_HASKELL__ >= 708
  {-# MINIMAL (unit, counit) | (leftAdjunct, rightAdjunct) #-}
#endif
  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 = forall (f :: * -> *) (g :: * -> *) b a.
Adjunction f g =>
(b -> f a) -> a -> g b
leftAdjunct forall a. a -> a
id
  counit = forall (f :: * -> *) (g :: * -> *) a b.
Adjunction f g =>
(a -> g b) -> b -> f a
rightAdjunct forall a. a -> a
id
  leftAdjunct b -> f a
f = forall (f :: * -> *) a' a.
Contravariant f =>
(a' -> a) -> f a -> f a'
contramap b -> f a
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) (g :: * -> *) a.
Adjunction f g =>
a -> g (f a)
unit
  rightAdjunct a -> g b
f = forall (f :: * -> *) a' a.
Contravariant f =>
(a' -> a) -> f a -> f a'
contramap a -> g b
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap forall (f :: * -> *) (g :: * -> *) b a.
Adjunction f g =>
(b -> f a) -> a -> g b
leftAdjunct (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap 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 = forall a b. (b -> a) -> Op a b
Op (\Op r a
k -> 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 = 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 = forall a. (a -> Bool) -> Predicate a
Predicate (\Predicate a
k -> forall a. Predicate a -> a -> Bool
getPredicate Predicate a
k a
a)
  counit :: forall a. a -> Predicate (Predicate a)
counit = 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 = forall a b c. (a -> b -> c) -> b -> a -> c
flip 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 = forall (f :: * -> *) (g :: * -> *) a b.
Adjunction f g =>
(a -> g b) -> b -> f a
rightAdjunct forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. a -> b -> a
const