{-# LANGUAGE CPP #-}
{-# LANGUAGE MultiParamTypeClasses #-}
#if __GLASGOW_HASKELL__ >= 702 && __GLASGOW_HASKELL__ < 710
{-# LANGUAGE Trustworthy #-}
#endif
-----------------------------------------------------------------------------
-- |
-- Module      :  Control.Monad.Trans.Contravariant.Adjoint
-- Copyright   :  (C) 2011 Edward Kmett
-- License     :  BSD-style (see the file LICENSE)
--
-- Maintainer  :  Edward Kmett <[email protected]>
-- Stability   :  provisional
-- Portability :  MPTCs, fundeps
--
-- Uses a contravariant adjunction:
--
-- f -| g : Hask^op -> Hask
--
-- to build a 'Comonad' to 'Monad' transformer. Sadly, the dual construction,
-- which builds a 'Comonad' out of a 'Monad', is uninhabited, because any
-- 'Adjunction' of the form
--
-- > f -| g : Hask -> Hask^op
--
-- would trivially admit unsafePerformIO.
--
----------------------------------------------------------------------------

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

import Prelude hiding (sequence)
#if __GLASGOW_HASKELL__ < 710
import Control.Applicative
#endif
import Control.Comonad
import Control.Monad (ap)
import Data.Functor.Identity
import Data.Functor.Contravariant
import Data.Functor.Contravariant.Adjunction

type Adjoint f g = AdjointT f g Identity

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

adjoint :: Contravariant g => g (f a) -> Adjoint f g a
adjoint :: forall (g :: * -> *) (f :: * -> *) a.
Contravariant g =>
g (f a) -> Adjoint f g a
adjoint = forall (f :: * -> *) (g :: * -> *) (w :: * -> *) a.
g (w (f a)) -> AdjointT f g w a
AdjointT forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a' a.
Contravariant f =>
(a' -> a) -> f a -> f a'
contramap forall a. Identity a -> a
runIdentity

runAdjoint :: Contravariant g => Adjoint f g a -> g (f a)
runAdjoint :: forall (g :: * -> *) (f :: * -> *) a.
Contravariant g =>
Adjoint f g a -> g (f a)
runAdjoint = forall (f :: * -> *) a' a.
Contravariant f =>
(a' -> a) -> f a -> f a'
contramap forall a. a -> Identity a
Identity forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) (g :: * -> *) (w :: * -> *) a.
AdjointT f g w a -> g (w (f a))
runAdjointT

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

instance (Adjunction f g, Comonad w) => Applicative (AdjointT f g w) where
  pure :: forall a. a -> AdjointT f g w a
pure = forall (f :: * -> *) (g :: * -> *) (w :: * -> *) a.
g (w (f a)) -> AdjointT f g w a
AdjointT forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) (g :: * -> *) b a.
Adjunction f g =>
(b -> f a) -> a -> g b
leftAdjunct forall (w :: * -> *) a. Comonad w => w a -> a
extract
  <*> :: forall a b.
AdjointT f g w (a -> b) -> AdjointT f g w a -> AdjointT f g w b
(<*>) = forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap

instance (Adjunction f g, Comonad w) => Monad (AdjointT f g w) where
  return :: forall a. a -> AdjointT f g w a
return = forall (f :: * -> *) a. Applicative f => a -> f a
pure
  AdjointT g (w (f a))
m >>= :: forall a b.
AdjointT f g w a -> (a -> AdjointT f g w b) -> AdjointT f g w b
>>= a -> AdjointT f g w b
f = forall (f :: * -> *) (g :: * -> *) (w :: * -> *) a.
g (w (f a)) -> AdjointT f g w a
AdjointT forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a' a.
Contravariant f =>
(a' -> a) -> f a -> f a'
contramap (forall (w :: * -> *) a b. Comonad w => (w a -> b) -> w a -> w b
extend (forall (f :: * -> *) (g :: * -> *) a b.
Adjunction f g =>
(a -> g b) -> b -> f a
rightAdjunct (forall (f :: * -> *) (g :: * -> *) (w :: * -> *) a.
AdjointT f g w a -> g (w (f a))
runAdjointT forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> AdjointT f g w b
f))) g (w (f a))
m