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

	-- | Versions of `|-` with various nesting levels
	($|-) :: 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
	($$|-) :: (Covariant v, Covariant w) =>
		v :. w :. t := a -> (a -> u b) -> v :. w := b
	(v :. (w :. 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 :. (w :. t)) := a) -> (v :. w) := b
forall (t :: * -> *) (u :: * -> *) a b.
(Covariant t, Covariant u) =>
(a -> b) -> ((t :. u) := a) -> (t :. u) := b
<$$> (v :. (w :. t)) := a
x
	($$$|-) :: (Covariant v, Covariant w, Covariant x) =>
		v :. w :. x :. t := a -> (a -> u b) -> v :. w :. x := b
	(v :. (w :. (x :. 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 :. (w :. (x :. t))) := a) -> (v :. (w :. x)) := b
forall (t :: * -> *) (u :: * -> *) (v :: * -> *) a b.
(Covariant t, Covariant u, Covariant v) =>
(a -> b) -> ((t :. (u :. v)) := a) -> (t :. (u :. v)) := b
<$$$> (v :. (w :. (x :. t))) := a
x
	($$$$|-) :: (Covariant v, Covariant w, Covariant x, Covariant y) =>
		v :. w :. x :. y :. t := a -> (a -> u b) -> v :. w :. x :. y := b
	(v :. (w :. (x :. (y :. 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 :. (w :. (x :. (y :. t)))) := a)
-> (v :. (w :. (x :. y))) := b
forall (t :: * -> *) (u :: * -> *) (v :: * -> *) (w :: * -> *) a b.
(Covariant t, Covariant u, Covariant v, Covariant w) =>
(a -> b)
-> ((t :. (u :. (v :. w))) := a) -> (t :. (u :. (v :. w))) := b
<$$$$> (v :. (w :. (x :. (y :. t)))) := a
x