The Arrow Calculus

February 5, 2021 Jeremiah Hendren

The Arrow Calculus

Lindley, Sam, Philip Wadler, and Jeremy Yallop
Journal of Functional Programming 20, no. 1 (2010): 51-69
https://doi.org/10.1016/j.entcs.2011.02.018

Formally, arrows are defined by extending simply typed lambda calculus with three constants satisfying nine laws. And here is where the problems start. While some of the laws are easy to remember, others are not. Further, arrow expressions written with these constants use a “pointless” style of expression that can be hard to read and to write. (Not to mention that “pointless” is the last thing arrows should be.) Fortunately, Paterson introduced a notation for arrows that is easier to read and to write, and in which some arrow laws may be directly expressed (Paterson 2001). But for all its benefits, Paterson’s notation is only a partial solution. It simply abbreviates terms built from the three constants, and there is no claim that its laws are adequate for all reasoning with arrows. Syntactic sugar is an apt metaphor: it sugars the pill, but the pill still must be swallowed.

Sam Lindley et al.

See this gallery in the original post