Lambda the Ultimate

I'm not sure this is LtU grade material

There is a lot more to the question than what appears on the surface, as I hope the ensuing discussion has revealed. Some of the fundamental questions are:

• What is the difference between function application, function evaluation, function execution, and function calling?
• What specifically is a quotation (e.g. "[1 +]" in Joy, and what is the type of the value it leaves on the stack?
• Are stack-language functions simply functions between stacks or are they functions that take arguments from the top of the stack and push results onto the stack? Is there a difference?
• What is the significance of the difference between: "3 1 [+] i" and "3 1 +"?
• Does the "i" in "3 1 [+] i" operate the "+" or on a function that is equivalent to "+"? Are there any significant differences?
• What does whitespace (or more precisely the juxtaposition of terms) mean in languages like Joy and Cat as opposed to ML or Haskell?

There really is nothing wrong with apply. It really has to do with what language we are used to using to describe what is going on in our heads.

I think about "function evaluation", James apparently thinks about "function calls", and you apparent think about "function application". It really is just different ways of naming the same thing.

I am really thinking that adding a letter (going from eval to apply), and gaining clarity for a larger audience is well worth the trade-off.

...at least not from a PL semantics perspective. From that perspective, if the question is whether "apply" is a more appropriate choice than "eval" in this case, I'd say yes.

In the traditional functional language semantic model, eval and apply are two distinct operations in the metalanguage (see e.g. SICP for the classic approach). 'Eval' takes an expression as input, represented as abstract syntax. When it encounters an expression that looks like an application, it invokes 'apply'. 'Apply' takes a function and a list of arguments, and applies the former to the latter. The operations of the same name that are exposed in the object language have equivalent behavior, at least in the case of e.g. Scheme. (Although in Scheme, there's a single generic "apply" function, whereas the metalanguage may also have an apply function for each type of applicable value, e.g. a different function for lambdas and primitives.)

In Joy at least, the "i" operator doesn't really behave like "eval". I would expect the equivalent of "eval" in Joy to be an operation which can consume any kind of stack, and evaluate it. Joy's dot operator (".") seems to fit this bill. The "i" operator, however, can only accept a stack which has a quotation on top. If you consider a quotation the rough equivalent of a lambda, then "i" is the closest equivalent of the "apply" operation, at least for quotations. This would be the rough equivalent of an "apply-closure" function in Scheme (which in Scheme, would normally only exist at the metalanguage level).

(BTW, tangentially I'd like to observe that this conclusion depends on type analysis, and is a minor example of why type systems are important to PL semantics.)

The i<->apply comparison isn't perfect, though, because in Joy "i" simply pushes the elements of a quotation individually onto the stack, which is similar to a traditional "apply" in some ways, but not others. For example, in a Joy program such as 1 [2 3] i 4 + + +, do you still consider the "i" to be "applying" something? I don't doubt that you can provide an interpretation in which that makes sense, but there are also others in which it doesn't.

[Edit: an additional observation about the type-specificity of "apply": in Joy, you can't use "i" on a primitive, or even on a named, user-defined function (even though such a function could well be implemented internally as a quotation). So to be specific, the name you want should really be something like "apply-quotation". I realize that's probably too long, but I'm mentioning it for the sake of preciseness.

Edit++: if you're looking for an abbreviation, "appq" could work. Hey, "setq" worked for Lisp...]

In the traditional functional language semantic model, eval and apply are two distinct operations in the metalanguage

Good point.

(BTW, tangentially I'd like to observe that this conclusion depends on type analysis, and is a minor example of why type systems are important to PL semantics.)

I agree. The type of what has been called "eval" in Cat (and now am very convinced that it should be "apply") is:

('A ('A -> 'B) -> 'B)

Where 'A and 'B are stack variables.

because in Joy "i" simply pushes the elements of a quotation individually onto the stack

That doesn't sound quite right. I would have said that "2 3 [+] i" applies the function + (which is a function on stacks) to a stack containing 2 3 on the top. To create a new stack containing 5 on the top.

I appreciate your insights into the issue.

because in Joy "i" simply pushes the elements of a quotation individually onto the stack

That doesn't sound quite right. I would have said that "2 3 [+] i" applies the function + (which is a function on stacks) to a stack containing 2 3 on the top. To create a new stack containing 5 on the top.

Sorry, I should have mentioned that my description was based on the rewriting system described here. The rewrite rule for the i combinator is as follows, where P is any program:

[P]  i  =>  P.

The rewriting system is somewhat agnostic about reduction strategy (see "The role of the stack" at the above link). But the above rule implies that "2 3 [+] i" can be considered equivalent to "2 3 +". This is what I meant by "pushes the elements of a quotation individually onto the stack". Similarly, "2 3 [4 5 +] i" is equivalent to "2 3 4 5 +".

This means that it's possible to define a semantics and/or implement an interpreter for Joy in which the i combinator doesn't itself perform an "apply" operation. This is what I was referring to when I wrote "there are also others in which it doesn't" (i.e. other interpretations in which "i" doesn't "apply").

[Edit: to summarize, I don't think 'apply' is a bad choice of name, it's just that from another perspective it could be called something like 'unquote'. Also, from either perspective, this "apply" operation only operates on quotations, not on primitives or other literals. This is worth keeping in mind when comparing to the more generic "apply" in languages like Scheme or Lisp.]

Sorry, I should have mentioned that my description was based on the rewriting system described here.

You may be interested to know that I have implemented that particular rewriting system as a macro language extension to Cat. I also use a variant of the term rewriting language to define the semantics for many of the Cat primitives. The term rewriting system turns out to be very interesting for optimization.

This is what I meant by "pushes the elements of a quotation individually onto the stack". Similarly, "2 3 [4 5 +] i" is equivalent to "2 3 4 5 +".

Yes but simply writing "+" isn't pushing anything on to the stack (well except the result of adding the top two values).

Your point about "unquote" is a good one. Function application can be described as a process of "dequoting" or "unquoting".

to define a semantics and/or implement an interpreter for Joy in which the i combinator doesn't itself perform an "apply" operation.

But how else could we describe the reduction step of the rewriting system? If we drop the terminology of quoting for a second, which I feel perhaps muddies the waters, then a quotation is really just a function. If we stop saying "quote" and "dequote", we are left with something like: "make function" and "apply function". Which just goes to support the terminology choice of "apply".

The following is an interesting fact about "quoting" and "dequoting": I have another operation called "qv" which creates a quotation from a value. The following MetaCat macro shows the rewriting result:

  macro { qv eval } => { }

But it all would probably be much better off if I use the names:

  macro { quote apply } => { }

By the way Anton, I really appreciate your feedback, and I have finally heeded your advice from an older post regarding Cat and posted the core operational semantics online: http://www.cat-language.com/manual.html.

I've used the core language, called the Level-0 specification, to define a large set of primitives for a pure subset of Cat, called the level-1 specification, which is described at: http://www.cat-language.com/primitives.html.

Yes but simply writing "+" isn't pushing anything on to the stack (well except the result of adding the top two values).

What I wrote was ambiguous, but what I had in mind was that the "+" within a quotation would be an identifier (a Joy program term), whereas the "+" appearing directly on the stack would represent the primitive + function, as a value. I believe that a correct semantics for Joy could be defined this way, although it may not be a typical one.

But how else could we describe the reduction step of the rewriting system?

In eval/apply terms, eval would invoke the rule for "i", which would turn the quotation (consisting of terms) into values on the stack, including primitive functional values. The resulting stack would be returned to eval, which would attempt to evaluate the stack, notice the + primitive on top, and invoke apply-primitive. And so on.

I played around with this a few years ago because I was interested in the relationship between lambda and Joy's quotations. I don't entirely agree that the quotation terminology muddies the waters, but the perspective on this is affected by which semantic approach you take.

I preferred the quotation approach because defining the semantics directly in terms of functions somewhat begs the question of the relationship between quotation and lambda. In the approach I took, the only true functions are primitives; literals are just ordinary values, not functions; quotations are just lists of terms, and "i" just pushes the corresponding values onto the stack. It's quite simple, and does away with the whole idea of user-defined functions. :)

I'm really glad to hear about your semantics, I'll definitely check it out (although probably not for a week or so).

I preferred the quotation approach because defining the semantics directly in terms of functions somewhat begs the question of the relationship between quotation and lambda.

That's an interesting question. Is a quotation simply a lambda expression without arguments?

In the approach I took, the only true functions are primitives; literals are just ordinary values, not functions; quotations are just lists of terms, and "i" just pushes the corresponding values onto the stack. It's quite simple, and does away with the whole idea of user-defined functions. :)

So you are creating a separate semantic category of terms to distinguish between values and functions? How does it do away with user-defined functions, and why do you want to?

I am not convinved is that a stack is an important or meaningful part of the semantics of Joy or Cat. Consider the following concatenative language defined entirely in terms of MetaCat rewriting rules:

macro { 0 iszero } => { true }
macro { $a succ iszero } => { false } 
macro { true [$A] [$B] if } => { $A }
macro { false [$A] [$B] if } => { $B }
macro { $a succ pred } => { $a }
macro { $a quote } => { [$a] }
macro { $a [$B] dip } => { $B $a }
macro { $a dup } => { $a $a }
macro { $a pop } => { }

This is actually almost the core of the Cat language (minus lists).

Other rules follow naturally from the above set:

macro { apply } => { true swap dup if }
macro { swap } => { quote dip } 
macro { bury } => { swap [swap] dip }
...

Simply applying these rules to an expression until no more reductions are possible will result in a computation.

I suspect this is similar to your approach?

Is a quotation simply a lambda expression without arguments?

Not just without (named) arguments, but also without an enclosing lexical environment. And with an implicitly available set of arguments on the stack. But I'm suggesting that it's overkill to explain quotations in terms of lambda.

So you are creating a separate semantic category of terms to distinguish between values and functions?

I'm using "term" in the usual way, as a syntactic element which denotes a value. The syntactic element "+" is an identifier, i.e. a kind of term, which in my approach denotes a primitive functional value which can be pushed onto the stack.

How does it do away with user-defined functions, and why do you want to?

It says that quotations are simply lists, nothing more. Turning the question around, rhetorically, why would you want to call a simple list a "function"? That's an interpretation which assumes a particular use of the list, and that the list contents follow certain rules. It's more like an idiom than a semantic feature.

Of course, I do understand the usefulness of thinking about quotations as functions, but I also think it can obscure the simplicity of the language. I wanted to examine the semantics of programs which are constructed using only literals, lists, and some primitives, without complicating the description unnecessarily.

I am not convinced that a stack is an important or meaningful part of the semantics of Joy or Cat.

Von Thun made a similar point in the section about "The role of the stack" in the rewriting system paper, which I mentioned earlier. Basically, the stack can be treated as an optimization which is useful during evaluation.

But I think there's more to it. You see something similar in the lambda calculus: you can evaluate lambda expressions using pure term rewriting, but you can also use a stack during evaluation to optimize substitution.

There's an obvious connection between term rewriting systems and stacks. When you rewrite a subexpression, the subexpression is replaced with a result. This introduces stack-like behavior in any system that involves recursive rewriting. This stack-like behavior inevitably enters into the programmer's reasoning process. In the LC, reasoning about "call stacks" or the equivalent (i.e. what function was applied/called from where) tends to be necessary. In Joy/Cat, reasoning about stacks of arguments and intermediate values is similarly unavoidable, whether or not you consider these as term rewriting systems. When considered as term rewriting systems, the stack can be considered an emergent property.

I suspect this is similar to your approach?

My approach still uses an explicit stack, which the pure term-rewriting approach can avoid. However, if you implemented the rule for "i" given earlier, then quotations would simply be replaced in the program by their contents, which is similar to how my approach pushes the elements of a quotation onto the stack.

The core Cat language doesn't have side effects, but the level-2 specification and above does. That is essentially Cat with ad-hoc polymophism and exceptions added. I just updated the manual if you want to read more.

I am now 100% convinced that "apply" is the right term to use, but I'm a little disheartened because I have a heck of a lot of code and documentaton to change.