Pandora.Pattern.Functor.Adjoint

Documentation

class (Covariant t, Covariant u) => Adjoint t u where

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

Minimal complete definition

(-|), (|-)

Methods

(-|) :: a -> (t a -> b) -> u b infixl 4

Left adjunction

(|-) :: t a -> (a -> u b) -> b infixl 4

Right adjunction

phi :: (t a -> b) -> a -> u b

Prefix and flipped version of -|

psi :: (a -> u b) -> t a -> b

Prefix and flipped version of |-

eta :: a -> (u :. t) := a

Also known as unit

epsilon :: ((t :. u) := a) -> a

Also known as counit

Instances

Adjoint Identity Identity

Defined in Pandora.Paradigm.Basis.Identity

Methods

(-|) :: a -> (Identity a -> b) -> Identity b

(|-) :: Identity a -> (a -> Identity b) -> b

phi :: (Identity a -> b) -> a -> Identity b

psi :: (a -> Identity b) -> Identity a -> b

eta :: a -> (Identity :. Identity) := a

epsilon :: ((Identity :. Identity) := a) -> a

Adjoint (Store s) (State s)

Defined in Pandora.Paradigm.Inventory.Optics

Methods

(-|) :: a -> (Store s a -> b) -> State s b

(|-) :: Store s a -> (a -> State s b) -> b

phi :: (Store s a -> b) -> a -> State s b

psi :: (a -> State s b) -> Store s a -> b

eta :: a -> (State s :. Store s) := a

epsilon :: ((Store s :. State s) := a) -> a

(Extractable t, Pointable t, Extractable u, Pointable u) => Adjoint (Yoneda t) (Yoneda u)

Defined in Pandora.Paradigm.Basis.Yoneda

Methods

(-|) :: a -> (Yoneda t a -> b) -> Yoneda u b

(|-) :: Yoneda t a -> (a -> Yoneda u b) -> b

phi :: (Yoneda t a -> b) -> a -> Yoneda u b

psi :: (a -> Yoneda u b) -> Yoneda t a -> b

eta :: a -> (Yoneda u :. Yoneda t) := a

epsilon :: ((Yoneda t :. Yoneda u) := a) -> a

Adjoint (Product a) ((->) a :: Type -> Type)

Defined in Pandora.Paradigm.Basis.Product

Methods

(-|) :: a0 -> (Product a a0 -> b) -> a -> b

(|-) :: Product a a0 -> (a0 -> a -> b) -> b

phi :: (Product a a0 -> b) -> a0 -> a -> b

psi :: (a0 -> a -> b) -> Product a a0 -> b

eta :: a0 -> ((->) a :. Product a) := a0

epsilon :: ((Product a :. (->) a) := a0) -> a0

type (-|) = Adjoint infixl 4