Arrow (computer science)

In computer science, arrows provide a more general interface to computation than monads. Monads essentially provide a sequential interface to computation: one can build a computation out of a value, or sequence two computations. Arrows provide more possibilities, including expressing (true, nondeterministic) parallel computation. Indeed, monads turn out to be equivalent to arrows of a particular kind, ArrowApply. Because arrows carry more type information than just the result type, composition can be more efficient—for example, eliminating space leaks.

Arrows have found use in functional reactive programming.

Definition

As a prerequisite, we define a category of types. It is given by:

• a type constructor $\text{hom}$ which takes two type parameters
• for any type A, an object $\text{id}: \text{hom} \, A \, A$
• for any three types A, B, C an operator $\circ: \text{hom} \, B \, C \rarr \text{hom} \, A \, B \rarr \text{hom} \, A \, C$

subject to the following laws:

• $\text{id} \circ f = f \circ \text{id} = f$
• $f \circ \left( g \circ h \right) = \left( f \circ g \right) \circ h$

Note that $\rarr$ defines a category of types, with the obvious choices for $\text{id}$ and $\circ$.

Alternative notations are defined for the composition operator:

$\lll: \text{hom} \, B \, C \rarr \text{hom} \, A \, B \rarr \text{hom} \, A \, C = (\circ)$

$\ggg: \text{hom} \, A \, B \rarr \text{hom} \, B \, C \rarr \text{hom} \, A \, C = \text{flip} \, (\circ)$.

An arrow is a category of types endowed with the following functions:

• $\text{arr}: (A \rarr B) \rarr \text{hom} \, A \, B$
• $\text{first}: \text{hom} \, A \, B \rarr \text{hom} \, (A \times C) \, (B \times C)$
• $\text{second}: \text{hom} \, A \, B \rarr \text{hom} \, (C \times A) \, (C \times B )$
• $\text{parcomp}: \text{hom} \, A \, B \rarr \text{hom} \, A' \, B' \rarr \text{hom} \, (A \times A') \, (B \times B')$
• $\text{fanout}: \text{hom} \, A \, B \rarr \text{hom} \, A \, B' \rarr \text{hom} \, A \, (B \times B')$;

subject to the following laws:

• $(\text{arr} \, f) \circ (\text{arr} \, g) = \text{arr} \, (f \circ g)$
• $\text{first} \, (\text{arr} \, f) = \text{arr} \, (\text{first} \, f)$
• $\text{second} \, (\text{arr} \, f) = \text{arr} \, (\text{second} \, f)$
• $\text{parcomp} \, (\text{arr} \, f) \, (\text{arr} \, g) = \text{arr} \, ( \text{parcomp} \, f \, g)$
• $\text{fanout} \, (\text{arr} \, f) \, (\text{arr} \, g) = \text{arr} \, ( \text{fanout} \, f \, g)$
• $\text{first} \, (f \circ g) = (\text{first} \, f) \circ (\text{first} \, g)$
• $\text{second} \, (f \circ g) = (\text{second} \, f) \circ (\text{second} \, g)$

where the $\rarr$ category of types is extended to an arrow as follows:

• $\text{arr}: (A \rarr B) \rarr A \rarr B = f \mapsto f$
• $\text{first}: (A \rarr B) \rarr A \times C \rarr B \times C = f \mapsto (a, \, c) \mapsto (f \, a, \, c)$
• $\text{second}: (A \rarr B) \rarr C \times A \rarr C \times B = f \mapsto (c, \, a) \mapsto (c, \, f \, a)$
• $\text{parcomp}: (A \rarr B) \rarr (A' \rarr B') \rarr A \times A' \rarr B \times B' = f \mapsto f' \mapsto (a, \, a') \mapsto ( f\, a, \, f' \, a')$
• $\text{fanout}: (A \rarr B) \rarr (A \rarr B') \rarr A \rarr B \times B' = f \mapsto f' \mapsto a \mapsto ( f\, a, \, f' \, a)$

Arrows with choice

We may extend the arrow construct with the ability to choose between alternative computation paths. An arrow with choice is characterized by the following functions:

