🚀 go-pugleaf

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.