I heard it evolved from Bertrand Russell, who used a notation such as \hat{x}.(x+1) to mean similar in Principia Mathematica. Church and maybe others in the logic community originally used the same notation but Church's publisher, not having latex, was unable to print it. So they wanted to move the hat in front of the letter, such as ^x.(x+1). The hat symbol either wasn't available or the instruction got mangled during production into the similar-looking lambda.
One benefit could be to emphasize the distinction between regular mathematical functions (e.g. x ↦ x+1) and λ-terms (e.g. λx. x+1): strictly speaking, those are different kind of objects.
Not much, but you immediately know it's a function (abstraction).
Besides, the standard notation for the "arrow function" is maplet (x ↦ x + 1) in mathematics. I assume λ notation sees frequent uses in logic and computation theory.
The characters in OP's arrow function have the benefit of being available on a standard keyboard layout. This has proven to be an important syntactic feature, imo.
> Extensionality fails in most dependent type theories
Is this a reason to use Isabelle?
I remember Bob Harper being interested in dependent typing. What is his take on extensionality?
> (according to one rumour, because Dana Scott was fond of curry)
I always assumed it was related to Haskell Curry, the logician.
That's because it is
She was fond of curry as well.
Dana Stewart Scott is a he, if I'm not mistaken.
What is the benefitsof the lambda notation over a more intuitive arrow notation like x->x+1?
I heard it evolved from Bertrand Russell, who used a notation such as \hat{x}.(x+1) to mean similar in Principia Mathematica. Church and maybe others in the logic community originally used the same notation but Church's publisher, not having latex, was unable to print it. So they wanted to move the hat in front of the letter, such as ^x.(x+1). The hat symbol either wasn't available or the instruction got mangled during production into the similar-looking lambda.
One benefit could be to emphasize the distinction between regular mathematical functions (e.g. x ↦ x+1) and λ-terms (e.g. λx. x+1): strictly speaking, those are different kind of objects.
Different how?
What about expressing something a bit more complex like: λf. (λx. f (x x))(λx. f (x x))
Not much, but you immediately know it's a function (abstraction).
Besides, the standard notation for the "arrow function" is maplet (x ↦ x + 1) in mathematics. I assume λ notation sees frequent uses in logic and computation theory.
The characters in OP's arrow function have the benefit of being available on a standard keyboard layout. This has proven to be an important syntactic feature, imo.
Haskell uses a single backslash \ in place of λ