• $\text{left}: \text{hom} \, A \, B \rarr \text{hom} \, (A + C) \, (B + C)$
• $\text{right}: \text{hom} \, A \, B \rarr \text{hom} \, (C + A) \, (C + B )$
• $\text{choose}: \text{hom} \, A \, B \rarr \text{hom} \, A' \, B' \rarr \text{hom} \, (A + A') \, (B + B')$
• $\text{fanin}: \text{hom} \, A \, B \rarr \text{hom} \, A' \, B \rarr \text{hom} \, (A + A') \, B$;

subject to the following laws:

• $\text{left} \, (\text{arr} \, f) = \text{arr} \, (\text{left} \, f)$
• $\text{right} \, (\text{arr} \, f) = \text{arr} \, (\text{right} \, f)$
• $\text{choose} \, (\text{arr} \, f) \, (\text{arr} \, g) = \text{arr} \, ( \text{choose} \, f \, g)$
• $\text{fanin} \, (\text{arr} \, f) \, (\text{arr} \, g) = \text{arr} \, ( \text{fanin} \, f \, g)$
• $\text{left} \, (f \circ g) = (\text{left} \, f) \circ (\text{left} \, g)$
• $\text{right} \, (f \circ g) = (\text{right} \, f) \circ (\text{right} \, g)$

where the $\rarr$ arrow is endowed with the following definition:

• $\text{fanin}: (A \rarr B) \rarr (A' \rarr B) \rarr (A + A') \rarr B =$$f \mapsto f' \mapsto x \mapsto \begin{cases} f \, a & \text{if} \ x = \text{inl} \, a \\ f' \, a' & \text{if} \ x = \text{inr} \, a' \end{cases}$
• $\text{choose}: (A \rarr B) \rarr (A' \rarr B') \rarr (A + A') \rarr (B + B') =$$f \mapsto f' \mapsto x \mapsto \begin{cases} \text{inl} \, (f \, a) & \mbox{if } x = \text{inl} \, a \\ \text{inr} \, (f' \, a') & \text{if} \ x = \text{inr} \, a' \end{cases}$
• $\text{left}: (A \rarr B) \rarr (A + C) \rarr (B + C) = f \mapsto \text{choose} \, f \, \text{id}$
• $\text{right}: (A \rarr B) \rarr (C + A) \rarr (C + B) = f \mapsto \text{choose} \; \text{id} \, f$

Arrows with application

Arrows with application extend the basic arrow type with an application morphism:

• $\text{app}: \text{hom} \, ((\text{hom} \, A \, B) \times A) \, B$

The $\rarr$ arrow has an application morphism, apply:

• $\text{app}: (A \rarr B, \, A) \rarr B = (f, \, a) \mapsto f \, a$

Kleisli arrows

For any monad M, functions of type $A \rarr \mathrm{M} \, B$ form a category of types, called the Kleisli category for the monad. Its definition is as follows:

• $\text{hom} \, A \, B \equiv A \rarr \mathrm{M} B$
• $\text{id}: A \rarr \mathrm{M} \, A = \text{return}$
• $\circ: (B \rarr \mathrm{M} \, C) \rarr (A \rarr \mathrm{M} \, B) \rarr A \rarr \mathrm{M} \, C = f \mapsto g \mapsto a \mapsto \text{bind} \, (g \, a) \, f$

The Kleisli category is also an arrow:

• $\text{arr}: (A \rarr B) \rarr A \rarr \mathrm{M} \, B = f \mapsto \text{return} \circ f$
• $\text{first}: (A \rarr \mathrm{M} \, B) \rarr (A \times C) \rarr \mathrm{M} \, (B \times C) = f \mapsto (a, \, c) \mapsto \text{bind} \, (f \, a) \, (b \mapsto \text{return} \, (b, \, c))$
• $\text{second}: (A \rarr \mathrm{M} \, B) \rarr (C \times A) \rarr \mathrm{M} \, (C \times B) = f \mapsto (c, \, a) \mapsto \text{bind} \, (f \, a) \, (b \mapsto \text{return} \, (c, \, b))$
• $\text{parcomp}: (A \rarr \mathrm{M} \, B) \rarr (A' \rarr \mathrm{M} \, B') \rarr (A \times A') \rarr \mathrm{M} \, (B \times B') = f \mapsto f' \mapsto (\text{second} \, f') \, \circ \, (\text{first} \, f)$
• $\text{fanout}: (A \rarr \mathrm{M} \, B) \rarr (A \rarr \mathrm{M} \, B') \rarr A \rarr \mathrm{M} \, (B \times B') = f \mapsto f' \mapsto a \mapsto \text{parcomp} \, f \, f' \, (a, \, a)$

