Making the point-free calculus less pointless

Functional programming is particularly well suited for equational reasoning – referential trans-parency ensures that expressions in functional programs behave as ordinary expressions in mathemat-ics. 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: “Associ-ated 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