We study monoidal profunctors as a tool to reason and structure pure functional programs both from a categorical perspective and as a Haskell implementation. From the categorical point of view we approach them as monoids in a certain monoidal category of profunctors. We study properties of this monoidal category and construct and implement the free monoidal profunctor. We study the relationship of the monoidal construction to optics, and introduce a promising generalization of the implementation which we illustrate by introducing effectful monoidal profunctors.

§ INTRODUCTION

Functors, applicative functors [14], monads [16, 22], profunctors, and arrows [4, 5] are by now part of the vocabulary of
the programmer who writes mathematically structured programs. In order to understand and develop these structures both the categorical view
and the programming view have been helpful. For example, Lindley et al. [12] compare these structures from the point of view of (typed) programming languages,
and Rivas and Jaskelioff [20] compare them from the point of view of monoidal categories.

In this last work, both monads and applicative functors are seen as monoids in a monoidal category of endofunctors.
Monads use functor composition as tensor, whereas applicative functors use the Day convolution as tensor.
Likewise, arrows can be seen as monoids in a monoidal category of (strong) profunctors.

However, given that the Day convolution can also be a tensor of profunctors there is another structure yet to be studied.
In this work we study monoidal profunctors, a structure obtained from considering monoids in a category of profunctors
taking the Day convolution as tensor, hence filling the gap in the following table:

functor     applicative     monad

profunctor     ????     arrow

Structure relations

Monoidal profunctors are a categorical structure with two components: an
identity computation and a generic parallel composition.

Therefore, with this paper we aim to gather the knowledge about monoidal
profunctors and study their application in the context of functional programming.

After some mathematical background (Section <ref>), we introduce monoidal profunctors as monoids in a monoidal category
and study some of their properties (Section <ref>). Then, in Section <ref>, we implement these ideas in Haskell and provide some instances.
We show the free monoidal profunctor and a Haskell implementation in Section <ref>.

In Section <ref>, we present an application of monoidal profunctors to optics [1]
and observe connections with well-known structures such as traversals and grates [19, 17].
In Section <ref>, we generalize the implementation to other categories and illustrate its application to effectful monoidal profunctors.

§ MATHEMATICAL BACKGROUND

§.§ Monoidal Categories and Monoids

A monoidal category [20] gives us a minimal framework for defining the categorical version of a monoid.

A monoidal category is a sextuple ($\mathcal{C}$, $\otimes$, $I$,
$\alpha$, $\rho$, $\lambda$) where

* $\mathcal{C}$ is a category;

* $\otimes:\mathcal{C} \times \mathcal{C} \rightarrow \mathcal{C}$ is
a bifunctor;

* $I$ is an object called unit;

* $\rho_A : A \otimes I\rightarrow A$, $\lambda_A : I \otimes A \rightarrow A$ and $\alpha_{ABC} : (A \otimes B) \otimes C \rightarrow A \otimes (B \otimes C)$ are three natural isomorphisms.

If the isomorphisms $\rho$, $\lambda$ and $\alpha$ are identities then the monoidal category is called strict, if there is a natural isomorphism
$\gamma_{AB} : A \otimes B \rightarrow B \otimes A$ the monoidal category is called symmetric.

A monoidal category is closed if there is an additional functor, called the internal hom,
$\Rightarrow : \mathcal{C}^{op} \times \mathcal{C} \rightarrow Set$ such that
$\CC (A \otimes B, C) \cong \CC(A,B \Rightarrow C)$, natural in $A$, $B$ and $C$, objects of $\mathcal{C}$.
The witnesses of this isomorphism are called currying and uncurrying. In $Set$, with $\otimes = \times$, $A \Rightarrow B$ is just the hom-set $A \rightarrow B$.

A monoid in a monoidal category $\mathcal{C}$ is the tuple $(M,e,m)$ where
$M$ is an object of $\mathcal{C}$, $e:I \rightarrow M$ is the unit morphism
and $m: M \otimes M \rightarrow M$ is the multiplication morphism, satisfying

* Right unit: $m \circ (id \otimes e) = \rho_{MMM}$

* Left unit: $m \circ (e \otimes id) = \lambda_{MMM}$

* Associativity: $m \circ (m \otimes id) = m \circ (id \otimes m) \circ \alpha_{MMM} $

§.§ Profunctors

A profunctor generalizes the notions of function relation and bimodule [10].

Given two categories $\mathcal{C}$ and $\mathcal{D}$, a profunctor from $\CC$ to $\DD$ is a functor $P : \mathcal{C}^{op} \times \mathcal{D} \rightarrow Set$, consisting of:

* for each $a$ object of $\mathcal{C}$ and $b$ object of $\mathcal{D}$, a set $P(a,b)$;

* for each $a$ object of $\mathcal{C}$ and $b, d$ objects of $\mathcal{D}$, a function (left action) $\mathcal{D}(d,b) \times P(a,d) \rightarrow P(a,b)$;

* for all $a,c$ objects of $\mathcal{C}$ and $b$ object of $\mathcal{D}$, a function (right action) $P(a,b) \times \CC(c,a) \rightarrow P(c,b)$.

This notion is also known as a Bimodule or a ($\mathcal{C}$,$\mathcal{D}$)-module, and also as a distributor.

Since a profunctor is a functor from the product category $\CC^{op} \times \DD$ to $Set$, it must satisfy the functor laws.

\begin{align*}
P(1_{C},1_{D}) &= 1_{P(C,D)} \\
P(f\circ g,h \circ i) &= P(g,h) \circ P(f,i)
\end{align*}

An example of a profunctor is the hom functor $Hom : \mathcal{C}^{op} \times \mathcal{C} \rightarrow Set$, written as $A \rightarrow B$ when $\CC = Set$, and its actions are just pre-composition and post-composition of set functions.

