Implicit mapping

The last post was about what happens when one tries to apply a function to a value that is too small (not wrapped in an applicative functor). This post is about what happens when the value is too big (wrapped in too many functors). Jakub Marian defines (when translated into my notation):
$$\begin{aligned} (f\ g)\ x &{}= f\ (g\ x) \\ f\ A &{}= \{f\ x : x\in A\} \end{aligned}$$ I posted the applicative function definition in the last post, but here we only need a regular functor. As far as I understand it, a functor is what comes directly from category theory, and an applicative functor just adds some functions that they nearly always have. There are very few functors that cannot be made into applicative functors.

$\newcommand{\fmap}{\text{fmap}}$A functor $f$ provides us with just:
$$\fmap : (a\rightarrow b)\rightarrow f\ a\rightarrow f\ b$$ For sets, $\fmap$ applies a function to every element of the set (eliminating duplicates afterwards), and for functions, it composes the given function (type $(a\rightarrow b)$) to the left of the functor's function (type $f\ a$, which is $t\rightarrow a$). I encourage you to see why the types work for the latter example.

$\newcommand{\neg}{\text{neg}} \newcommand{\R}{\mathbb R}$So, post done? Pretty much. It's maybe worth going through the example of $\neg\ {}_\cdot^{\neg\ 1}D$, where $\neg : \R\rightarrow\R$ is the negation function and $D : (\R\rightarrow\R)\rightarrow \R\rightarrow\R$ is the differentiation function (and the superscript-subscript notation is described in the initial post). Of course, limiting to real numbers is arbitrary; I just needed a number type.

Firstly, we try to apply $\neg : \R\rightarrow\R$ to ${}_\cdot^{\neg\ 1} : \R\rightarrow\R$. $\R\rightarrow\R$ doesn't match $\R$, but it does match $f\ \R$, where $f = (a\rightarrow)$. So, we transform $\neg\ {}_\cdot^{\neg\ 1}$ into $\fmap\ \neg\ {}_\cdot^{\neg\ 1}$, which is $\neg\circ{}_\cdot^{\neg\ 1}$, the negative reciprocal function. Let's call it $\text{negrec} : \R\rightarrow\R$.

Next, we try to apply that to $D : (\R\rightarrow\R)\rightarrow \R\rightarrow\R$. $D$'s type certainly doesn't match the expected $\R$, but it does match $h\ (g\ \R)$, where $g = (b\rightarrow)$ (where $b = \R$) and $h = (c\rightarrow)$ (where $c = \R\rightarrow\R$). Note that it doesn't match $i\ \R$ where $i = ((\R\rightarrow\R)\rightarrow\R\rightarrow)$ because $\rightarrow$ is not associative (it binds to the right). So, $\text{negrec}\ D$ becomes $\fmap\ (\fmap\ \text{negrec})\ D$, or $(\text{negrec}\circ{})\circ D$.

That's as far as we can go, so let's apply this function to, say, $\exp$ and $0$. $$\begin{aligned} ((\text{negrec}\circ{})\circ D)\ \exp\ 0 &{}= ((\text{negrec}\circ{})\ (D\ \exp))\ 0 \\ &{}= (\text{negrec}\circ\exp)\ 0 \\ &{}= \text{negrec}\ (\exp 0) \\ &{}= \text{negrec}\ 1 \\ &{}= \neg\ 1 \end{aligned}$$ And that tells us that the gradient of the normal to the exponential curve at 0 is negative 1.