nLab arrow (in computer science)

Idea

In computer science, the notion of arrows [Hughes 2000] generalizes that of monads in computer science.

More concretely, the notion of arrow abstracts that of the hom-profunctor of the Kleisli category $\mathrm{Kl}(T)$ for a strong monad $T \colon \mathbf C \to \mathbf C$ as an endoprofunctor on $\mathbf C$.

Therefore, an arrow $A \colon \mathbf C^{op} \times \mathbf C \to \mathbf{Set}$ can be thought as a putative replacement of $\mathrm{Hom}_{\mathbf C} \colon \mathbf C^{op} \times \mathbf C \to \mathbf{Set}$. In fact an arrow comes equipped with a transformation $\mathrm{arr} : \mathrm{Hom}_{\mathbf C} \Rightarrow A$ that lift morphisms of $\mathbf C$ to the ‘augmented’ morphisms given by $A$, and with a transformation $\ggg : A \circ A \Rightarrow A$ that behaves like a composition operation. Then one requires that $\ggg$ is associative and that $\mathrm{arr}(1_a)$ is the unit of this operation.

These data makes $A$ a promonad on $\mathbf C$, i.e. a monad on $\mathbf C$ in the bicategory of profunctors. Since every monad on $\mathbf{Set}$ (or on any reasonable enriching base where programmers work) is strong, arrows traditionally generalize the hom-profunctor of strong monads. The additional requirement that $A$ is a strong profunctor (and the laws it is required to satisfy) imply that an arrow is a strong monad in the bicategory of profunctors (Asada10).

Definition

Definition

An arrow $A$ on a monoidal category $\mathbf C$ is a monoid in the category of strong endoprofunctors on $\mathbf C$, i.e. it’s a functor $\mathbf C^{op} \times \mathbf C \to \mathbf{Set}$ equipped with the following structure:

1. A natural family of morphisms $\mathrm{arr} : \mathbf C(a,b) \to A(a,b)$ (the unit of the monoid),
2. A natural family of morphisms called composition $\ggg : A(a,b) \times A(b,c) \to A(a,c)$ (the multiplication of the monoid), which satisfy an associative law and for which $\mathrm{arr}_{a,a}(1_a)$ is the unit,
3. A family of morphisms called strength $s_{a,b,m} : A(a,b) \to A(m \otimes a, m \otimes b)$, which is dinatural in $m$ and natural in $a, b$, and satisfies coherence laws that make $(A, s)$ a strong profunctor.

References

Arrows originate in Section 2 of

• John Hughes, Generalising monads to arrows, Sci. Comput. Program. 37 1-3 (2000) 67-111 [doi:10.1016/S0167-6423(99)00023-4, pdf]

The ‘justification’ of arrows as strong monads in $\mathbf{Prof}$ is given in

• Kazuyuki Asada, Arrows are strong monads, 2010 (pdf)

Comparisons of monads with applicative functors (also known as idioms) and with arrows (in computer science) are in

• Sam Lindley?, Philip Wadler, Jeremy Yallop?, Idioms are Oblivious, Arrows are Meticulous, Monads are Promiscuous, Electron. Notes Theor. Comput. Sci. 229(5), pp. 97–117, 2011 (doi:10.1016/j.entcs.2011.02.018)
• Exequiel Rivas?, Relating Idioms, Arrows and Monads from Monoidal Adjunctions, MSFP@FSCD 2018, pp. 18–33 (arXiv:1807.04084, doi:10.4204/EPTCS.275.3)