On 5/1/19 9:45 AM, Ben Lippmeier wrote:
Check out:
A useful lambda-notation. Fairouz Kamareddine, Rob Nederpelt. Theoretical Computer Science 115 (1996) 85-109
They use “item notation”, and argue that maybe function application isn’t what we should be writing to begin with.
500+ pages of TaPL later, I can read this =) Their item notation goes a bit further than function application because it encompasses the typed lambda calculi: * Item notation has to handle inline function definitions like (lambda x. 2*x) y (apply the doubling function to "y") * Item notation needs to account for the type annotations in lambda abstractions, such as lambda x:T. f x (declare the argument "x" is of type "T") But, the main idea of item notation is simple: 1. Values, types, and kinds are left alone. 2. Type annotations are handled in a way that is irrelevant for my next few paragraphs. 3. The function application "f x" is translated to "(x delta)f" (These translations are actually performed recursively on terms, but the idea should be clear). The interesting one is #3, because in Dijkstra-dot notation we would write "f x" as "f.x", to mean "apply f to the argument x". The item notation, on the other hand, uses (x delta)f to mean, essentially, "feed x to the function f as an argument." They've used a delta instead of a dot (the dot is taken in the lambda calculus), but the idea is similar. If we were to reverse the Dijkstra-dot notation and write "x.f" to indicate the application of "f" to "x", then we recover the same idea. Doing so has some other benefits -- it makes diagrams easier to read, especially if you write (f;g) for the composition of g and f: x.(f;g) <===> feed x to f, then feed its result to g Older algebra books often adopt this convention modulo the dot, writing for example "xA" for the application of "A" to "x". (When these are vectors/matrices, you can explain away the heresy by defining R^n to consist of row vectors.) And in the presence of anonymous functions -- namely, lambda abstractions -- the item notation paper makes good arguments for this preference. In any case, parentheses are the worst possible choice, and I do find it interesting that the same ideas keep reappearing. Thanks for the reference.