Idris2Doc : Data.Profunctor.Types

Data.Profunctor.Types

(source)
This module contains the Profunctor interface itself, along with a few
examples of profunctors.

Definitions

interface Profunctor : (Type -> Type -> Type) -> Type
  An interface for (self-enriched) profunctors `Idr -/-> Idr`.

Formally, a profunctor is a binary functor that is contravariant in its
first argument and covariant in its second. A common example of a profunctor
is the (non-dependent) function type.

Implementations can be defined by specifying either `dimap` or both `lmap`
and `rmap`.

Laws:
* `dimap id id = id`
* `dimap (f . g) (h . i) = dimap g h . dimap f i`

Parameters: p
Methods:
dimap : (a -> b) -> (c -> d) -> p b c -> p a d
  Map over both parameters of a profunctor at the same time, with the
left function argument mapping contravariantly.
lmap : (a -> b) -> p b c -> p a c
  Map contravariantly over the first parameter of a profunctor.
rmap : (b -> c) -> p a b -> p a c
  Map covariantly over the second parameter of a profunctor.

Implementations:
Profunctor Morphism
Functor f => Profunctor (Kleislimorphism f)
Functor f => Profunctor (Star f)
Functor f => Profunctor (Costar f)
Profunctor Tagged
Profunctor (Forget r)
Profunctor (Coforget r)
Bifunctor ten => Profunctor p => Profunctor (GenTambara ten p)
Profunctor (GenPastro ten p)
Profunctor p => Profunctor (Closure p)
Profunctor (Environment p)
dimap : Profunctor p => (a -> b) -> (c -> d) -> p b c -> p a d
  Map over both parameters of a profunctor at the same time, with the
left function argument mapping contravariantly.

Totality: total
Visibility: public export
lmap : Profunctor p => (a -> b) -> p b c -> p a c
  Map contravariantly over the first parameter of a profunctor.

Totality: total
Visibility: public export
rmap : Profunctor p => (b -> c) -> p a b -> p a c
  Map covariantly over the second parameter of a profunctor.

Totality: total
Visibility: public export
0 (:->) : (k -> k' -> Type) -> (k -> k' -> Type) -> Type
  A transformation between profunctors that preserves their type parameters.

Formally, this is a natural transformation of functors `Idrᵒᵖ * Idr => Idr`.

If the transformation is `tr`, then we have the following law:
* `tr . dimap f g = dimap f g . tr`

Totality: total
Visibility: public export
Fixity Declaration: infix operator, level 0
record Star : (k -> Type) -> Type -> k -> Type
  Lift a functor into a profunctor in the return type.

This type is equivalent to `Kleislimorphism` except for the polymorphic type
of `b`.

Totality: total
Visibility: public export
Constructor: 
MkStar : (a -> f b) -> Star f a b

Projection: 
.applyStar : Star f a b -> a -> f b

Hints:
Applicative f => Applicative (Star f a)
Contravariant f => Contravariant (Star f a)
Functor f => Functor (Star f a)
Functor f => GenStrong Pair (Star f)
Applicative f => GenStrong Either (Star f)
Monad f => Monad (Star f a)
Functor f => Profunctor (Star f)
.applyStar : Star f a b -> a -> f b
Totality: total
Visibility: public export
applyStar : Star f a b -> a -> f b
Totality: total
Visibility: public export
record Costar : (k -> Type) -> k -> Type -> Type
  Lift a functor into a profunctor in the argument type.

Totality: total
Visibility: public export
Constructor: 
MkCostar : (f a -> b) -> Costar f a b

Projection: 
.applyCostar : Costar f a b -> f a -> b

Hints:
Applicative (Costar f a)
Functor f => Closed (Costar f)
Functor (Costar f a)
Monad (Costar f a)
Functor f => Profunctor (Costar f)
.applyCostar : Costar f a b -> f a -> b
Totality: total
Visibility: public export
applyCostar : Costar f a b -> f a -> b
Totality: total
Visibility: public export
record Tagged : k -> Type -> Type
  The profunctor that ignores its argument type.
Equivalent to `const id` up to isomorphism.

Totality: total
Visibility: public export
Constructor: 
Tag : b -> Tagged a b

Projection: 
.runTagged : Tagged a b -> b

Hints:
Applicative (Tagged a)
Foldable (Tagged a)
Functor (Tagged a)
GenStrong Either Tagged
Monad (Tagged a)
Profunctor Tagged
Traversable (Tagged a)
.runTagged : Tagged a b -> b
Totality: total
Visibility: public export
runTagged : Tagged a b -> b
Totality: total
Visibility: public export
retag : Tagged a c -> Tagged b c
  Retag the value with a different type-level parameter.

Totality: total
Visibility: public export
record Forget : Type -> Type -> k -> Type
  `Forget r` is equivalent to `Star (Const r)`.

Totality: total
Visibility: public export
Constructor: 
MkForget : (a -> r) -> Forget r a b

Projection: 
.runForget : Forget r a b -> a -> r

Hints:
Monoid r => Applicative (Forget r a)
Contravariant (Forget r a)
Foldable (Forget r a)
Functor (Forget r a)
GenStrong Pair (Forget r)
Monoid r => GenStrong Either (Forget r)
Monoid r => Monad (Forget r a)
Profunctor (Forget r)
Traversable (Forget r a)
.runForget : Forget r a b -> a -> r
Totality: total
Visibility: public export
runForget : Forget r a b -> a -> r
Totality: total
Visibility: public export
reforget : Forget r a b -> Forget r a c
Totality: total
Visibility: public export
record Coforget : Type -> k -> Type -> Type
  `Coforget r` is equivalent to `Costar (Const r)`.

Totality: total
Visibility: public export
Constructor: 
MkCoforget : (r -> b) -> Coforget r a b

Projection: 
.runCoforget : Coforget r a b -> r -> b

Hints:
Applicative (Coforget r a)
Bifunctor (Coforget r)
Functor (Coforget r a)
GenStrong Either (Coforget r)
Monad (Coforget r a)
Profunctor (Coforget r)
.runCoforget : Coforget r a b -> r -> b
Totality: total
Visibility: public export
runCoforget : Coforget r a b -> r -> b
Totality: total
Visibility: public export
recoforget : Coforget r a c -> Coforget r b c
Totality: total
Visibility: public export