Typed Lambda-Terms are a nice thing which produces readable and comparably short terms. Computer Scientists and Logicians know this and therefore use them. Not so for the rest of Mathematics. Still, in Analysis, I mostly see notions like
. As a typed Lambda-Term, one could just write
, or just
(since the image-type is clear anyway). In this case, of course, its neither shorter nor clearer than the notation before.
But in one recent lecture I took we were talking about curves which are homotopic to the one-pointed curve. The one-pointed curve for a Point A had to be defined by
, which is syntactically wrong because universal quantifiers have to be written in front of the expression they quantify, but at least purely syntactical - there are people who really write "for all" every time. In Lamda-Notation, this would just have been
with full type-annotations, but in fact we can omit these and just write
, even further, we can just use
instead of naming this function. When handling with a lot of functions that are not needed often, inlining can be a very nice utility.
Well, one has to get used to this type of Notation. And one may argue why writing
(the main reason could be that lambda notation is already widespread). But I think it would make huge parts of Analysis (and Linear Algebra) much more enjoyable.