[Haskell-cafe] Looking for a paper

[Michael Orlitzky]

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.