Let $\CC$ and $\DD$ be small categories, $Prof(\CC,\DD)$ is the profunctor category consisting of profunctors $\CC^{op} \times \DD \to Set$ as objects, natural transformations between profunctors as morphisms, and vertical composition to compose them. The fact that $\CC$ and $\DD$ are small categories will always be implied when some statement about the category $Prof(\CC,\DD)$ is present. We will call this category $Prof$ when the categories $\CC$ and $\DD$ are clear from the context.

The profunctor category inherits some structure from the category $Set$ such as binary products given by $(P \times Q) (S,T) = P(S,T) \times Q(S,T)$ and binary coproducts given by $(P + Q) (S,T) = P(S,T) + Q(S,T)$, where $\times, +$ are the respective universal constructions from $Set$. There are also terminal and initial profunctors given by $1_p(S,T) = \{*\}$ and $0_p(S,T) = \emptyset$, i.e., they are just constant maps to the initial and terminal object of $Set$, respectively.

§.§ Day Convolution

Let $\mathcal{E}$ be a small monoidal category and $F,G : \mathcal{E} \rightarrow Set$, then the Day convolution [2] of F and G is another functor (in $T$) given by the coend

\begin{equation}
(F \star G) T = \int^{XY} FX \times GY \times \mathcal{D}(X \otimes Y, T).
\end{equation}

One can work with this coend in the category $Prof(\CC,\DD)$ of profunctors, that is, letting $\mathcal{E} = \mathcal{C}^{op} \times \mathcal{D}$ in the above definition, enabling us to derive the following Day convolution for profunctors.

\[
(P \star Q)(S,T) \cong \int^{ABCD} P(A,B) \times Q(C,D) \times \mathcal{C}(S, A \otimes C) \times \mathcal{C}(B \otimes D, T)
\]

The profunctor $J(A,B) = \CC(A,I) \times \CC(I,B)$ is a unit for $\star$. When $I = 1$, where $1$ is the terminal object, then $J(A,B) \cong B$. When $\CC = Set$, this convolution gives rise to a monoidal profunctor (see next section), when $\CC$ is a Kleisli category on Set (same objects, but morphisms relies on a monad) gives the notion of an effectful monoidal profunctor (see Section <ref>).

Let $\CC$ be a monoidal category, the profunctor $J(A,B) = \CC(A,I) \times \CC(I,B)$ is the right and left unit of $\star$.

The calculation is standard coend calculus [13] using Yoneda's lemma. This is a proof for $J$ being a right unit, for the left one is analogous.

(P ⋆J)(S,T)     = ∫^ABCD P(A,B) ×J(C,D) ×(S, A ⊗C) ×(B ⊗D, T)

≅∫^ABCD P(A,B) ×(C,I) ×(I,D) ×(S, A ⊗C) ×(B ⊗D, T)

≅∫^ABD P(A,B) ×(I,D) ×(S, A ⊗I) ×(B ⊗D, T)

≅∫^AB P(A,B) ×(S, A ⊗I) ×(B ⊗I, T)

≅∫^AB P(A,B) ×(S, A) ×(B, T)

The associativity of $\star$ is required to define a monoidal profunctor category.

Let ($\CC$,$\otimes$,$I$) be a monoidal category and $S,T$ two objects of $\CC$, the Day convolution for profunctors is an associative tensor product $(P \star Q) \star R \cong P \star (Q \star R)$.

The proof follows the same coend calculus pattern using Yoneda's lemma whenever needed.

In order to be able to define monoids in a monoidal profunctor category, one needs to check that when $\CC$ and $\DD$ are monoidal categories then $(Prof(\CC,\DD)), \star, J)$ is a monoidal category.

Let $\CC$ and $\DD$ are monoidal small categories. Then $(Prof(\CC,\DD)), \star, J)$ is a monoidal category.

Since $\CC$ and $\DD$ are monoidal categories, $\star$ is a bifunctor by construction, and by Proposition <ref> and <ref> gives the desired morphisms, it follows that $(Prof(\CC,\DD)), \star, J)$ is a monoidal category.

Having obtained a monoidal category of profunctors, it is now possible to define a monoid in this category. In order to do that, we will use the following proposition (as in the work of Rivas and Jaskelioff [20]).

Let $\DD = \CC^{op} \otimes \CC$, there is a one-to-one correspondence defining morphisms going out of a Day convolution for profunctors

\begin{equation*}
\int_{XY} (P\star Q)(X,Y) \to R(X,Y) \cong \int_{ABCD} P(A,B) \times Q(C,D) \to R(A \otimes C,B \otimes D)
\end{equation*}

which is natural in $P$, $Q$ and $R$.

This proof uses the same coend calculus pattern with the help of Yoneda lemma and the fact that the hom functor commutes with ends and coends [13].

\begin{align*}
&\int_{XY} (P\star Q)(X,Y) \to R(X,Y)  \\
\cong & \int_{XY} (\int^{ABCD} (P(A,B) \times Q(C,D)) \times \CC(X, A \otimes C) \times \CC(B \otimes D,Y)) \to R(X,Y) \\
\cong& \int_{XYABCD} (P(A,B) \times Q(C,D)) \times \CC(X, A \otimes C) \times \CC(B \otimes D,Y) \to R(X,Y) \\
\cong& \int_{XYABCD} (P(A,B) \times Q(C,D)) \to \CC(X, A \otimes C) \to \CC(B \otimes D,Y) \to R(X,Y) \\
\cong& \int_{YABCD} (P(A,B) \times Q(C,D)) \to \CC(B \otimes D,Y) \to R(A \otimes C,Y) \\
\cong& \int_{ABCD} P(A,B) \times Q(C,D) \to R(A \otimes C,B \otimes D)
\end{align*}

Whenever $P = Q = R$ in the equation of Proposition $\ref{monprof}$ we get the following isomorphism, useful to define a monoid in the profunctor category $Prof$ with Day convolution as its tensor.

\[
\int_{XY} (P\star P)(X,Y) \to P(X,Y) \cong \int_{ABCD} P(A,B) \times P(C,D)\to P(A \otimes C,B \otimes D)
\]

