Refactoring in Tunes
Tue, 11 Jan 2000 02:02:25 +0100
> > From: Francois-Rene Rideau [mailto:firstname.lastname@example.org]
> > For any "refactoring" trick, you can find a decomposition of it into
> > nice and general metaprogramming rules. Massimo already talked about
> > lambda-abstraction and beta-expansion: concepts indeed difficult to
> > express if at all in languages such as C, C++, Java, but trivial in
> > functional programming languages such as LISP, FORTH, ML,
> > Haskell, etc.
> ...and irrelevant to computer science in general. Lambda calculus has been
> a huge drag on computer science (I assert), and the sooner we get rid of it,
> the better. I posted a link to the 'Joy' page a bit earlier; take a look
> for a study of computation theory completely without lambda calculus.
> > The fact that such operations be done before runtime leads us in the realms
> > of "partial-" or staged evaluation. Combining them leads us to substitution,
> > and finding the right substitution is unification (which can get pretty
> > difficult for higher-order terms).
> And none of this is relevant without lambda calculus. Pretty neat, huh?
Lambda calculus and unification not relevant to computer science
in general? Bill, this is an hazardous statement. :o)
Seriously, too often lambda calculus is presented as an esoteric
subject, but it's not so complicated (at least the basic
principles): it talks about function application and with lambda
notation you are not forced to name a function. Next step (in
semplification) are combinators that avoids variables, like in
Forth. As noticed from Henry Baker in "Linear Logic and
Permutation Stacks -- The Forth Shall Be First", p. 5:
HTML - ftp://ftp.netcom.com/pub/hb/hbaker/ForthStack.html
or Postscript - ftp://ftp.netcom.com/pub/hb/hbaker/ForthStack.ps.Z
FORTH IS A SYSTEM OF LINEAR COMBINATORS
Combinatory logic [Curry58] is a logical structure which is
closely related to the lambda calculus [Church41]. Lambda calculus
talks about names and substitutions in expression trees, while
combinatory logic achieves the same "computations", but without
needing any names. [my note: but performing substitutions]
Most Forth operators take their operands from the top of the stack
and return their values to the top of the stack. A persual of this
Forth code reveals the absence of variable names which is
characteristics of combinators. The programming of Forth operators
can therefore be seen as the construction of larger combinators
from smaller ones. A Forth which incorporates only stack
permutation operations like swap, rotate and roll must be linear,
because it has no copying or killing operators.
Moreover, the principal data structure of most lamda-based
functional languages, the list, is isomorphic to (is substantially
the same as) the principal data structure of Forth, the stack. The
underlying implementation of some (many?) functional (and probably
logic) languages is based on combinators, while Forth shows that
is praticable to program directly with combinators (and with RPN,
Reverse Polish Notation).
The interesting (at the first look) link about Joy, that you had
post here, says that it's based on combinators (even).
Unification is a fundamental mechanism in Prolog (permit procedure
invocation, from a procedural point of view), in languages based
on term rewriting and functional languages. It allow type
inference. An ad-hoc mechanism of unification is "regular
In my not so humble opinion (I'm joking, of course ;-) these
subjects are not irrelevant. But I'm always open to new ideas.