Lambda calculus and differential geometry

You can perfectly demonstrate the essence of currying in almost any modern language, but there are some phenomena that are only revealed to programmers who program in ML/Lisp languages. I want to say something about that.

Take for example map function in Haskell. Its type is (a - > b) -> ([a] -> [b]) (often written as (a - > b) -> [a] -> [b]). This type can be interpreted in two different ways:

• function map takes a function and a list and gives us a list. This is probably the first interpretation that the majority of programmers have in mind when see a type like this.
• function map takes a function and gives us a new function (between lists). In other words, map lifts functions to the level of list types.

Someone would maybe even argue that there is no difference here: the type of the map is (a - > b) -> ([a] -> [b]) and it is clear what it represents. But I think that we all automatically look at curried functions as functions of multiple arguments, and often miss this subtlety.

Operator <*> :: f (a -> b) -> f a -> f b is another nice example. You can see it as a function application in the context of applicative functors: it takes function and value both wrapped in applicative f, and it returns a new value wrapped in f. But we can also understand it as a transformation of functions wrapped in f: it unwraps a -> b from f and give us f a -> f b. It is almost like the distributive law of f over ->:

$$ \mathtt {f (a \rightarrow b) \Rightarrow f a \rightarrow f b}$$

Another example

In differential geometry, at every point $\mathbf p$ of a surface (or generally a manifold), there is a tangential plane $T_{\mathbf p}$ that consists of tangential vectors. In order to measure things on s surface, you need a metric $g$. This object is a generalization of dot products: for each point $\mathbf p$, metric $g_{\mathbf p}$ it takes two vectors $X_{\mathbf p}, Y_{\mathbf p}$ form $T_{\mathbf p}$ and gives a real number denoted by $g_{\mathbf p}\left(X_{\mathbf p}, Y_{\mathbf p}\right)$ (you can think about it like $g_{\mathbf p}\left(X_{\mathbf p}, Y_{\mathbf p}\right) = \left\langle X_{\mathbf p}, Y_{\mathbf p} \right\rangle$ ). Therefore the type of $g_{\mathbf p}$ is $$T_{\mathbf p} \times T_{\mathbf p} \rightarrow \mathbb R.$$

Among many other (more useful) things, $g$ can be used to transform vectors into covectors. Covector is a linear function that takes a vector and spits out a real number. Therefore covector is a function of type $T_{\mathbf p} \rightarrow \mathbb R$. The space of all covectors at point $\mathbf p$ is denoted by $T_{\mathbf p}^{*}$.

You maybe already see how $g_{\mathbf p}$ transforms vectors into covectors. Take vector $X_{\mathbf p}$ and partially apply it to the $g_{\mathbf p}$. This gives us function $$y \mapsto g_{\mathbf p}\left(X_{\mathbf p}, y\right) \colon T_{\mathbf p} \rightarrow \mathbb R,$$ which is of course a covector. But this means that $g_{\mathbf p}$ could be understood as function of type $T_{\mathbf p} \rightarrow T_{\mathbf p}^*$: it takes vectors and gives covectors.

Again, the same function can be interpreted in two ways.

What is my point here?

There are often multiple ways you can understand the type of a function. This phenomenon is present in many areas of math (I choose the example from geometry because I noticed it yesterday), and also we can see glimpses of it in programming.

Currying is generally well understood among programmers (even if they write Javascript, Python, Go,…), but can hide the thing that I am talking here about. Once we learn and master currying, we lose the ability to think differently. Type like A -> B -> C becomes for us just (A, B) -> C, even if the former one can give us a different and more interesting perspective.

P.S. Example from geometry is half of a story called the musical isomorphism.

P.P.S. The irony here is that function map lifts functions, while metrics $g$ flats vectors.