§ MONOIDAL PROFUNCTORS

We define monoidal profunctors as monoids in the monoidal category of profunctors of theorem <ref>.

Let ($\CC$,$\otimes$,$I$) be a small monoidal category, $P: \CC^{op} \times \CC \to Set$ be a profunctor, and $S,T$ two objects of $\CC$. Then $\CC(J(S,T),P(S,T)) \cong P(I,I)$.

\begin{align*}
\CC(J(S,T),P(S,T)) &\cong \CC(S,I) \times \CC(I,T) \to P(S,T) \\
& \cong \CC(S,I) \to \CC(I,T) \to P(S,T) \\
& \cong \CC(S,I) \to P(S,I) \\
& \cong P(I,I)
\end{align*}

With all categorical tools in hand, the central notion of this work emerges from the category of monoidal profunctors.

Let $(\CC,\otimes,I)$ and $(\DD,\otimes,I)$ be small monoidal categories. A monoid in the monoidal profunctor category $Prof(\CC,\DD)$ consists of a profunctor $P$, a unit $e : P(I,I)$, and a multiplication given by a natural family of morphisms $m_{ABCD} : P(A,B) \times P(C,D)\to P(A \otimes C,B \otimes D)$.

The unit is a natural transformation $e : J \to P$, which by proposition <ref> is isomorphic to $e : P(I,I)$. The multiplication is a natural transformation $m : P \star P \to P$, which by proposition <ref> is equivalent to the family above.

As an example, consider $(Set,\otimes,I)$, where $I$ is a singleton set, and the $Hom$ profunctor $P(A,B) = A \to B$, trivially gives us a monoidal profunctor.

Let $(\CC,\otimes,I)$ and $(\DD,\otimes,J)$ be a small monoidal categories, and $P, Q$ monoidal profunctors, then

\[
(P \Rightarrow Q)(X,Y) = \int_{CD} P(C,D) \rightarrow Q(X \otimes C,Y \otimes D)
\]

defines an internal hom on the monoidal profunctor category $Prof(\CC,\DD)$.

This proof follows the same steps as in the functor case [20] but adapting it for $Prof(\CC,\DD)$.

This proposition states that the monoidal category of profunctors $Prof$ is closed.

§ IMPLEMENTATION IN HASKELL

We implement in Haskell the concepts of profunctors, Day convolution, and monoidal profunctors defined before. Although other monoidal profunctors can be derived using other bifunctors, this work focuses only on the product. This section considers the (fictitious) category $Hask$ as a small monoidal category and $Prof(Hask,Hask)$ as the small category of profunctors to implement the typeclass  which represents the desired monoid over this category.

§.§ Profunctors

A profunctor is an instance of the following class

[B]𝐜𝐥𝐚𝐬𝐬 Profunctor p 𝐰𝐡𝐞𝐫𝐞[E]

[5]dimap::(a→b)→(c→d)→p b c→p a d[E]

A profunctor is a functor, thus  needs to satisfy the functor laws.

The profunctor interface lifts pure functions into both type arguments, the first in a contravariant manner, and the second in a covariant way.

A morphism in the $Prof$ category can be represented, in Haskell, as the type below.

[B]𝐭𝐲𝐩𝐞 () p q=∀x y∘.p x y→q x y[E]

The function type , is the most basic example of a profunctor.

One notion captured by a Profunctor is that of a structured input and structured output of a function . This type generalizes Kleisli arrows which allow a pure input and a structured output.
[B]𝐝𝐚𝐭𝐚 SISO f g a b=SISO {1.5mu unSISO::f a→g b1.5mu}[E]

[B]𝐢𝐧𝐬𝐭𝐚𝐧𝐜𝐞 (Functor f,Functor g)⇒Profunctor (SISO f g) 𝐰𝐡𝐞𝐫𝐞[E]

[5]dimap ab cd (SISO bc)=SISO (fmap cd∘.bc∘.fmap ab)[E]

§.§ The Day convolution type

The Day convolution is represented by the existential type

[B]𝐝𝐚𝐭𝐚 Day p q s t=∀a b c d∘.Day (p a b) (q c d) (s→(a,c)) (b→d→t)[E]

Since $\CC(A,I)$ is isomorphic to a singleton set (unit of the cartesian product $\times$), and $\CC(I,B) \cong B$, one can write, in Haskell, the type

[B]𝐝𝐚𝐭𝐚 I a b=I {1.5mu unI::b1.5mu}[E]

as the unit of the Day convolution. The following functions are representations of the right and left units.

[B]ρ::Profunctor p⇒Day p Ip[E]

[B]ρ (Day pab (I d) sac bdt)=dimap (fst∘.sac) (λb→bdt b d) pab[E]

[B]λ::Profunctor q⇒Day I qq[E]

[B]λ (Day (I b) qcd sac bdt)=dimap (snd∘.sac) (λd→bdt b d) qcd[E]

The associativity of the Day convolution and its symmetric map also can be represented in Haskell as the functions below.

[B]α::(Profunctor p,Profunctor q,Profunctor r)⇒Day (Day p q) rDay p (Day q r)[E]

[B]α (Day (Day p q s_1 f) r s_2 g)=Day p (Day q r f_1 f_2) f_3 f_4[E]

[23]=first' (snd∘.s_1)∘.s_2[E]

[9]f_2 d_1 d_2[23]
[26](d_2,λx→f x d_1)[E]

[23]=first' (fst∘.s_1∘.(fst∘.s_2))∘.diag[E]

[9]f_4 b_1 (d_2,h)[23]
[23]=g (h b_1) d_2[E]

[B]γ::(Profunctor p,Profunctor q)⇒Day p qDay q p[E]

[B]γ (Day p q sac bdt)=Day q p (swap∘.sac) (flip bdt)[E]

[5]𝐰𝐡𝐞𝐫𝐞 swap (x,y)=(y,x)[E]

Functions , , and  are natural isomorphisms. We leave the definition of the inverses as an exercise for the reader.

