Home » forums » LtU Forum

Higher Order Functions Considered Unnecessary for Higher Order Programming

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 uni cation 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 fi rst 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 fi rst 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 de ned functions, exceptions, overloading, multiple representation, and coercion. Although higher order logic cannot always be avoided in specifi cation and veri fication, it should be avoided wherever possible, for the same reasons as in programming. This paper contains several examples, including one in hardware verifi cation. An appendix shows how to extend standard equational logic with quanti fication over functions, and justi fies 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'?

By irisjae at 2018-07-12 17:14 | LtU Forum | previous forum topic | next forum topic | other blogs | 6590 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

This first order style can

This first order style can encode all uses of higher order functions, but I wouldn't say that it can subsume them. There are lots of examples where higher order style is more natural.

A more subtle point is that higher order logic does not always mix well with subsorts

This claim isn't well argued by the link you've given, linking only to a pay-walled paper. And anyway, claims that "X does not mix well with Y" can usually be translated to "I don't understand X and Y very well."

I think modules & theories are a good idea (the working name of my language is Theory), but mine are first class / higher order. On the balance, I think my language is closer in flavor to typical functional programming language built on type theory than to the OBJ family, which doesn't seem to have many descendants.

By Matt M at Thu, 2018-07-12 18:38 | login or register to post comments

Argument seems to rely on notation

The author claims

However, a language with sufficiently powerful parameterized modules does not need higher order functions

IIUC, the number of parameterized modules in any program is statically boundable while the number of higher order functions allocated by a program may depend on input, so parameterized modules are not a 1:1 substitute for high order functions that close over state.

The claim seems to be that some specific notational choices make working with parameterized modules as convenient as higher order functions:

On the other hand, the notational overhead of theories and views is excessive for applying just one function. However, this is exactly the case where our abbreviated view and operation notations can be used to advantage. And we should not forget that it can be much more difficult to reason with higher order functions than with first order functions;

(emphasis added)

I'm unsure but it seems that the count of views and theories are also statically boundable. I'd be much less skeptical that they "subsume all uses of higher order functions" if the count of at least one of (modules, theories, views) were not statically boundable.

By mikesamuel at Thu, 2018-07-12 18:54 | login or register to post comments