{-# LANGUAGE DataKinds #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  Data.Functor.Adjunction.Square
-- License     :  BSD-style (see the file LICENSE)
-- Maintainer  :  sjoerd@w3future.com
--
-----------------------------------------------------------------------------
module Data.Functor.Adjunction.Square where

import Data.Square
import Data.Profunctor
import qualified Data.Functor.Adjunction as A

-- |
-- > +-----+
-- > |     |
-- > f<-@->g
-- > |     |
-- > +-----+
--
-- > leftAdjunct = unit === (toLeft ||| toRight)
leftAdjunct :: A.Adjunction f g => Square '[Costar f] '[Star g] '[] '[]
leftAdjunct :: forall (f :: * -> *) (g :: * -> *).
Adjunction f g =>
Square '[Costar f] '[Star g] '[] '[]
leftAdjunct = forall (ps :: [* -> * -> *]) (qs :: [* -> * -> *]) (fs :: [* -> *])
       (gs :: [* -> *]).
(IsPList ps, IsPList qs, IsFList fs, IsFList gs,
 Profunctor (PList qs)) =>
(forall a b.
 PlainP ps a b -> PlainP qs (PlainF fs a) (PlainF gs b))
-> Square ps qs fs gs
mkSquare (forall {k} (f :: k -> *) d (c :: k). (d -> f c) -> Star f d c
Star forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(f a -> b) -> a -> u b
A.leftAdjunct forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (d :: k) c. Costar f d c -> f d -> c
runCostar)

-- |
-- > +-----+
-- > |     |
-- > g>-@-<f
-- > |     |
-- > +-----+
--
-- > rightAdjunct = (fromLeft ||| fromRight) === counit
rightAdjunct :: A.Adjunction f g => Square '[Star g] '[Costar f] '[] '[]
rightAdjunct :: forall (f :: * -> *) (g :: * -> *).
Adjunction f g =>
Square '[Star g] '[Costar f] '[] '[]
rightAdjunct = forall (ps :: [* -> * -> *]) (qs :: [* -> * -> *]) (fs :: [* -> *])
       (gs :: [* -> *]).
(IsPList ps, IsPList qs, IsFList fs, IsFList gs,
 Profunctor (PList qs)) =>
(forall a b.
 PlainP ps a b -> PlainP qs (PlainF fs a) (PlainF gs b))
-> Square ps qs fs gs
mkSquare (forall {k} (f :: k -> *) (d :: k) c. (f d -> c) -> Costar f d c
Costar forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(a -> u b) -> f a -> b
A.rightAdjunct forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) d (c :: k). Star f d c -> d -> f c
runStar)

-- |
-- > +-----+
-- > |     |
-- > | /@\ |
-- > | v v |
-- > +-f-g-+
--
-- > unit = fromRight ||| leftAdj ||| fromLeft
unit :: A.Adjunction f g => Square '[] '[] '[] '[f, g]
unit :: forall (f :: * -> *) (g :: * -> *).
Adjunction f g =>
Square '[] '[] '[] '[f, g]
unit = forall (ps :: [* -> * -> *]) (qs :: [* -> * -> *]) (fs :: [* -> *])
       (gs :: [* -> *]).
(IsPList ps, IsPList qs, IsFList fs, IsFList gs,
 Profunctor (PList qs)) =>
(forall a b.
 PlainP ps a b -> PlainP qs (PlainF fs a) (PlainF gs b))
-> Square ps qs fs gs
mkSquare (forall (f :: * -> *) (u :: * -> *) a.
Adjunction f u =>
a -> u (f a)
A.unit forall b c a. (b -> c) -> (a -> b) -> a -> c
.)

-- |
-- > +-g-f-+
-- > | v v |
-- > | \@/ |
-- > |     |
-- > +-----+
--
-- > counit = toRight ||| rightAdjoint ||| toLeft
counit :: A.Adjunction f g => Square '[] '[] '[g, f] '[]
counit :: forall (f :: * -> *) (g :: * -> *).
Adjunction f g =>
Square '[] '[] '[g, f] '[]
counit = forall (ps :: [* -> * -> *]) (qs :: [* -> * -> *]) (fs :: [* -> *])
       (gs :: [* -> *]).
(IsPList ps, IsPList qs, IsFList fs, IsFList gs,
 Profunctor (PList qs)) =>
(forall a b.
 PlainP ps a b -> PlainP qs (PlainF fs a) (PlainF gs b))
-> Square ps qs fs gs
mkSquare (forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) (u :: * -> *) a.
Adjunction f u =>
f (u a) -> a
A.counit)