Data.Profunctor.Strong

(source)

This module defines profunctor strength with respect to a particular
monoidal structure.

Unlike Haskell's profunctors library, `Strong` and `Choice` are here
special cases of the interface `GenStrong`, which defines strength with
respect to an arbitrary tensor product. When writing implementations for
a profunctor, `GenStrong Pair` and `GenStrong Either` should be used instead
of `Strong` and `Choice` respectively.

Definitions

interface GenStrong : (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type

  Profunctor strength with respect to a tensor product.
  A strong profunctor preserves the monoidal structure of a category.
  
  These constraints are not required by the interface, but the tensor product
  `ten` is generally expected to implement `(Tensor ten i, Symmetric ten)`.
  
  Laws:
  * `strongl = dimap swap' swap' . strongr`
  * `dimap unitr.rightToLeft unitr.leftToRight . strongl = id`
  * `lmap (mapSnd f) . strongl = rmap (mapSnd f) . strongl`
  * `strongr . strongr = dimap assocr assocl . strongr`
  
  @ ten The tensor product of the monoidal structure

Parameters: ten, p
Constraints: Profunctor p
Methods:

strongl : p a b -> p (ten a c) (ten b c)

  The left action of a strong profunctor.

strongr : p a b -> p (ten c a) (ten c b)

  The right action of a strong profunctor.

Implementations:

Bifunctor ten => GenStrong ten Morphism
Functor f => GenStrong Pair (Kleislimorphism f)
Applicative f => GenStrong Either (Kleislimorphism f)
Functor f => GenStrong Pair (Star f)
Applicative f => GenStrong Either (Star f)
GenStrong Either Tagged
GenStrong Pair (Forget r)
Monoid r => GenStrong Either (Forget r)
GenStrong Either (Coforget r)
Associative ten => Symmetric ten => Profunctor p => GenStrong ten (GenTambara ten p)
(Associative ten, Symmetric ten) => GenStrong ten (GenPastro ten p)
Strong p => GenStrong Pair (Closure p)

strongl : GenStrong ten p => p a b -> p (ten a c) (ten b c)

  The left action of a strong profunctor.

Totality: total
Visibility: public export

strongr : GenStrong ten p => p a b -> p (ten c a) (ten c b)

  The right action of a strong profunctor.

Totality: total
Visibility: public export

Strong : (Type -> Type -> Type) -> Type

  Profunctor strength with respect to the product (`Pair`).

Totality: total
Visibility: public export

first : Strong p => p a b -> p (a, c) (b, c)

  A special case of `strongl` with constraint `Strong`.
  This is useful if the typechecker has trouble inferring the tensor product.

Totality: total
Visibility: public export

second : Strong p => p a b -> p (c, a) (c, b)

  A special case of `strongr` with constraint `Strong`.
  This is useful if the typechecker has trouble inferring the tensor product.

Totality: total
Visibility: public export

Choice : (Type -> Type -> Type) -> Type

  Profunctor strength with respect to the coproduct (`Either`).

Totality: total
Visibility: public export

left : Choice p => p a b -> p (Either a c) (Either b c)

  A special case of `strongl` with constraint `Choice`.
  This is useful if the typechecker has trouble inferring the tensor product to use.

Totality: total
Visibility: public export

right : Choice p => p a b -> p (Either c a) (Either c b)

  A special case of `strongr` with constraint `Choice`.
  This is useful if the typechecker has trouble inferring the tensor product to use.

Totality: total
Visibility: public export

uncurry' : Strong p => p a (b -> c) -> p (a, b) c

Totality: total
Visibility: public export

strong : Strong p => (a -> b -> c) -> p a b -> p a c

Totality: total
Visibility: public export

record GenTambara : (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type

  The comonad generated by the reflective subcategory of profunctors that
  implement `GenStrong ten`.

Totality: total
Visibility: public export
Constructor:

MkTambara : p (ten a c) (ten b c) -> GenTambara ten p a b

Projection:

.runTambara : GenTambara ten p a b -> p (ten a c) (ten b c)

Hints:

Bifunctor ten => Profunctor p => Functor (GenTambara ten p a)
Associative ten => Symmetric ten => Profunctor p => GenStrong ten (GenTambara ten p)
Bifunctor ten => Profunctor p => Profunctor (GenTambara ten p)
ProfunctorAdjunction (GenPastro ten) (GenTambara ten)
Tensor ten i => ProfunctorComonad (GenTambara ten)
ProfunctorFunctor (GenTambara ten)

.runTambara : GenTambara ten p a b -> p (ten a c) (ten b c)

Totality: total
Visibility: public export

runTambara : GenTambara ten p a b -> p (ten a c) (ten b c)

Totality: total
Visibility: public export

Tambara : (Type -> Type -> Type) -> Type -> Type -> Type

  The comonad generated by the reflective subcategory of profunctors that
  implement `Strong`.
  
  This is a special case of `GenTambara`.

Totality: total
Visibility: public export

TambaraSum : (Type -> Type -> Type) -> Type -> Type -> Type

  The comonad generated by the reflective subcategory of profunctors that
  implement `Choice`.
  
  This is a special case of `GenTambara`.

Totality: total
Visibility: public export

tambara : GenStrong ten p => p :-> q -> p :-> GenTambara ten q

Totality: total
Visibility: public export

untambara : Tensor ten i => Profunctor q => p :-> GenTambara ten q -> p :-> q

Totality: total
Visibility: public export

data GenPastro : (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type

  The monad generated by the reflective subcategory of profunctors that
  implement `GenStrong ten`.

Totality: total
Visibility: public export
Constructor:

MkPastro : (ten y z -> b) -> p x y -> (a -> ten x z) -> GenPastro ten p a b

Hints:

(Associative ten, Symmetric ten) => GenStrong ten (GenPastro ten p)
Profunctor (GenPastro ten p)
ProfunctorAdjunction (GenPastro ten) (GenTambara ten)
ProfunctorFunctor (GenPastro ten)
(Tensor ten i, Symmetric ten) => ProfunctorMonad (GenPastro ten)

Pastro : (Type -> Type -> Type) -> Type -> Type -> Type

  The monad generated by the reflective subcategory of profunctors that
  implement `Strong`.
  
  This is a special case of `GenPastro`.

Totality: total
Visibility: public export

PastroSum : (Type -> Type -> Type) -> Type -> Type -> Type

  The monad generated by the reflective subcategory of profunctors that
  implement `Choice`.
  
  This is a special case of `GenPastro`.

Totality: total
Visibility: public export

pastro : GenStrong ten q => p :-> q -> GenPastro ten p :-> q

Totality: total
Visibility: public export

unpastro : Tensor ten i => GenPastro ten p :-> q -> p :-> q

Totality: total
Visibility: public export