§.§ MonoPro typeclass

We define a typeclass called  for implementing monoidal profunctors.
The type  is a representation in Haskell of the unit $P(I,I)$.
The multiplication is obtained from Proposition <ref>, which gives the multiplication a type $\int_{ABCD} P(A,B) \times P(C,D)\to P(A \otimes C,B \otimes D)$ allowing to write the following class in Haskell.

[B]𝐜𝐥𝐚𝐬𝐬 Profunctor p⇒MonoPro p 𝐰𝐡𝐞𝐫𝐞[E]

[5]mpempty::p () ()[E]

[5](⋆)::p b c→p d e→p (b,d) (c,e)[E]

satisfying the monoid laws

* Left  identity:

* Right identity:

* Associativity:

where the helper functions ,
, and  are the obvious ones.

Another way to understand  is that it lifts pure functions with many
inputs to a binary constructor type, while a profunctor only lifts functions
with one type as input parameter.

[B]lmap_2::MonoPro p⇒(s→(a,c))→p a b→p c d→p s (b,d)[E]

[B]lmap_2 f pa pc=dimap f id (pa⋆pc)[E]

[B]rmap_2::MonoPro p⇒((b,d)→t)→p a b→p c d→p (a,c) t[E]

[B]rmap_2 f pa pc=dimap id f (pa⋆pc)[E]

which can work together as one function

[B]rlmap::MonoPro p⇒((b,d)→t)→(s→(a,c))→p a b→p c d→p s t[E]

[B]rlmap f g pa pc=dimap f g (pa⋆pc)[E]

which is the same behavior as the Day convolution of  with itself. Such convolution is the raison d'être of a monoidal profunctor. A parallel composition is followed by a covariant and a contravariant lifting of two pure functions matching the inner structure, which in our case is the product type .

If one chooses a suitable monoidal profunctor  and type ,
inherits the applicative functor behavior naturally.

[B]appToMonoPro::MonoPro p⇒p s (a→b)→p s a→p s b[E]

[B]appToMonoPro pab pa=[24]
[24]dimap diag (uncurry ($)) (pab⋆pa)[E]

The  typeclass has a straightforward instance for the Hom profunctor  which satisfies the monoidal profunctor laws trivially. A practical use for this instance is writing expressions in a pointfree manner. One can write an  function, for example, for any functor that has as as input a pair type. A  is another example of a monoidal profunctor.

[B]𝐢𝐧𝐬𝐭𝐚𝐧𝐜𝐞 [11]
[11](Functor f,Applicative g)⇒MonoPro (SISO f g) 𝐰𝐡𝐞𝐫𝐞[E]

[5]mpempty=SISO (λ→pure ())[E]

[5]SISO f⋆SISO g=SISO (zip'∘.(f⋆g)∘.unzip')[E]

where  is the applicative functor multiplication. The most basic notion of a monoidal profunctor is represented by this instance. It tells us that the input needs to be a functor instance because of , the functions  and  are composed in a parallel manner using the monoidal profunctor instance for  and then regrouped together using the applicative (monoidal) behavior of .

§ FREE MONOIDAL PROFUNCTORS

There are different theorems with different hypothesis that ensure the existence of a free monoid in a monoidal category.
Here, we follow Rivas and Jaskelioff [20] and use the following proposition to ensure the existence of the free monoidal profunctor.

Let $(\CC, \otimes, I)$ be a monoidal category with internal homs. If $\CC$ has binary coproducts, and for each $A \in ob(\CC)$ the initial algebra for the endofunctor $I + A \otimes -$ exists, then for each A the free monoid $A^{*}$ exists and its carrier is the carrier of the initial algebra.

The category $Prof(\CC,\CC)$, when $\CC$ is a small monoidal category, is monoidal with the Day convolution $\star$ and the profunctor $I$ as its unit, and also has binary coproducts and internal homs. The least fixed point of the endofunctor $Q(X) = J + P \star X$ in $Prof(\CC,\CC)$ gives the free monoidal profunctor.

Following this definition we arrive at the following implementation of the free monoidal profunctor (see also [15]).
[B]𝐝𝐚𝐭𝐚 FreeMP p s t 𝐰𝐡𝐞𝐫𝐞[E]

[5]MPempty::t→FreeMP p s t[E]

[5]FreeMP::(s→(x,z))→((y,w)→t)→p x y→FreeMP p z w→FreeMP p s t[E]

where  corresponds to , and  is the multiplication. The multiplication will be apparent if one expands the definition of Day convolution for $P$ and $P^*$. This interface stacks profunctors, and in each layer, it provides pure functions to simulate the parallel composition nature of a monoidal profunctor.

The following functions provide the necessary functions to build the free construction on monoidal profunctors,  insert a single profunctor into the free structure, and  provides a way of evaluating the structure, collapsing it into a single monoidal profunctor.

[B]toFreeMP::Profunctor p⇒p s t→FreeMP p s t[E]

[B]toFreeMP p=FreeMP diag fst p (MPempty ())[E]

[B]foldFreeMP::(Profunctor p,MonoPro q)⇒(pq)→FreeMP p s t→q s t[E]

[B]foldFreeMP  (Arr t)=dimap (92 95 →()) (λ()→t) arrr[E]

[B]foldFreeMP (Prof h) (FreeMP f g p mp)=dimap f g ((h p)⋆foldFreeMP (Prof h) mp)[E]

A free construction behaves like a list and, of course,  should provide a way to embed a plain profunctor into the free context.

[B]consMP::Profunctor p[25]
[25]⇒p a b→FreeMP p s t→FreeMP p (a,s) (b,t)[E]

[B]consMP pab (MPempty t)[31]
[31]=FreeMP id id pab (MPempty t)[E]

[B]consMP pab (FreeMP f g p fp)[31]
[31]=FreeMP (id⋆f) (id⋆g) pab (consMP p fp)[E]

and with it, an instance of  for the free structure can be defined as

