I thought it was more of an accident? The story I know goes that Church used hats over variables, and then he switched over to lambda prefixes for ease of printing.
I have often thought that if I were to teach a class on functional programming, I would use JavaScript’s fat arrow notation to introduce lambda calculus. Less succinct with all the extra parentheses that occur in function calls but I think it’s easy enough to explain.
Pretty much the same idea, but in math contexts I tend to use the \mapsto arrow (↦), since mathematicians are more familiar with this than lambda calculus. (The fat arrow seems like an interesting alternative in programming contexts, but I worry that it might be confused with implication.)
The function that swaps the arguments to a two-argument function:
f ↦ ((x, y) ↦ f(y, x))
Interesting. The mathematical notation I learned in school was: f:x↦2x+3, So I guess this would translate to f:(x,y)↦(y,x).
Alternatively, the f(x,y) = (y,x) notation would work (sort of, you tend to explicitly write out the base vector 𝑒ₖ for both notations: f(x,y) = f(x𝑒₁+y𝑒₂) = y𝑒₁+x𝑒₂ )
That's close but not quite how I meant for the notation to be interpreted: f is an argument to an anonymous function. Maybe clearer is
swap = f ↦ ((x, y) ↦ f(y, x))
The rule this satisfies is
swap(f)(x, y) = f(y, x)
and the type for swap is
swap : (X × Y → Z) → (Y × X → Z)
for some types/sets X, Y, and Z.
(Also, note that tuples might not be anything like a vector space. For example, for String × [Int], you wouldn't usually write ("hi", [2,3]) as "hi"𝑒₁ + [2,3]𝑒₂ since there's not really a good commutative addition operation for strings or lists.)
