Gary (and the Silent Others),
I also want to respond to your statement: "[In a Lisp,] there are no arrows,
dots, pipes, equals signs or anything else in the language."
You do realize that I am just describing the abstract syntax of a *calculus*,
right? The actual language implementation's syntax need not use the same symbols
at all. For example, rather than defining:
Terms T ::= C  V  T T  (T > T  T)  Fix T.T
I could just as easily define the syntax as:
Expressions E ::=
C
 V
 (E E)
 (at E E E)
 (fix E E)
This syntactic reformulation is purely aesthetic. Now, if you grant me syntactic
sugar for "let" binding and "fail" omission (not actually necessarysee far,
far below), as before, then we can write EXPANDM as:
let EXPANDM =
(at M
(fix EXPAND (M
(at ( F G) ( (EXPAND F) (EXPAND G))
(at (at F G) (at (EXPAND F) (EXPAND G))
(at (fix F G) (fix (EXPAND F) (EXPAND G))
(at F F))))))
(OOPS: In my earlier version of "EXPANDM", I didn't apply "M" in the right spot...)
So, there "are no arrows, dots, pipes, equals signs or anything else" in *this*
language, either. ***IMPORTANT***: Unlike a Lisp, this calculus does not
conflate concrete and abstract syntax. The parser reads in your source code
(abstract syntax), and then the compiler/interpreter processes the expression
tree in whatever internal representation (concrete syntax) makes the most sense
to the implementor. Concrete is not equal to abstract.
Now, if you're sharp, then at this point you might object: "Ha! That means you
can rewrite *terms*, certainly, but since the internal representation of those
terms is separate from their abstract syntax, you can't add new language
constructs!" Surprisingly enough, you would be wrong. What is the first form in
the term syntax? An arbitrary set of constants "C". Those aren't just for
showyou can apply them to terms, and then match and rewrite them as the
desired forms. As an example, rather than counting on syntactic sugar from the
parser, let's introduce a "let" construct natively:
constant LET : var('a) > 'a > 'b > 'b
Fix LETM.
( (LET X Y Z) > ((X > Z) Y)
 X > X)
The first line is just a type declaration, MLstyle, over universallyquantified
type variables 'a and 'b. What's with the "var" nonsense? I've augmented the
type system to type free variables as something other than the type of their
bound value (that is, if I have a variable "X", which only binds to integers,
its type is not "int"rather, it is "var(int)").
Now, I can just do the old "EXPANDM LETM P" trick and all occurrences of "LET
X Y Z" (read: "Let X = Y in Z") are transformed as I'd like them to be. For
example, suppose I have the trivial program P:
(LET X 5 (ADD X 2))
and I evaluate:
(EXPANDM LETM P)
EXPANDM deconstructs P and recursively applies LETM to each of its subterms.
Those which fail LETM's first case are left alone, since its second case is the
identity: "X > X". In fact, the only term which succeeds is the outermost term,
which matches the pattern "(LET X Y Z)", yielding the result:
((X > Z) Y)
But the above variables were just bound to the matching terms in P, so
substitution gives:
((X > (ADD X 2)) 5)
which reduces to:
(ADD 5 2)
and then to:
7
Come to think about it, it's actually kind of silly that I just took all of this
time to demonstrate how easy it is to add new constructs, since I've already
given a definition for the crownjewel of language constructsmacro
expansionas EXPANDM.
Sexy, no?
Best,
Andrew
P.S. Have you ever seen someone overuse colons as much as I have been?!!
