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
![f:U\rightarrow\mathbb{C},f(x)=x^2](/latex?n=f2ada3c24d8314ef4e9f3e1e3768b5910e9ea6ecb18a10ea1b11bbbc263eeb70)
. As a typed Lambda-Term, one could just write
![f=(\lambda x^U.x^2)^{U\rightarrow\mathbb{C}}](/latex?n=48ff469646de539fa6f05d18e55b736c8db30fe99a649558fc22772ec47ba69d)
, or just
![f=\lambda x^U.x^2](/latex?n=51d442087d3939c62d9e095942d8569d372cc5adad9d5e8a2e52c2a137d6cb91)
(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
![f:]0;1[\rightarrow\mathbb{C},f(x)=A\forall x\in]0;1[](/latex?n=591f216dac73f0ccd62fc57d50aacdbd2aa23ffeabd4abe533d54797ee573114)
, 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
![f=(\lambda x^{]0;1[}.A)^{]0;1[\rightarrow\mathbb{C}}](/latex?n=f29fab8689f91203842bcd003fba390f4d03786b6ba35d7154a167f7d1cd2e28)
with full type-annotations, but in fact we can omit these and just write
![f=\lambda x.A](/latex?n=b0e73148f9e7c41623cfe1bb7139520054fb08a4a36cb9a1451e3a8eb6bed454)
, even further, we can just use
![\lambda x.A](/latex?n=5fef4f58d63311e1b33f784dfccb977ba85679246134f19734e371f600aa3b76)
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
![\lambda x.A](/latex?n=5fef4f58d63311e1b33f784dfccb977ba85679246134f19734e371f600aa3b76)
instead of
![x\rightarrow A](/latex?n=fa5731a84d3fe9ac6b1211031584e4149babd55d9e54c1a8ca13fcf373c80ad3)
(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.