Categorifying Computations into Components via Arrows as Profunctors

The notion of arrow by Hughes is an axiomatization of the algebraic structure possessed by structured computations in general. We claim that an arrow also serves as a basic component calculus for composing state-based systems as components—in fact, it is a categorified version of arrow that does so. In this paper, following the second author's previous work with Heunen, Jacobs and Sokolova, we prove that a certain coalgebraic modeling of components—which generalizes Barbosa's—indeed carries such arrow structure. Our coalgebraic modeling of components is parametrized by an arrow A that specifies computational structure exhibited by components; it turns out that it is this arrow structure of A that is lifted and realizes the (categorified) arrow structure on components. The lifting is described using the first author's recent characterization of an arrow as an internal strong monad in Prof, the bicategory of small categories and profunctors.