[B]𝐢𝐧𝐬𝐭𝐚𝐧𝐜𝐞 Profunctor p⇒MonoPro (FreeMP p) 𝐰𝐡𝐞𝐫𝐞[E]

[5]mpempty=MPempty ()[E]

[5]MPempty t[16]
[34]=dimap snd (λx→(t,x)) q[E]

[16]⋆MPempty t[34]
[34]=dimap fst (λx→(x,t)) q[E]

[5](FreeMP f g p fp)[24]
[34]=dimap [43]
[43](assoc∘.(f⋆id)) ((g⋆id)∘.assoc^-1) (consMP p (fp⋆fq))[E]

where  and .

When  is an arrow, then  is an arrow. In order to define this instance one needs to collapse all parallel profunctors in order to make the sequential composition.

[B]𝐢𝐧𝐬𝐭𝐚𝐧𝐜𝐞 (MonoPro p,Arrow p)⇒Category (FreeMP p) 𝐰𝐡𝐞𝐫𝐞[E]

[14]=FreeMP (λx→(x,())) fst (arr id) (MPempty ())[E]

[14]=toFreeMP (fromFreeMP mpK.∘.fromFreeMP mq)[E]

[B]𝐢𝐧𝐬𝐭𝐚𝐧𝐜𝐞 (MonoPro p,Arrow p)⇒Arrow (FreeMP p) 𝐰𝐡𝐞𝐫𝐞[E]

[5]arr f[12]
[12]=FreeMP (λx→(x,())) fst (arr f) (MPempty ())[E]

It is good to remember that the type class  is the one that has the two methods  and , which represents the notion of a category in Haskell.

§ MONOIDAL PROFUNCTOR OPTICS - MONOCLES

Data accessors are an essential part of functional programming. They allow reading and writing a whole data structure or parts of it [19]. In Haskell, one needs to deal with Algebraic Data Types (ADTs) such as products (fields), sums, containers, function types, to name a few. For each of these structures, the action of handling can be a hard task and not compositional at all. To circumvent this problem, different type of data accessors were created, such as lenses, prisms, and traversables [9, 8]. These different notions of modular (composable) data accessors [19] were grouped together and called optics. Optics help to tackle the data accessor problem with the help of some category-theoretic constructions such as profunctors.

An optic is a general denotation to locate parts (or even the whole) of a data structure in which some action needs to be performed. Each optic deals with a different ADT, for example, the well-known lenses deal with product types, prisms with sum types, traversals with traversable containers, grates with function types, isos deals with any type but cannot change its shape, and so on. A general optic is a polymorphic type on a binary type constructor type with a typeclass restriction  on it.

[B]𝐭𝐲𝐩𝐞 Optic r s t a b=∀p∘.r p⇒p a b→p s t[E]

The idea of an optic is to have an in-depth look into get/set operations, for example, if one has a “big” data structure , it is possible to extract a piece of it, say , which can be written as a function . Whereas, if one provides a “big” structure , and a value  (which is a part of ), we can modify  into another “big” structure  (the structure might not change and the data still be ). This description is modelled by the function .

Both functions (get and set) are specializations of  yielding the type
[B]𝐭𝐲𝐩𝐞 Lens s t a b=∀p∘.Strong p⇒p a b→p s t[E]

Here,  is a profunctor dependent typeclass having the method  (it also has a method ). For example, one can recover a get function using a lens [19, 17], and to achieve that we use the profunctor  that is just the contravariant hom-functor:

[B]𝐧𝐞𝐰𝐭𝐲𝐩𝐞 Forget r a b=Forget {1.5mu runForget::a→r1.5mu}[E]

[B]get::Lens s t a b→s→a[E]

[B]get lens=runForget (lens (Forget id))[E]

Lenses help to give the intuition behind this profunctorial optics machinery, but this work will solely focus on the optic derived from a monoidal profunctor with
$\otimes = \times$, which combines grates and traversals. It will be called a monocle.

[B]𝐭𝐲𝐩𝐞 Monocle s t a b=∀p∘.MonoPro p⇒p a b→p s t[E]

A  locates every position of a product (tuple) type (which can be generalized to a finite vector [6]) while a  locates parts of it. We now list some basic monocles to observe their behavior. Furthermore, one can observe that those monocles can be generalized if dependent types are used.

[B]each2::MonoPro p⇒p a b→p (a,a) (b,b)[E]

[B]each2 p=p⋆p[E]

[B]each3::MonoPro p⇒p a b→p (a,a,a) (b,b,b)[E]

[B]each3 p=dimap flat3i flat3l (p⋆p⋆p)[E]

[B]each4::MonoPro p⇒p a b→p (a,a,a,a) (b,b,b,b)[E]

[B]each4 p=dimap flat4i flat4l (p⋆p⋆p⋆p)[E]

As one can observe,  deals with parallel composition of the argument  with itself using the  interface. The focus is on tuples of size 2. The monocles  and  deal with tuples of size 3 and 4 and depend on the tuple flattening functions.

[B]flat3l ((a,b),c)=(a,b,c)[E]

[B]flat3i (a,b,c)=((a,b),c)[E]

[B]flat4l (((a,b),c),d)=(a,b,c,d)[E]

[B]flat4i (a,b,c,d)=(((a,b),c),d)[E]

To have a better understanding of those Monocles we adapt the representation theorem of Jaskelioff and O'Connor [6] from functors to profunctors.

(Unary representation for profunctors) Consider an adjunction between profunctors $-^* \vdash U  : \mathcal{E} \to \mathcal{F}$, where $\mathcal{F}$ is small and $\mathcal{E}$ is a full
subcategory of $Prof(Set,Set)$, the family of profunctors $Iso_{A,B}(S,T) = (S \to A) \times (B \to T)$ gives the following isomorphism natural in $A, B$, and dinatural in $S,T$.

\[
\int_{P} UP(A,B) \to UP(S,T) \cong Iso^{*}_{A,B}(S,T),
\]

