pop@cs.umass.edu (05/31/90)
Surely one important point of functional programming is that it provides a basis for reasoning about programs, and for program transformation. This was certainly one of the considerations behind the development of Hope, but seems to have subsequently been under-emphasised. E.g. ML and Haskell do not feature a defined, manipulable internal representation of programs, in the way that LISP and Prolog do (more or less messily). Certainly a weak equivalence [in the sense that two function definitions are weakly equivalent if, when they terminate, they terminate with equal results] is found useful by mathematicians [e.g. (x^2-1)/(x-1) is often simplified to x+1], and, like type-checking, can provide the basis for greater assurance that a program is correct. Regarding the equational definitions of functions as _more_ than syntactic sugar provides support for reasoning about programs in a way that concurs with people's basic mathematical training. Thus it would seem healthy to regard treat such function definitions as potential inputs to a term-rewriting system, and to discourage order-dependent definitions, however meaningful they may be when translated into the lambda calculus. No doubt a smart compiler can optimise out the redundant checks. The problem with patterns and data-abstraction is that the idea of "constructor" has become too mechanistic. The requirement that a function symbol f can be used at in inner level on the left of a function definition is simply that it be algebraically free, i.e. f(x1,...xn) = f(y1...yn) implies x_i=y_i, all i. This requirement of being free was reasonably clearly expressed in the POP-2 reference manual (accepting that POP-2 data-structures are updatable, so the form of the statement is somewhat more complicated). A particular implementation, namely record classes, is introduced in a subsequent section of the manual. Subsequent language designers seem to have lost sight of this view, and have tied algebraically free functions to particular implementations, with unfortunate consequences for efficiency etc.
fs@rex.cs.tulane.edu (Frank Silbermann) (06/05/90)
In article <14921@dime.cs.umass.edu> pop@cs.umass.edu () writes: > > Surely one important point of functional programming > is that it provides a basis for reasoning about programs, > and for program transformation. E.g. ML and Haskell > do not feature a defined, manipulable internal representation > of programs, in the way that LISP and Prolog do. > > Regarding the equational definitions of functions > as _more_ than syntactic sugar provides support > for reasoning about programs in a way that concurs > with people's basic mathematical training. This would be nice, but unfortunately, the resulting languages do not seem to be computable (not merely difficult, but impossible, at least in the higher-order case). This is why I consider pattern-matching to be a syntactic sugar; a shorthand for programmers which provides a non-enforced documentation of his intentions. > Thus it would seem healthy to treat such definitions > as potential inputs to a term-rewriting system. What does term-rewriting have to do with any theory of domains and mappings (e.g. programming with functions)? Frank Silbermann fs@rex.cs.tulane.edu Tulane University, New Orleans, Louisianna, USA