(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­se­quen­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 rea­son that hap­pens is the fact that it has as a con­se­quence. There are not nor­mally ex­po­nen­tial ob­jects like this in Bayes’ nets, but I think you can mod­ify so that it makes sense. (I’m not sure that this works, but you have a Carte­sian closed cat­e­gory with nodes that are the nodes in your Bayes net, and add small num­ber of mor­phisms from product nodes to in­di­vi­d­ual nodes, cor­re­spond­ing to the func­tions in the Bayes’ net. The acyclic­ness of the Bayes’ net roughly cor­re­sponds to this cat­e­gory be­ing thin. Then you can con­sider hav­ing other types of mor­phisms that can keep the cat­e­gory thin.)

If you have a game be­tween two agents with ac­tion nodes and , with util­ities and . The game im­ple­ments a pair of func­tions and . We can Curry these func­tions and think of them as and . Bring­ing in the agency of both play­ers leads to cy­cle. This cy­cle 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­tu­nately, there is an­other rea­son to think that these agency ar­rows will be lossy. Law­vere’s Fixed Point The­o­rem says that in a Carte­sian closed cat­e­gory, un­less has the fixed point prop­erty, you can­not have a sur­jec­tive func­tion , in Set this is say­ing that if has more than one el­e­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 el­e­ment of the do­main, , so Argmax has type .

This one is a bit more of a stretch, but if you look at gra­di­ent de­scent, you have some space , you have a func­tion . The gra­di­ent can be thought of as a func­tion from in­finites­i­mal changes in to in­finites­i­mal changes in . Gra­di­ent de­scent works by con­vert­ing this gra­di­ent into a change in . i.e. Gra­di­ent de­scent looks kind of like .