where $Iso^*$ is the free profunctor generated by $Iso$. Whenever the left-hand side end exists, the isomorphism holds.

Since the free monoidal profunctor exists and is of the form
\[ P^{*}(S,T) = (J + P \star P^*)(S,T),\]
this theorem helps us find the unary representation for monoidal profunctors.

The unary representation for monoidal profunctors is given by the isomorphism:

\[
\int_{P} P(A,B) \to P(S,T) \cong \sum\limits_{n \in \mathbb{N}} (S \to A^n) \times (B^n \to T)
\]

where $P$ ranges over all monoidal profunctors.

By theorem <ref>, it is enough to show that
\[ U(Iso^{*}_{A,B})(S,T) \cong \sum\limits_{n \in \mathbb{N}} (S \to A^n) \times (B^n \to T).  \]

This is proven using Yoneda, the fact that Day convolution preserves coproducts, and induction on $n$.

The right-hand side of the above isomorphism tells us that the source type can be split as a finite number of copies of a type , and a finite number of copies of a type  can be amalgamated in a type , which gives us a semantic for  such as . Using categorical tools to reason about  (the other functions can be understood similarly), one can rewrite it as follows.

[B]each2::MonoPro p⇒(s→(a,a))→((b,b)→t)→p a b→p s t[E]

[B]each2 f g p=dimap f g (p⋆p)[E]

Since theorem <ref> holds, one can interchangeably use the  or a more easy to reason type as
, but the limitation of the latter is obvious.

Actions can now be performed on a monocle, given the desired location; one can read/write any product (tuple) type.

[B]foldOf::Monoid a⇒Monocle s t a b→s→a[E]

[B]foldOf monocle=runForget (monocle (Forget id))[E]

This action tells that given a  (location) one can monoidally collect many parts  from the big structure  (in this case, tuples). For example,
[B]foldOf each3::Monoid a⇒(a,a,a)→a[E]
behaves in the same way as the function  does with lists, its evaluation on the value  gives  as expected. The list function  has a corresponding Monocle called ,

[B]foldMapOf::Monoid r⇒Monocle s t a b→(a→r)→s→r[E]

[B]foldMapOf monocle f=runForget (monocle (Forget f))[E]

which can locate all elements of a 3-element tuple with the expression B@>l<@
[B]foldMapOf each3::Monoid r⇒(a→r)→(a,a,a)→r[E]
as expected.

Every profunctorial optic has a so-called van Laarhoven [18] functorial representation. For a monocle, this representation can be obtained by the following function.

[B]convolute::(Applicative g,Functor f)⇒Monocle s t a b→(f a→g b)→f s→g t[E]

[B]convolute monocle f=unSISO (monocle (SISO f))[E]

If we specialize  using the identity functor , one gets the definition of a , which is a defined in the lens package [8].

[B]traverseOf::Applicative g⇒Monocle s t a b→(Id a→g b)→(Id s→g t)[E]

[B]traverseOf monocle=convolute monocle[E]

One can specialize  using the applicative functor , to get the van Laarhoven representation for grates (which depends on a Closed type class of Profunctors) [17].

[B]𝐜𝐥𝐚𝐬𝐬 Profunctor p⇒Closed p 𝐰𝐡𝐞𝐫𝐞[E]

[3]closed::p a b→p (x→a) (x→b)[E]

[B]zipFWithOf::Functor f⇒Monocle s t a b→(f a→Id b)→(f s→Id t)[E]

[B]zipFWithOf monocle=convolute monocle[E]
Monoidal profunctors with $\otimes = \times$ capture the essence of a grate and a traversal. Grates have a structured contravariant part (input) while traversals, the covariant one (output), while a monocle has both structures.

§ EFFECTFUL MONOIDAL PROFUNCTORS

The typeclass for monoidal profunctors  is defined in terms of a profunctor  over the (fictitious) base category of Haskell types and functions usually known as Hask.
However, the Day convolution allows us to use morphisms from other categories, instead of using Hask everywhere. This section presents a generalization of the class  which allows to use morphisms from other categories. We illustrate its use by applying it to morphisms from a Kleisli category, hence allowing effects to be lifted into the structure. The profunctor class will also have a modified form to lift two abstract morphisms instead of pure functions.

[B]𝐜𝐥𝐚𝐬𝐬 Category k⇒CatProfunctor k p 𝐰𝐡𝐞𝐫𝐞[E]

[5]catdimap::k a b→k c d→p b c→p a d[E]

A  represents a profunctor working with morphisms on an arbitrary category $\CC$ instead of $Hask$, and provides an interface to lift two of those abstract morphisms defined by the binary type constructor . This new class needs to be a multi-parameter type class because of the added constraint .

[B]𝐜𝐥𝐚𝐬𝐬 (Category k,CatProfunctor k p)⇒CatMonoPro k p|p→k 𝐰𝐡𝐞𝐫𝐞[E]

[16]::k s ()→k () t→p s t[E]

[16]::k s (a,c)→k (b,d) t→p a b→p c d→p s t[E]

It is good to remember that in the  class, the type of  is isomorphic to , and the type of  is isomorphic to . The functional dependency  allows to write the unit  having the same role as , and  also having the same role as 's  satisfying the same laws as seen before.

[B]cmpempty::p () ()[E]

[B]cmpempty=unitmp id id[E]

[B](⋆⋆)::CatMonoPro k p⇒p a b→p c d→p (a,c) (b,d)[E]

[B]p⋆⋆q=convolute id id p q[E]

