nLab arrow (in computer science)

Redirected from "arrows in computer science".
Contents

Contents

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 Kl(T)\mathrm{Kl}(T) for a strong monad T:CCT \colon \mathbf C \to \mathbf C as an endoprofunctor on C\mathbf C.

Therefore, an arrow A:C op×CSetA \colon \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} \colon \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 January 12, 2024 at 19:52:29. See the history of this page for a list of all contributions to it.