module Pandora.Pattern.Functor.Adjoint where

import Pandora.Core.Functor (type (:.), type (:=))
import Pandora.Pattern.Category (identity)
import Pandora.Pattern.Functor.Covariant (Covariant ((<$>)))

type (-|) = Adjoint

infixl 3 -|, |-, -|$, $|-

{- |
> When providing a new instance, you should ensure it satisfies the four laws:
> * Left adjunction identity: phi cozero ≡ identity
> * Right adjunction identity: psi zero ≡ identity
> * Left adjunction interchange: phi f ≡ comap f . eta
> * Right adjunction interchange: psi f ≡ epsilon . comap f
-}

class (Covariant t, Covariant u) => Adjoint t u where
	{-# MINIMAL (-|), (|-) #-}
	-- | Left adjunction
	(-|) :: a -> (t a -> b) -> u b
	-- | Right adjunction
	(|-) :: t a -> (a -> u b) -> b

	-- | Prefix and flipped version of '-|'
	phi :: (t a -> b) -> a -> u b
	phi t a -> b
f a
x = a
x a -> (t a -> b) -> u b
forall (t :: * -> *) (u :: * -> *) a b.
Adjoint t u =>
a -> (t a -> b) -> u b
-| t a -> b
f
	-- | Prefix and flipped version of '|-'
	psi :: (a -> u b) -> t a -> b
	psi a -> u b
g t a
x = t a
x t a -> (a -> u b) -> b
forall (t :: * -> *) (u :: * -> *) a b.
Adjoint t u =>
t a -> (a -> u b) -> b
|- a -> u b
g
	-- | Also known as 'unit'
	eta :: a -> u :. t := a
	eta = (t a -> t a) -> a -> (u :. t) := a
forall (t :: * -> *) (u :: * -> *) a b.
Adjoint t u =>
(t a -> b) -> a -> u b
phi t a -> t a
forall (m :: * -> * -> *) a. Category m => m a a
identity
	-- | Also known as 'counit'
	epsilon :: t :. u := a -> a
	epsilon = (u a -> u a) -> ((t :. u) := a) -> a
forall (t :: * -> *) (u :: * -> *) a b.
Adjoint t u =>
(a -> u b) -> t a -> b
psi u a -> u a
forall (m :: * -> * -> *) a. Category m => m a a
identity

	(-|$) :: Covariant v => v a -> (t a -> b) -> v (u b)
	v a
x -|$ t a -> b
f = (a -> (t a -> b) -> u b
forall (t :: * -> *) (u :: * -> *) a b.
Adjoint t u =>
a -> (t a -> b) -> u b
-| t a -> b
f) (a -> u b) -> v a -> v (u b)
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$> v a
x

	($|-) :: Covariant v => v (t a) -> (a -> u b) -> v b
	v (t a)
x $|- a -> u b
f = (t a -> (a -> u b) -> b
forall (t :: * -> *) (u :: * -> *) a b.
Adjoint t u =>
t a -> (a -> u b) -> b
|- a -> u b
f) (t a -> b) -> v (t a) -> v b
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$> v (t a)
x