Making the point-free calculus less pointless
Alcino Cunha, Jorge Sousa Pinto · Portuguese National Funding Agency for Science, Research and Technology (RCAAP Project by FCT) · 2004
Functional programming is particularly well suited for equational reasoning – referential transparency ensures that expressions in functional programs behave as ordinary expressions in mathematics. However, unstructured programming can still difficult formal treatment. As such, when John Backus proposed a new functional style of programming in his 1977 ACM Turing Award lecture, the main features were the absence of variables and the use of functional forms or combinators to combine existing functions into new functions [1]. The choice of the combinators was based not only on their programming power, but also on the power of the associated algebraic laws. Quoting Backus: “Associated with the functional style of programming is an algebra of programs [. . . ] This algebra can be used to transform programs and to solve equations whose “unknowns” are programs in much the same way one transforms equations in high-school algebra”. This style of programming is usually called point-free, as opposed to the point-wise style, where the arguments are explicitly stated. The basic set of combinators used in this paper as been already extensively presented in many publications, such as [6], and includes the typical products, with split (· M ·) and projections fst and snd, sums, with either (· O ·) and injections inl and inr, and exponentials, with curry · and application ap. Although the point-free style has a rich calculus for reasoning about programs, there are still many authors that resort to the point-wise style both for programming and for calculation. They claim that the point-free style is not very natural since the intuitive meaning of programs can easily be lost, and jokingly call it the pointless style. In fact, we agree that some point-free derivations are very long and tedious, namely when dealing with higher-order functions. However, we don’t think this is an intrinsic disadvantage of point-free, but merely lack of adequate combinators and proof methodology. As such, the objective of this work is to improve the machinery that is used to perform point-free calculations, namely in a higher-order setting. As Jeremy Gibbons puts it [3], “We are interested in extending what can be calculated precisely because we are not interested in the calculations themselves [. . . ]”, or, in other words, we aim at extending the calculus with new useful operators that help reducing the burden of proofs just to the creative parts. Point-free programming is usually complemented with extensive use of recursion patterns – higherorder operators that encapsulate typical patterns of recursion, such as the well-known fold or catamorphism. They prevent the use of arbitrary recursive definitions, and also have a nice set of equational laws. Although initially they were only defined for lists, it became clear that they could be generalized for any recursive data type viewed as fixed point of a functor [5]. In this paper we will only use the catamorphism, that given a function of type g : F A→ A is denoted by (|g|)F : μF → A, the function that builds its result by replacing the constructors of the input by g. One of the most important laws about this recursion operator is fusion – given a strict f , if f ◦ g = h ◦ Ff then f ◦ (|g|)F = (|h|)F . Suppose that we want to obtain a efficient version of the reverse function using the accumulation strategy introduced by Richard Bird [2]. This technique uses fusion to derive it from an inefficient version using the concatenation operator cat : List A× List A→ List A.