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

{-# LANGUAGE CPP #-}
#if __GLASGOW_HASKELL__ >= 702
{-# LANGUAGE Trustworthy #-}
#endif
#if __GLASGOW_HASKELL__ >= 708
{-# LANGUAGE EmptyCase #-}
#endif

-------------------------------------------------------------------------------------------
-- |
-- 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

#if __GLASGOW_HASKELL__ < 710
import Control.Applicative
#endif
import Control.Arrow ((&&&), (|||))
import Control.Monad.Free
#if __GLASGOW_HASKELL__ < 707
import Control.Monad.Instances ()
#endif
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
#if __GLASGOW_HASKELL__ >= 708
  {-# MINIMAL (unit, counit) | (leftAdjunct, rightAdjunct) #-}
#endif
  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 (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 (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 (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 (f :: * -> *) (u :: * -> *) a.
Adjunction f u =>
a -> u (f a)
unit
  rightAdjunct a -> u b
f = f (u b) -> b
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 (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 :: 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 (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 (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 (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (c -> u d) -> f c -> d
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 :: (f () -> b) -> u b
tabulateAdjunction f () -> b
f = (f () -> b) -> () -> 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 :: u b -> f a -> b
indexAdjunction = (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 :: (a -> b -> c) -> u a -> f b -> c
zapWithAdjunction a -> b -> c
f u a
ua = (b -> u c) -> f b -> c
forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(a -> u b) -> f a -> b
rightAdjunct (\b
b -> (a -> c) -> u a -> u c
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 :: f a -> (a, f ())
splitL = (a -> u (a, f ())) -> f a -> (a, f ())
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 (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 :: a -> f () -> f a
unsplitL = a -> f () -> f a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
(<$)

extractL :: Adjunction f u => f a -> a
extractL :: 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 :: f a -> f (f a)
duplicateL f a
as = f a
as f a -> f a -> f (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 :: (u a, u b) -> u (a, b)
zipR = (f (u a, u b) -> (a, b)) -> (u a, u b) -> u (a, 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 (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 (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 (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 :: u (a, b) -> (u a, u b)
unzipR = ((a, b) -> a) -> u (a, b) -> u a
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 (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 (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 :: 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 :: f Void -> Void
unabsurdL = (Void -> u Void) -> f Void -> Void
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 :: 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 (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 (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 (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 (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 :: Either (f a) (f b) -> f (Either a b)
uncozipL = (a -> Either a b) -> f a -> f (Either a 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 (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 (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 :: ((e, a) -> b) -> a -> e -> b
leftAdjunct (e, a) -> b
f a
a e
e      = (e, a) -> b
f (e
e, a
a)
  rightAdjunct :: (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 :: (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 :: (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 :: 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 (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 :: IdentityT f (IdentityT g a) -> a
counit = (IdentityT g a -> g a) -> f (IdentityT g a) -> a
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 :: 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 (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 (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(f a -> b) -> a -> u b
leftAdjunct
  counit :: 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 (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 :: 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 (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 (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\a
a -> (a
a, s
s)) m a
ma))
  counit :: WriterT s m (TracedT s w a) -> a
counit = ((TracedT s w a, s) -> w a) -> m (TracedT s w a, s) -> a
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 :: 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 (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 (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 :: Compose f' f (Compose g g' a) -> a
counit = (f (Compose g g' a) -> g' a) -> f' (f (Compose g g' a)) -> a
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 (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(a -> u b) -> f a -> b
rightAdjunct Compose g g' a -> g (g' a)
forall k1 (f :: k1 -> *) k2 (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 (f :: k1 -> *) k2 (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 :: 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 (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 (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 :: 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 (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 (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 :: a -> Cofree u (Free f a)
unit a
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 (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(f a -> b) -> a -> u b
leftAdjunct (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 :: Free f (Cofree u a) -> a
counit (Pure Cofree u a
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 (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 (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 :: a -> U1 (V1 a)
unit a
_ = U1 (V1 a)
forall k (p :: k). U1 p
U1
  counit :: V1 (U1 a) -> a
counit = V1 (U1 a) -> a
forall a b. V1 a -> b
absurdV1

absurdV1 :: V1 a -> b
#if __GLASGOW_HASKELL__ >= 708
absurdV1 :: V1 a -> b
absurdV1 V1 a
x = case V1 a
x of {}
#else
absurdV1 x = x `seq` undefined
#endif

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