(A → B) → A

This post is about fol­low­ing type sig­na­ture, which I call the type of agency: . You can also think of it as con­sequen­tial­ism or do­ing things on pur­pose. This post will be a rant with a bunch of ran­dom thoughts re­lated to this type sig­na­ture, and it will likely not make sense. It will also be sloppy and will have type er­rors, but I think it is worth post­ing any­way.

First, in­ter­pret these ar­rows as causal ar­rows, but you can also think of them as func­tion ar­rows. This is say­ing that the causal re­la­tion­ship from to causes to hap­pen. Think of as an ac­tion and as the goal. The reason that hap­pens is the fact that it has as a con­sequence. There are not nor­mally ex­po­nen­tial ob­jects 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 cat­egory with nodes that are the nodes in your Bayes net, and add small num­ber of morph­isms from product nodes to in­di­vidual nodes, cor­res­pond­ing to the func­tions in the Bayes’ net. The acyc­lic­ness of the Bayes’ net roughly cor­res­ponds to this cat­egory be­ing thin. Then you can con­sider hav­ing other types of morph­isms that can keep the cat­egory thin.)

If you have a game between two agents with ac­tion nodes and , with util­it­ies and . The game im­ple­ments a pair of func­tions and . We can Curry these func­tions and think of them as and . Bringing in the agency of both play­ers leads to cycle. This cycle does not make sense un­less the agency ar­rows are lossy in some way, so as to not be able to cre­ate a con­tra­dic­tion.

For­tunately, there is an­other reason to think that these agency ar­rows will be lossy. Lawvere’s Fixed Point The­orem says that in a Cartesian closed cat­egory, un­less has the fixed point prop­erty, you can­not have a sur­ject­ive func­tion , in Set this is say­ing that if has more than one ele­ment, you can­not have an in­jec­tion . i.e. The agency ar­rows have to be lossy.

Also, no­tice that Argmax, takes in a func­tion from some set to , and re­turns an ele­ment of the do­main, , so Argmax has type .

This one is a bit more of a stretch, but if you look at gradi­ent des­cent, you have some space , you have a func­tion . The gradi­ent can be thought of as a func­tion from in­fin­ites­imal changes in to in­fin­ites­imal changes in . Gradi­ent des­cent works by con­vert­ing this gradi­ent into a change in . i.e. Gradi­ent des­cent looks kind of like .