As an example, one can work with  and  alongside a Kleisli arrow. That is, objects are types but morphisms are Kleisli arrows. The  instance in this example will permit computations to be lifted covariantly and contravariantly. The  gives a convolutional effect for computations and not just pure functions (as in 's ).

The Kleisli arrow is just a wrapped type:

[B]𝐧𝐞𝐰𝐭𝐲𝐩𝐞 Kleisli m a b=Kleisli {1.5mu runKleisli::a→m b1.5mu}[E]

having a lawful  instance as follows.

[B]𝐢𝐧𝐬𝐭𝐚𝐧𝐜𝐞 Monad m⇒Category (Kleisli m) 𝐰𝐡𝐞𝐫𝐞[E]

[5]id=Kleisli return[E]

[5](Kleisli bmc)∘.(Kleisli amb)=Kleisli (λa→(amb a)bmc)[E]

A datatype called  is a  with respect to the Kleisli arrow.

[B]𝐧𝐞𝐰𝐭𝐲𝐩𝐞 Lift t m a b=Lift {1.5mu runLift::m a→t m b1.5mu}[E]

This polymorphic type represents a general version of the function  used to lift monadic computations into a monad transformer [3]. A monad transformer is a way to stack two or more monads together in order to enable more than one effectful computation together [7, 11]. By packing lift into a profunctor concerning the Kleisli arrow, one gets ways to precompose and post-compose computations with a monad transformer's inner monad. For example, suppose a monad transformer  (where  is a monad). It is possible to use  to compose effectful computations in  having its results in the monad transformer.

[B]𝐢𝐧𝐬𝐭𝐚𝐧𝐜𝐞 (MonadT t,Monad m,Monad (t m))⇒CatProfunctor (Kleisli m) (Lift t m) 𝐰𝐡𝐞𝐫𝐞[E]

[9]catdimap (Kleisli f) (Kleisli g) (Lift h)=Lift$λma→[68]
[68]𝐥𝐞𝐭 [73]
[73]k=h (maf)[E]

[68]𝐢𝐧 kl[E]

As an important note,  is a  with , and . For a plain profunctor,  works only with a ,  need not be a monad transformer, and  needs only to be an . Hence this instance is substantially different from the mentioned one.

To work with a  instance with respect to the Kleisli arrow, a notion of reordering effects (commutativity) is needed.

[B]𝐢𝐧𝐬𝐭𝐚𝐧𝐜𝐞 (CommT t,Traversable m,Monad m,Monad (t m))⇒[E]

[5]CatMonoPro (Kleisli m) (Lift t m) 𝐰𝐡𝐞𝐫𝐞[E]

[9]cmpunit (Kleisli f) (Kleisli g)=Lift (λm→lift (mfg ()))[E]

[9]convolute (Kleisli f) (Kleisli g) (Lift h) (Lift l)=[E]

[28]𝐥𝐞𝐭 (ma,mc)=unzip' (msf)[E]

[28]𝐢𝐧 comm (fmap g (zip' ((h ma),(l mc))))[E]

After the  of function , the remaining expression will have the type . This can be fixed by building a class giving a function  to reorder those effects. A traversable instance is used here to provide that swap but other commutativity notions [7] may be used.

[B]𝐜𝐥𝐚𝐬𝐬 MonadT t⇒CommT t 𝐰𝐡𝐞𝐫𝐞[E]

[5]comm::(Monad m,Traversable m)⇒t m (m a)→t m a[E]

This setup provides a use of the maybe monad transformer  with
a monad like  which is traversable (all necessary type class instances can be found in the mtl [3]).

[B]𝐢𝐧𝐬𝐭𝐚𝐧𝐜𝐞 CommT MaybeT 𝐰𝐡𝐞𝐫𝐞[E]

[5]comm (MaybeT mna)=MaybeT (mnasequence)[E]

Using the monoidal profunctor  helps us deal with multiple monads at once, enabling us to deal with product types' computations. Consider the effectful function , in writer monad, that splits in two a list of  (or any Ord instance) by its order (in this case, lexicographical). One list for elements less or equal to the head, and the other has bigger elements than the head. The effect is logging, telling what the function is doing for debugging purposes.

[B]lsplit::[1.5mu String1.5mu]→Writer [1.5mu String1.5mu] ([1.5mu String1.5mu],[1.5mu String1.5mu])[E]

[B]lsplit (z:zs)=𝐝𝐨[E]

[5]xs←return (filter (<z) zs)[E]

[5]ys←return (filter (≥z) zs)[E]

[5]tell [1.5mu 34 Splitting: 34show zs34  into 34show xs34 , 34[76]
[76]show ys1.5mu][E]

[5]return (xs,ys)[E]

The function  below just concats two lists and logs this action.

[B]rsplit::String→([1.5mu String1.5mu],[1.5mu String1.5mu])→Writer [1.5mu String1.5mu] [1.5mu String1.5mu][E]

[B]rsplit l (xs,ys)=𝐝𝐨[E]

[5]tell [1.5mu 34 Merging: 34show xs[35]
[35]34 , 34l34 , and 34show ys1.5mu][E]

[5]return (xs[1.5mu l1.5mu]ys)[E]

A quicksort can be logged and stopped if an invalid value is found while keeping the logs of what the algorithm did (in this case an empty string). The instance of  helps with the splitting, and merging the sorted results inside this / context easily.

[B]qsort::[1.5mu String1.5mu]→MaybeT (Writer [1.5mu String1.5mu]) [1.5mu String1.5mu][E]

[B]qsort [1.5mu 1.5mu]=return [1.5mu 1.5mu][E]

[B]qsort xs=𝐝𝐨[E]

[5]guard (head xs≢34 34)[E]

[16]←runLift [28]
[28](lconvolute (Kleisli lsplit) lift' lift') (return xs)[E]

[16]←runKleisli [31]
[31]((Kleisli qsort)⋆(Kleisli qsort)) (ls,rs)[E]

[16]←runLift [28]
[28](rconvolute (Kleisli (rsplit (head xs))) lift' lift') (return (ls',rs'))[E]

[5]return ss[E]

The functions  and  have  (from typeclass ) function in the left and right similar as  and . For example,  and the right convolution is similar changing the id order. It is also possible to observe the use of a plain monoidal profunctor by using its multiplication since  is a Kleisli arrow which has a trivial  instance (it is isomorphic to a SISO with  and ). Finally, the expression  is , that is, the monad transformer's  in the monoidal profunctor setting.

§ RELATED WORK

Several of the results collected in this article are folklore. In the following, we point out the cases where a publication mentioning them is known to us.
Rivas and Jaskelioff introduce notions of computation as monoids [20], and this work follows their path presenting another notion that is not in that work and that has not been well explored in the community. The type class  is defined by Pickering, Gibbons, and Wu [19], but it was not their main focus. The representation of Monocles is also found in the work of Pickering, Gibbons and Wu [19] which states the relationship between a  and  by using an optic called . A similar representation of a Monocle was found in the work of O'Connor [17] and is called . This representation relies on a type class called , isomorphic to , which deals with tuples that use type-level naturals. Also in O'Connor's work, there is a mention of the type  which is called  here. A profunctor optic called  is defined by Román [21] which is also similar to Monocles. However, in this work we study for the first time the monoidal profunctor semantics of the mentioned optics.

The effectful monoidal profunctor and its examples are also new.

§ CONCLUSION

We have studied monoidal profunctors as monoids in a monoidal category of profunctors, shown that such category is symmetric closed, and obtained the free monoidal profunctor. We have shown how to implement monoidal profunctors in Haskell and have shown some applications related to optics and a generalization to apply monoidal profunctors in a Kleisli category that we call effectful monoidal profunctors. We would like to investigate applications of this extension to parallel and concurrent algorithms.

[1]
authorBryce Clarke, authorDerek
Elkins, authorJeremy Gibbons, authorFosco Loregiàn, authorBartosz Milewski, authorEmily Pillmore & authorMario Román (year2020):
titleProfunctor optics, a categorical update.
journalCoRR volumeabs/2001.07488.

[2]
authorBrian Day (year1970):
titleOn closed categories of functors.
In editorS. MacLane,
editorH. Applegate,
editorM. Barr,
editorB. Day,
editorE. Dubuc,
editorA. Pultr,
editorR. Street,
editorM. Tierney &
editorS. Swierczkowski, editors: booktitleReports of the Midwest Category Seminar IV,
publisherSpringer Berlin Heidelberg, addressBerlin,
Heidelberg, pp. pages1–38, 10.1007/BFb0079385.

[3]
authorAndy Gill:
titlemtl: Monad classes, using functional dependencies.
noteAccessed: 2019-05-28.

[4]
authorJohn Hughes (year2005):
titleProgramming with Arrows.
In: booktitleProceedings of the 5th International
Conference on Advanced Functional Programming, seriesAFP'04,
publisherSpringer-Verlag, addressBerlin, Heidelberg,
pp. pages73–129, 10.1007/11546382_2.

[5]
authorBart Jacobs, authorChris
Heunen & authorIchiro Hasuo (year2009): titleCategorical
semantics for arrows.
journalJournal of Functional Programming
volume19(number3-4), p. pages403–438,

[6]
authorMauro Jaskelioff &
authorRussell O'Connor
(year2015): titleA representation theorem for
second-order functionals.
journalJournal of Functional Programming
volume25, p. pagese13,

[7]
authorMark P. Jones &
authorLuc Duponcheel
(year1993): titleComposing Monads.
typeTechnical Report.

[8]
authorEdward Kmett:
titlelens: Lenses, Folds and Traversals.
noteAccessed: 2019-05-28.

[9]
authorT van Laarhoven:
titleWhere do I get my non-regular types?
noteAccessed: 2020-08-08.

[10]
authorTom Leinster (year2003):
titleHigher Operads, Higher Categories.

[11]
authorSheng Liang, authorPaul
Hudak & authorMark Jones (year1995): titleMonad
Transformers and Modular Interpreters.
In: booktitleProceedings of the 22nd ACM
SIGPLAN-SIGACT Symposium on Principles of Programming Languages,
seriesPOPL '95, publisherAssociation for Computing
Machinery, addressNew York, NY, USA, p.
pages333–343, 10.1145/199448.199528.

[12]
authorSam Lindley, authorPhilip
Wadler & authorJeremy Yallop (year2011): titleIdioms are
Oblivious, Arrows are Meticulous, Monads are Promiscuous.
journalElectronic Notes in Theoretical Computer
Science volume229(number5), pp. pages97
– 117, 10.1016/j.entcs.2011.02.018.
noteProceedings of the Second Workshop on Mathematically
Structured Functional Programming (MSFP 2008).

[13]
authorFosco Loregian
(year2020): titleCoend calculus.

[14]
authorConor Mcbride &
authorRoss Paterson
(year2008): titleApplicative Programming with
journalJ. Funct. Program.
volume18(number1), pp. pages1–13,

[15]
authorBartosz Milewski:
titleFree Monoidal Profunctors.
noteAccessed: 2019-10-20.

[16]
authorEugenio Moggi
(year1991): titleNotions of Computation and
journalInf. Comput.
volume93(number1), pp. pages55–92,

[17]
authorRussell O'Connor:
titleGrate: A new kind of Optic.
noteAccessed: 2019-02-02.

[18]
authorRussell O'Connor:
titleA Representation Theorem for Second-Order
noteAccessed: 2019-02-01.

[19]
authorMatthew Pickering,
authorJeremy Gibbons &
authorNicolas Wu (year2017):
titleProfunctor Optics: Modular Data Accessors.
journalThe Art, Science, and Engineering of
Programming volume1(number2),

[20]
authorExequiel Rivas &
authorMauro Jaskelioff
(year2017): titleNotions of computation as
journalJournal of Functional Programming
volume27, p. pagese21,

[21]
authorMario Román
(year2020): titleProfunctor optics and
journalArXiv volumeabs/2001.08045.

[22]
authorPhilip Wadler
(year1992): titleThe Essence of Functional
In: booktitleProceedings of the 19th ACM
SIGPLAN-SIGACT Symposium on Principles of Programming Languages,
seriesPOPL '92, publisherACM, addressNew
York, NY, USA, p. pages1–14, 10.1145/143165.143169.