The Kleisli category is an arrow with choice:

• $\text{fanin}: (A \rarr \mathrm{M} \, B) \rarr (A' \rarr \mathrm{M} \, B) \rarr (A + A') \rarr \mathrm{M} \, B = f \mapsto f' \mapsto x \mapsto \begin{cases} f \, a & \text{if} \ x = \text{inl} \, a \\ f' \, a' & \text{if} \ x = \text{inr} \, a' \end{cases}$
• $\text{choose}: (A \rarr \mathrm{M} \, B) \rarr (A' \rarr \mathrm{M} \, B') \rarr (A + A') \rarr \mathrm{M} \, (B + B') = f \mapsto f' \mapsto x \mapsto \begin{cases} g \, a & \text{if} \ x = \text{inl} \, a \\ g' \, a' & \text{if} \ x = \text{inr} \, a' \end{cases}$ where $\begin{align} g = & ((\text{return} \, \text{inl}) \circ f) \\ g' = & ((\text{return} \, \text{inr}) \circ f')\end{align}$
• $\text{left}: (A \rarr \mathrm{M} \, B) \rarr (A + C) \rarr \mathrm{M} \, (B + C) = f \mapsto x \mapsto \begin{cases} g \, a & \text{if} \ x = \text{inl} \, a \\ \text{return} \, ( \text{inr} \, c) & \text{if} \ x = \text{inr} \, c \end{cases}$ where $g = ((\text{return} \, \text{inl}) \circ f)$
• $\text{right}: (A \rarr \mathrm{M} \, B) \rarr (C + A) \rarr \mathrm{M} \, (C + B) = f \mapsto x \mapsto \begin{cases} \text{return} \,(\text{inl} \, c) & \text{if} \ x = \text{inl} \, c \\ g \, a & \text{if} \ x = \text{inr} \, a\end{cases}$ where $g = ((\text{return} \, \text{inr}) \circ f)$

The Kleisli category is an arrow with application:

• $\text{app}: (A \rarr \mathrm{M} \, B) \times A \rarr \mathrm{M} \, B = (f, \, x) \mapsto f \, x$

Conversely, given any arrow with application, the corresponding monad $\text{hom} \, 1 \, B$ (where $1$ denotes the unit type) is defined by the following functions:

• $\text{return}: B \rarr \text{hom} \, 1 \, B = x \mapsto \text{arr} (a \mapsto x)$
• $\text{bind}: (\text{hom} \, 1 \, B) \rarr (B \rarr \text{hom} \, 1 \, B') \rarr (\text{hom} \, 1 \, B') = m \mapsto f \mapsto \text{app} \circ (\text{arr} (x \mapsto (f \, x, ()))) \circ m$

The fmap and join functions are:

• $\text{join}: (\text{hom} \, 1 \, (\text{hom} \, 1 \, B)) \rarr (\text{hom} \, 1 \, B) = f \mapsto \text{app} \circ (\text{arr} (x \mapsto (f \, x, ())))$
• $\text{fmap}: (B \rarr B') \rarr (\mathrm{hom} \, 1 \, B) \rarr (\mathrm{hom} \, 1 \, B') = f \mapsto m \mapsto \text{app} \circ (\text{arr} (x \mapsto (\text{arr} \, (a \mapsto f \, x), ()))) \circ m$

External links

• Arrows: A General Interface to Computation
• “Generalising Monads to Arrows”, John Hughes, in Science of Computer Programming 37, pp67–111, May 2000.
• A New Notation for Arrows, Ross Paterson, in ICFP, Sep 2001.
• Arrows and Computation, Ross Paterson, in The Fun of Programming, Palgrave, 2003.
• Arrow notation ghc manual