{-# LANGUAGE Rank2Types, MultiParamTypeClasses, FunctionalDependencies, UndecidableInstances #-}
{-# LANGUAGE CPP #-}
#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 702
{-# LANGUAGE Trustworthy #-}
#endif
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
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)
counit :: a -> f (g a)
leftAdjunct :: (b -> f a) -> a -> g b
rightAdjunct :: (a -> g b) -> b -> f a
unit = (f a -> f a) -> a -> g (f a)
forall (f :: * -> *) (g :: * -> *) b a.
Adjunction f g =>
(b -> f a) -> a -> g b
leftAdjunct f a -> f a
forall a. a -> a
id
counit = (g a -> g a) -> a -> f (g a)
forall (f :: * -> *) (g :: * -> *) a b.
Adjunction f g =>
(a -> g b) -> b -> f a
rightAdjunct g a -> g a
forall a. a -> a
id
leftAdjunct b -> f a
f = (b -> f a) -> g (f a) -> g b
forall (f :: * -> *) a b. Contravariant f => (a -> b) -> f b -> f a
contramap b -> f a
f (g (f a) -> g b) -> (a -> g (f a)) -> a -> g b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> g (f a)
forall (f :: * -> *) (g :: * -> *) a.
Adjunction f g =>
a -> g (f a)
unit
rightAdjunct a -> g b
f = (a -> g b) -> f (g b) -> f a
forall (f :: * -> *) a b. Contravariant f => (a -> b) -> f b -> f a
contramap a -> g b
f (f (g b) -> f a) -> (b -> f (g b)) -> b -> f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> f (g b)
forall (f :: * -> *) (g :: * -> *) a.
Adjunction f g =>
a -> f (g a)
counit
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 :: p (a -> g b) (h (c -> g d)) -> p (b -> f a) (h (d -> f c))
adjuncted = ((b -> f a) -> a -> g b)
-> (h (c -> g d) -> h (d -> f c))
-> p (a -> g b) (h (c -> g d))
-> p (b -> f a) (h (d -> f c))
forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap (b -> f a) -> a -> g b
forall (f :: * -> *) (g :: * -> *) b a.
Adjunction f g =>
(b -> f a) -> a -> g b
leftAdjunct (((c -> g d) -> d -> f c) -> h (c -> g d) -> h (d -> f c)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (c -> g d) -> d -> f c
forall (f :: * -> *) (g :: * -> *) a b.
Adjunction f g =>
(a -> g b) -> b -> f a
rightAdjunct)
{-# INLINE adjuncted #-}
instance Adjunction (Op r) (Op r) where
unit :: a -> Op r (Op r a)
unit a
a = (Op r a -> r) -> Op r (Op r a)
forall a b. (b -> a) -> Op a b
Op (\Op r a
k -> Op r a -> a -> r
forall a b. Op a b -> b -> a
getOp Op r a
k a
a)
counit :: a -> Op r (Op r a)
counit = a -> Op r (Op r a)
forall (f :: * -> *) (g :: * -> *) a.
Adjunction f g =>
a -> g (f a)
unit
instance Adjunction Predicate Predicate where
unit :: a -> Predicate (Predicate a)
unit a
a = (Predicate a -> Bool) -> Predicate (Predicate a)
forall a. (a -> Bool) -> Predicate a
Predicate (\Predicate a
k -> Predicate a -> a -> Bool
forall a. Predicate a -> a -> Bool
getPredicate Predicate a
k a
a)
counit :: a -> Predicate (Predicate a)
counit = a -> Predicate (Predicate a)
forall (f :: * -> *) (g :: * -> *) a.
Adjunction f g =>
a -> g (f a)
unit
contrarepAdjunction :: Adjunction f g => (a -> f ()) -> g a
contrarepAdjunction :: (a -> f ()) -> g a
contrarepAdjunction = ((a -> f ()) -> () -> g a) -> () -> (a -> f ()) -> g a
forall a b c. (a -> b -> c) -> b -> a -> c
flip (a -> f ()) -> () -> g a
forall (f :: * -> *) (g :: * -> *) b a.
Adjunction f g =>
(b -> f a) -> a -> g b
leftAdjunct ()
coindexAdjunction :: Adjunction f g => g a -> a -> f ()
coindexAdjunction :: g a -> a -> f ()
coindexAdjunction = (() -> g a) -> a -> f ()
forall (f :: * -> *) (g :: * -> *) a b.
Adjunction f g =>
(a -> g b) -> b -> f a
rightAdjunct ((() -> g a) -> a -> f ())
-> (g a -> () -> g a) -> g a -> a -> f ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. g a -> () -> g a
forall a b. a -> b -> a
const