nLab arrow (in computer science)

Contents

Contents

Idea

A generalization of the concept of monad (in computer science). In particular, it generalizes the attitude that monads in computer science are useful insofar as they generate a Kleisli category. Thus an arrow abstracts the hom-profunctor of Kl(T)\mathrm{Kl}(T) for a strong monad T:CCT: \mathbf C \to \mathbf C as an endoprofunctor on C\mathbf C.

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

These data makes AA a promonad? on C\mathbf C, i.e. a monad on C\mathbf C in the bicategory of profunctors. Since every monad on Set\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 AA 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 AA on a monoidal category C\mathbf C is a monoid in the category of strong endoprofunctors on C\mathbf C, i.e. it’s a functor C op×CSet\mathbf C^{op} \times \mathbf C \to \mathbf{Set} equipped with the following structure:

  1. A natural family of morphisms arr:C(a,b)A(a,b)\mathrm{arr} : \mathbf C(a,b) \to A(a,b) (the unit of the monoid),
  2. A natural family of morphisms called composition :A(a,b)×A(b,c)A(a,c)\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 arr a,a(1 a)\mathrm{arr}_{a,a}(1_a) is the unit,
  3. A family of morphisms called strength s a,b,m:A(a,b)A(ma,mb)s_{a,b,m} : A(a,b) \to A(m \otimes a, m \otimes b), which is dinatural in mm and natural in a,ba, b, and satisfies coherence laws that make (A,s)(A, s) a strong profunctor.

References

Arrows originate in Section 2 of

The ‘justification’ of arrows as strong monads in Prof\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

Last revised on October 5, 2021 at 12:52:15. See the history of this page for a list of all contributions to it.