(A → B) → A

[Scott Garrabrant]

This post is about following type signature, which I call the type of agency: $(A\to B)\to A$. You can also think of it as consequentialism or doing things on purpose. This post will be a rant with a bunch of random thoughts related to this type signature, and it will likely not make sense. It will also be sloppy and will have type errors, but I think it is worth posting anyway.

First, interpret these arrows as causal arrows, but you can also think of them as function arrows. This is saying that the causal relationship from $A$ to $B$ causes $A$ to happen. Think of $A$ as an action and $B$ as the goal. The reason that $A$ happens is the fact that it has $B$ as a consequence. There are not normally exponential objects like this in Bayes’ nets, but I think you can modify so that it makes sense. (I’m not sure that this works, but you have a Cartesian closed category with nodes that are the nodes in your Bayes net, and add small number of morphisms from product nodes to individual nodes, corresponding to the functions in the Bayes’ net. The acyclicness of the Bayes’ net roughly corresponds to this category being thin. Then you can consider having other types of morphisms that can keep the category thin.)

If you have a game between two agents with action nodes $A_1$ and $A_2$, with utilities $U_1$ and $U_2$. The game implements a pair of functions $A_1\times A_2\to U_1$ and $A_1\times A_2\to U_2$. We can Curry these functions and think of them as $A_2\to (A_1\to U_1)$ and $A_1\to (A_2\to U_2)$. Bringing in the agency $(A_i\to U_i)\to A_i$ of both players leads to cycle. This cycle does not make sense unless the agency arrows are lossy in some way, so as to not be able to create a contradiction.

Fortunately, there is another reason to think that these agency arrows will be lossy. Lawvere’s Fixed Point Theorem says that in a Cartesian closed category, unless $B$ has the fixed point property, you cannot have a surjective function $A\to (A\to B)$, in Set this is saying that if $B$ has more than one element, you cannot have an injection $(A\to B)\to A$. i.e. The agency arrows have to be lossy.

Also, notice that Argmax, takes in a function $f$ from some set $A$ to $R$, and returns an element of the domain, $A$, so Argmax has type $(A\to R)\to A$.

This one is a bit more of a stretch, but if you look at gradient descent, you have some space $X$, you have a function $f:X\to R$. The gradient can be thought of as a function from infinitesimal changes in $X$ to infinitesimal changes in $f\left(X\right)$. Gradient descent works by converting this gradient into a change in $X$. i.e. Gradient descent looks kind of like $(\partial X\to \partial R)\to \partial X$.