{-# 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 a b. (f a -> b) -> a -> u b
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 a b. (a -> u b) -> f a -> b
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 a b. (a -> b) -> u 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 a. 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 a. f (u a) -> a
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 a b. (a -> b) -> f a -> f 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 :: forall (f :: * -> *) (u :: * -> *) (p :: * -> * -> *) (g :: * -> *)
       a b c d.
(Adjunction f u, Profunctor p, Functor g) =>
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 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 (f a -> b) -> a -> u b
forall a b. (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 a b. (a -> b) -> g a -> g b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (c -> u d) -> f c -> d
forall a b. (a -> u b) -> f a -> b
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 :: forall (f :: * -> *) (u :: * -> *) b.
Adjunction f u =>
(f () -> b) -> u b
tabulateAdjunction f () -> b
f = (f () -> b) -> () -> u b
forall a b. (f a -> b) -> a -> 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 :: forall (f :: * -> *) (u :: * -> *) b a.
Adjunction f u =>
u b -> f a -> b
indexAdjunction = (a -> u b) -> f a -> b
forall a b. (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 :: forall (f :: * -> *) (u :: * -> *) a b c.
Adjunction f u =>
(a -> b -> c) -> u a -> f b -> c
zapWithAdjunction a -> b -> c
f u a
ua = (b -> u c) -> f b -> c
forall a b. (a -> u b) -> f a -> b
forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(a -> u b) -> f a -> b
rightAdjunct (\b
b -> (a -> c) -> u a -> u c
forall a b. (a -> b) -> u a -> u b
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 :: forall (f :: * -> *) (u :: * -> *) a.
Adjunction f u =>
f a -> (a, f ())
splitL = (a -> u (a, f ())) -> f a -> (a, f ())
forall a b. (a -> u b) -> f a -> b
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 a b. (f a -> b) -> a -> u b
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 :: forall (f :: * -> *) a. Functor f => a -> f () -> f a
unsplitL = a -> f () -> f a
forall a b. a -> f b -> f a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
(<$)

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