*Joseph A. Goguen, Higher Order Functions Considered Unnecessary for Higher Order Programming (1987).*

It is often claimed that the essence of functional programming is the use of functions as values, i.e., of higher order functions, and many interesting examples have been given showing the power of this approach. Unfortunately, the logic of higher order functions is difficult, and in particular, higher order unication is undecidable. Moreover (and closely related), higher order expressions are notoriously difficult for humans to read and write correctly. However, this paper shows that typical higher order programming examples can be captured with just first order functions, by the systematic use of parameterized modules, in a style that we call parameterized programming. This has the advantages that correctness proofs can be done entirely within first order logic, and that interpreters and compilers can be simpler and more efficient. Moreover, it is natural to impose semantic requirements on modules, and hence on functions. A more subtle point is that higher order logic does not always mix well with subsorts, which can nonetheless be very useful in functional programming by supporting the clean and rigorous treatment of partially dened functions, exceptions, overloading, multiple representation, and coercion. Although higher order logic cannot always be avoided in specification and verification, it should be avoided wherever possible, for the same reasons as in programming. This paper contains several examples, including one in hardware verification. An appendix shows how to extend standard equational logic with quantification over functions, and justifies a perhaps surprising technique for proving such equations using only ground term reduction.

This (old paper) proposes an interesting approach for formulating functional programs. But can this truly subsume all uses of higher order functions? I don't see the paper address how the uses of higher order functions *in general* can be replaced (not that I have a counterexample in mind).

Anyone familiar with the OBJ language? Do other languages share this notion of 'modules', 'theories'?

## Recent comments

1 min 47 sec ago

12 min 36 sec ago

2 hours 17 min ago

9 hours 8 min ago

10 hours 40 min ago

13 hours 45 min ago

13 hours 58 min ago

14 hours 16 min ago

15 hours 46 sec ago

17 hours 17 min ago