{-# LANGUAGE CPP #-}
{-# LANGUAGE MultiParamTypeClasses #-}
#if __GLASGOW_HASKELL__ >= 702 && __GLASGOW_HASKELL__ < 710
{-# LANGUAGE Trustworthy #-}
#endif
-----------------------------------------------------------------------------
-- |
-- Copyright   :  (C) 2011-2013 Edward Kmett
-- License     :  BSD-style (see the file LICENSE)
--
-- Maintainer  :  Edward Kmett <ekmett@gmail.com>
-- Stability   :  provisional
-- Portability :  MPTCs, fundeps
--
----------------------------------------------------------------------------

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

import Prelude hiding (sequence)
#if __GLASGOW_HASKELL__ < 710
import Control.Applicative
#endif
import Control.Comonad
import Control.Comonad.Trans.Class
import Data.Functor.Adjunction
import Data.Functor.Extend
import Data.Functor.Identity
import Data.Distributive

type Adjoint f g = AdjointT f g Identity

newtype AdjointT f g w a = AdjointT { AdjointT f g w a -> f (w (g a))
runAdjointT :: f (w (g a)) }

adjoint :: Functor f => f (g a) -> Adjoint f g a
adjoint :: f (g a) -> Adjoint f g a
adjoint = f (Identity (g a)) -> Adjoint f g a
forall (f :: * -> *) (g :: * -> *) (w :: * -> *) a.
f (w (g a)) -> AdjointT f g w a
AdjointT (f (Identity (g a)) -> Adjoint f g a)
-> (f (g a) -> f (Identity (g a))) -> f (g a) -> Adjoint f g a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (g a -> Identity (g a)) -> f (g a) -> f (Identity (g a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap g a -> Identity (g a)
forall a. a -> Identity a
Identity

runAdjoint :: Functor f => Adjoint f g a -> f (g a)
runAdjoint :: Adjoint f g a -> f (g a)
runAdjoint = (Identity (g a) -> g a) -> f (Identity (g a)) -> f (g a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Identity (g a) -> g a
forall a. Identity a -> a
runIdentity (f (Identity (g a)) -> f (g a))
-> (Adjoint f g a -> f (Identity (g a)))
-> Adjoint f g a
-> f (g a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Adjoint f g a -> f (Identity (g a))
forall (f :: * -> *) (g :: * -> *) (w :: * -> *) a.
AdjointT f g w a -> f (w (g a))
runAdjointT

instance (Adjunction f g, Functor w) => Functor (AdjointT f g w) where
  fmap :: (a -> b) -> AdjointT f g w a -> AdjointT f g w b
fmap a -> b
f (AdjointT f (w (g a))
g) = f (w (g b)) -> AdjointT f g w b
forall (f :: * -> *) (g :: * -> *) (w :: * -> *) a.
f (w (g a)) -> AdjointT f g w a
AdjointT (f (w (g b)) -> AdjointT f g w b)
-> f (w (g b)) -> AdjointT f g w b
forall a b. (a -> b) -> a -> b
$ (w (g a) -> w (g b)) -> f (w (g a)) -> f (w (g b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((g a -> g b) -> w (g a) -> w (g b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> b) -> g a -> g b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f)) f (w (g a))
g
  a
b <$ :: a -> AdjointT f g w b -> AdjointT f g w a
<$ (AdjointT f (w (g b))
g) = f (w (g a)) -> AdjointT f g w a
forall (f :: * -> *) (g :: * -> *) (w :: * -> *) a.
f (w (g a)) -> AdjointT f g w a
AdjointT (f (w (g a)) -> AdjointT f g w a)
-> f (w (g a)) -> AdjointT f g w a
forall a b. (a -> b) -> a -> b
$ (w (g b) -> w (g a)) -> f (w (g b)) -> f (w (g a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((g b -> g a) -> w (g b) -> w (g a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (a
b a -> g b -> g a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$)) f (w (g b))
g

instance (Adjunction f g, Extend w) => Extend (AdjointT f g w) where
  extended :: (AdjointT f g w a -> b) -> AdjointT f g w a -> AdjointT f g w b
extended AdjointT f g w a -> b
f (AdjointT f (w (g a))
m) = f (w (g b)) -> AdjointT f g w b
forall (f :: * -> *) (g :: * -> *) (w :: * -> *) a.
f (w (g a)) -> AdjointT f g w a
AdjointT (f (w (g b)) -> AdjointT f g w b)
-> f (w (g b)) -> AdjointT f g w b
forall a b. (a -> b) -> a -> b
$ (w (g a) -> w (g b)) -> f (w (g a)) -> f (w (g b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((w (g a) -> g b) -> w (g a) -> w (g b)
forall (w :: * -> *) a b. Extend w => (w a -> b) -> w a -> w b
extended ((w (g a) -> g b) -> w (g a) -> w (g b))
-> (w (g a) -> g b) -> w (g a) -> w (g b)
forall a b. (a -> b) -> a -> b
$ (f (w (g a)) -> b) -> w (g a) -> g b
forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(f a -> b) -> a -> u b
leftAdjunct (AdjointT f g w a -> b
f (AdjointT f g w a -> b)
-> (f (w (g a)) -> AdjointT f g w a) -> f (w (g a)) -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (w (g a)) -> AdjointT f g w a
forall (f :: * -> *) (g :: * -> *) (w :: * -> *) a.
f (w (g a)) -> AdjointT f g w a
AdjointT)) f (w (g a))
m

instance (Adjunction f g, Comonad w) => Comonad (AdjointT f g w) where
  extend :: (AdjointT f g w a -> b) -> AdjointT f g w a -> AdjointT f g w b
extend AdjointT f g w a -> b
f (AdjointT f (w (g a))
m) = f (w (g b)) -> AdjointT f g w b
forall (f :: * -> *) (g :: * -> *) (w :: * -> *) a.
f (w (g a)) -> AdjointT f g w a
AdjointT (f (w (g b)) -> AdjointT f g w b)
-> f (w (g b)) -> AdjointT f g w b
forall a b. (a -> b) -> a -> b
$ (w (g a) -> w (g b)) -> f (w (g a)) -> f (w (g b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((w (g a) -> g b) -> w (g a) -> w (g b)
forall (w :: * -> *) a b. Comonad w => (w a -> b) -> w a -> w b
extend ((w (g a) -> g b) -> w (g a) -> w (g b))
-> (w (g a) -> g b) -> w (g a) -> w (g b)
forall a b. (a -> b) -> a -> b
$ (f (w (g a)) -> b) -> w (g a) -> g b
forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(f a -> b) -> a -> u b
leftAdjunct (AdjointT f g w a -> b
f (AdjointT f g w a -> b)
-> (f (w (g a)) -> AdjointT f g w a) -> f (w (g a)) -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (w (g a)) -> AdjointT f g w a
forall (f :: * -> *) (g :: * -> *) (w :: * -> *) a.
f (w (g a)) -> AdjointT f g w a
AdjointT)) f (w (g a))
m
  extract :: AdjointT f g w a -> a
extract = (w (g a) -> g a) -> f (w (g a)) -> a
forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(a -> u b) -> f a -> b
rightAdjunct w (g a) -> g a
forall (w :: * -> *) a. Comonad w => w a -> a
extract (f (w (g a)) -> a)
-> (AdjointT f g w a -> f (w (g a))) -> AdjointT f g w a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AdjointT f g w a -> f (w (g a))
forall (f :: * -> *) (g :: * -> *) (w :: * -> *) a.
AdjointT f g w a -> f (w (g a))
runAdjointT

{-
instance (Adjunction f g, Monad m) => Applicative (AdjointT f g m) where
  pure = AdjointT . leftAdjunct return
  (<*>) = ap
-}

instance (Adjunction f g, Distributive g) => ComonadTrans (AdjointT f g) where
  lower :: AdjointT f g w a -> w a
lower = f (g (w a)) -> w a
forall (f :: * -> *) (u :: * -> *) a.
Adjunction f u =>
f (u a) -> a
counit (f (g (w a)) -> w a)
-> (AdjointT f g w a -> f (g (w a))) -> AdjointT f g w a -> w a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (w (g a) -> g (w a)) -> f (w (g a)) -> f (g (w a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap w (g a) -> g (w a)
forall (g :: * -> *) (f :: * -> *) a.
(Distributive g, Functor f) =>
f (g a) -> g (f a)
distribute (f (w (g a)) -> f (g (w a)))
-> (AdjointT f g w a -> f (w (g a)))
-> AdjointT f g w a
-> f (g (w a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AdjointT f g w a -> f (w (g a))
forall (f :: * -> *) (g :: * -> *) (w :: * -> *) a.
AdjointT f g w a -> f (w (g a))
runAdjointT