Gary (and others),
I know not everyone is familiar with the lambda calculus or its variants, so I
feel compelled to qualify your potentially misleading (not intentionally, of
course) statement that "all but the last two [term] expansions...are the
fundamental elements of McCarthy's original Lisp." While it is true that these
term expansions (constants, variables, application and abstraction--by any other
name) comprise the "fundamental elements of McCarthy's original Lisp," it should
be pointed out that Lisp is by no means their progenitor. Rather, this model of
computation is more properly attributed to the lambda calculus of Church and
Kleene, from way back in the 1930's. Further, these sorts of terms form the
basis not only for Lisp, but also for almost(*) every other functional
programming language in existence. To be perfectly clear: Lisp has no special
claim to them.
(*) = There are strange, painful languages composed entirely of combinators, for
The two term expansions which are different from Lisp's set are, of course,
pattern abstraction and the fixpoint primitive. You did a good job of explaining
*what* fixed point combinators do, but I would also like to explain (for the
benefit of the others) *why* the particular calculus I'm advancing "needs" a
fixpoint primitive, whereas a Lisp does not. (It's not an important point,
however). Briefly put, in variants of the *untyped* lambda calculus (e.g.,
loosely speaking, Lisp), a fixpoint primitive is unnecessary because a fixed
point combinator is trivially expressable by certain compositions of ordinary
terms. In contrast, in variants of the *simply-typed* lambda calculus, no such
compositions can be made which are well-typed. As such, in simply-typed calculi,
it is common practice to include a fixpoint primitive, to support recursion and
still preserve static typing. It should most certainly be noted, however, that
fancier typing disciplines, such as those with "recursive types", allow one to
compose fixed point combinators which *are* well-typed--these do not need a
fixpoint primitive. I chose to adopt the simply-typed discipline purely for it's
simplicity. I see no reason why the calculus could not be extended with
recursive types, and so obviate the need for a fixpoint primitive, if so desired.
A little review on pattern matching (feel free to skip):
Pattern abstraction is strictly a generalization of lambda abstraction. The term
"lambda x.T" can be understood as the construction of a new function, which
takes a single argument "x". When a term "U" is applied to this function, as in
"(lambda x.T) U)", the result is "T", such that all occurrences of "x" in "T"
are first substituted with the value of "U". Lambda abstraction is what Lisp uses.
In several modern functional languages, such as Haskell, pattern-matching is
used instead of lambda abstraction--even when you don't realize it. Lambda
abstraction is a strict subset of pattern-matching, where the "pattern" is
limited to terms of the form "x" (essentially, any term). The familiar
abstraction, "lambda x.T", is thus reimagined as "x -> T" (read: "at x use T").
The real fun of pattern matching, however, is when the pattern is more complex
than a single variable, allowing one to "deconstruct" the argument term. For
example, given term constants NIL, CONS and ADD, one can define a recursive
function for computing the length of a list as follows:
Fix LENGTH.NIL -> 0 | (CONS x xs) -> (ADD 1 (LENGTH xs))
Intuitively, if the input to this function is NIL, then the length of the list
is zero. Otherwise, the argument was a non-trivial list, so the second pattern
matches, in which case we recurse and add one to the result. This same sort of
logic is easily expressible in Lisp, and, indeed, the proper macros can yield a
similar degree of succinctness. But that's all old hat. I'm just briefly
explaining this so that it is clear to everyone that nothing strange or magical
(or silly) is going on with pattern-matching or lambda abstraction. That is,
they are essentially the same thing, except pattern-matching allows you to bind
more than one variable at a time, and restricts successful evaluation to only
the application of arguments of a given "form".
At this point, I can't help but pick some low-hanging fruit: Gary said, "It
would be quite something if you could match on a function application as you've
outlined in [EXPAND-M] since an application is not a terminal form." By
"terminal form", I believe Gary means "normal form" (are these synonyms?). When
a term is in normal form, that means that the reduction semantics of the
language cannot reduce it any further. For example, trivially, all constants are
in normal form (e.g., the number 5 wouldn't be expected to reduce to anything
but itself). Contrast this with "ADD 1 2", which one would expect to reduce to
"3". However, not all applicative terms ("ADD 1 2" is the application of [the
application of ADD to 1] to 2) reduce. For example, "CONS 5 NIL" does not reduce
further. And, clearly, as demonstrated in function LENGTH, one can match on
these sorts of terms. I don't think this is what Gary meant to say (I will
address what I believe to be his complaint far, far, below, however).
Gary's assertion that "the only thing that's actually new here are the pattern
extensions" is very much not true, and I apologize if I gave that impression.
Extensions are not my work, and they're not new. In fact, it is well-known that
the "proceed to next case on match failure" semantics is trivially realizable
with vanilla pattern abstraction, in either an untyped or recursively-typed
calculus. I chose to use extension rather than vanilla pattern abstraction for
the same reason I included the fixpoint primitive: I wanted to use the
simply-typed discipline with a minimum of fuss.
What *is* new, then? One thing, and one thing only: Matching on cases
(abstractions). Until now, pattern-matching semantics have limited the set of
valid patterns to terms consisting exclusively of variables, constants and
applications--no abstraction. So, for example, a term such as:
(F -> G) -> G
would not be valid, since the pattern "F -> G" is an abstraction. Why has
everyone made this restriction? The free variable problem. Suppose I applied the
above to the term:
(2 -> 5),
(x -> 5),
(x -> x),
where "x" is a variable over the *integers*. In all three instances, there would
be a match (e.g. "F -> G" matches "2 -> 3"). On a match, the variables in the
pattern would bind to the corresponding terms in the argument (e.g. "F" = "2";
"G" = "5"), and then be substituted into the result. Therefore, for the first
and second instances, the result would be "5". For the third instance, however,
the result would be "x". This term contains a free variable! This sort of
asymmetry occurs despite the fact that all three terms are closed and of the
same type ("int -> int"). How is the type system supposed to predict/prevent
this? That's what I contribute. We augment the variables, type system and
reduction semantics to account for binding/reference contexts for the matching
variables. It's fairly straightforward, so I imagine the reason no one has
tackled this problem yet is merely because it wasn't clear what the practical
use of solving it might be.
So, just to be perfectly clear: the only novelty I'm presenting is the ability
to match on cases. Extensions aren't mine, pattern-matching (obviously) isn't
mine, multi-stage computation (as in MetaML) isn't mine. Fixpoints are
irrelevant. Extensions are (beyond their pattern-matching functionality)
irrelevant. All that's really important is pattern-matching on cases and
multi-stage computation. More on this below:
In reference to my claim of being able to simulate/implement/subsume Lisp's
macro facilities with simpler machinery, Gary said: "In order for this to work,
you must add...the ability to pattern match on the structure/type of an
expression without first evaluating it...What I don't see is the mechanism by
which your language actually blocks this evaluation." I must again apologize for
being unclear--this time in my exposition of the key features of MetaML's
MetaML is an implementation of a multi-stage calculus. Normally, a term (a block
of code) can be thought of as being in stage 1 (or is it 0? It's not important).
When such a term is evaluated, the normal reduction rules apply. However, if we
preface this term with a backquote (as in Lisp) or tag it with some other
syntactic primitive (I think surrounding it with angle brackets looks pretty),
then the code is elevated to stage 2. Likewise, if we quote stage 2 code, we get
stage 3 code, and so on. Only stage 1 code is reduced (excusing antiquote).
Blocks of code can be reduced to a lower stage by prefacing them with a comma
(as in Lisp) or tagging it with some other syntactic primitive (I like prefixing
a tilde to a pair of surrounding parentheses, to represent antiquote). So, for
ADD 1 2
is in stage 1, has type "int", and reduces to "3". However,
<ADD 1 2>
is in stage 2, has type "code of int", and is in normal form. Similarly,
<<ADD 1 2>>
is in stage 3, has type "code of code of int", and is also in normal form.
Adding in antiquote,
<ADD 1 ~(SUB 5 3)>
is in stage 2, has type "code of int", and reduces to
<ADD 1 2>.
The antiquote mechanism (the tilde) reduces the subterm "SUB 5 3" to stage 1, of
type "int", upon which it reduces to "2" in the broader term.
Beyond the addition of type judgements, these semantics are essentially the same
as those of Lisp's backquote mechanism. Very straightforward.
So now, if you're still wondering how I "pattern match on the structure/type of
an expression without first evaluating it", let's look at an example. Let's try
matching "ADD 1 2" with the pattern "F X Y", without the argument reducing to
"3" and causing the match to fail:
(<F X Y> -> TRIVIAL) <ADD 1 2>.
As you can see, the match succeeds, and the result is TRIVIAL. But am I
"cheating", by quoting the argument? I don't think so. A conventional macro
system is nothing more than a two-stage evaluation mechanism (albeit usually
with dissimilar semantics between the two)--the program code starts in stage 2.
A functional program is essentially one big term, albeit perhaps with a great
number of nested "let" binders for the "separate" functions. Simply pop a quote
around it and pass it to the rewriting term. Worried it might still be quoted?
Look at this puppy:
<F> -> F
Bam. Not that you couldn't just have the righthand sides of the rewriting rules
be unquoted, in the first place.
You also said: "The macro system that you are describing must be applied
manually in your code to each P expression which is macro-transformable by
M...Moreover, it seems that your macros are less intelligible because they
combine multiple transformations into one definition, with the appropriate
transformation being selected by the shape of the input P to that macro."
I'm not really sure what you mean. Since we're talking about a "real" language,
allow me syntactic sugar for "let" binding, and let's define and bind functions
REDUCE and EXPAND-M. Then, Given program "P", and so-called macros M1, M2, ... ,
M[n], here is how we perform macro-expansion:
EXPAND-M M1 (EXPAND-M M2 ... (EXPAND-M M[n] <P>) ... )
If you want, we can construct a list of the macros, MACRO-LIST, and then reduce
the list onto P. Then we have:
(REDUCE EXPAND-M MACRO-LIST) <P>.
I don't see the problem...?
Also: "Even if I were to grant you the evaluation blocking mechanism...then you
have just expressed a static mechanism for replacing one expression with another
via structural rearrangement...more on the order of a C macro than a Lisp one.
In Lisp, I can use the entire language to write an arbitrary program (macro) to
perform code transformations, including lexical bindings, partial evaluation of
some inputs but not others (and functions of those evaluated results),
recursions, and so on."
As I hope is now clear, I *do* have "the entire language" at my disposable for
term-rewriting (whether you want to call it a "macro" or not is personal
preference). The argument term can be rearranged, substituted, evaluated,
partially evaluated, had arbitrary tests performed on it, recursed upon, had
recursion introduced to it, etc., etc. Obviously you can't do that in C. Name me
something that you can do in Lisp that the described system does not trivially
You also said: "[In a Lisp,] there are no arrows, dots, pipes, equals signs or
anything else in the language. When your [EXPAND-M] applications start
generating terms that look like: [CODE REMOVED]...the syntactic complexity is
sure to multiply very quickly. So again, I'm just not seeing your homoiconicity
here, except for the VERY high-level abstraction that "everything is a term."
Come on. Every term type has a different shape." I imagine you only wrote the
first part of this because you didn't understand the evaluation semantics at the
time. Hopefully it is clear now that each macro expansion would not balloon out
into the entire body of EXPAND-M. Rather, the result of the matching case would
replace the "expanded" term.
And as far as talking about homoiconicity, you're ignoring the difference
between the *presented syntax* and the actual syntax as far as defining the
*reduction semantics*. The reduction semantics are what it's all about. You
don't just have lists and atoms, as evidenced by the number of cases in eval
(each of those is a syntactic category, and a special "shape"). In McCarthy's
"Recursive Functions of Symbolic Expressions and Their Computation by Machine",
in defining S-expressions, he says: "We shall define five elementary functions
and predicates, and build from them by composition, conditional expressions, and
recursive definitions an extensive class of functions". This is a very large set
of primitive forms, with several different "shapes" (for example, "cons" takes
two arguments). Further, the axioms cannot all be lumped into a single syntactic
category (e.g. "constants" or "variables" or even "symbols"), because they each
have their own nontrivial reduction semantics. In contrast, I could have said,
for my calculus, "We shall define two elementary forms: constants and variables,
and build from them by application, extension and recursive definitions an
extensive class of functions." Much, much simpler. No "eval" parsing things from
lists to lists. Just terms evaluating to terms directly. Unlike the multiple
cases in Lisp's "eval", there is only *one* reduction rule in the pattern
calculus: beta reduction on application of a term to an extension. And I think
there's only one or two in the multi-stage bit, too.
And how hard is it for me to define CAR, CDR, EQ and COND in this calculus?
CAR : (CONS X XS) -> X
CDR : (CONS X XS) -> XS
EQ : X -> (X -> TRUE | FALSE) (this may be wrong...?)
COND: LHS -> RHS -> ELSE -> (LHS -> RHS -> ELSE)
This is all just *application* and *extension* with arbitrary constants. And
here is "eval", on a term "T":
<T> -> T,
if you're feeling fussy. I mean, seriously, which language provides a more
natural basis for the other? It would be massively easier to implement Lisp in
this calculus than to implement this calculus in Lisp.
I sincerely hope I'm not being a major bastard. You may notice I'm sending this
at 3:00 in the morning... My social skills aren't so hot when I'm this tired.
Let me know what remains unclear or glaringly, obviously wrong (seemingly).