[Prev][Next][Index][Thread]

[goguen@csl.sri.com: higher order functions considered unnecessary]

To: fp@YALE.ARPA
Cc: goguen@csl.sri.com
Subject: higher order functions considered unnecessary
Date: Tue, 05 Jan 88 18:58:28 -0800
From: goguen@csl.sri.com

I have just finished a paper which some of you might find amusing; the
abstract is appended below.  If you want a hardcopy, just send me a msg with
your hardcopy address.  Best wishes for the New Year to everyone on the list!
Cheers, Joseph

#########################################################################
Higher-Order Functions Considered Unnecessary for Higher-Order Programming
  Joseph A. Goguen

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 unification is undecidable.  Moreover (and closely related), higher
order expressions are notoriously difficult for humans to read and write
correctly.  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 interpreters and compilers can be simpler and more
efficient.  A more subtle, but still important, point is that higher order
logic does not mix well with *order sorted logic*.  However, subsorts are very
useful in functional programming, since they support the clean and rigorous
treatment of partially defined 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.  Some examples are given,
including a hardware verification example, and an appendix justifies a perhaps
surprising technique for proving equations with second quantifiers using only
first order reduction.

--------