There are two different ways of reading Scott’s kickoff of the type signature, though.
You took it in the direction of a term j:A→B is a sort of belief about how actions turn into outcomes.
But it’s plausible to me that Scott meant “the item j from A→B is actually the underlying reality”. The idea there would be that (A→B)→A isn’t a comment that directly concerns the implementation, but it’s a philosophical statement about embedded agency. Items j needn’t be models, they could be the actual configurations of reality; agents are these terms that we can, either through proper prediction or post-hoc explanation, understand as turning physical configurations of causal arrows from actions to the world into actions. Like, it’s a thing we observe them doing. Then to implement a (A→B)→A you would need a whole bunch of machinery including subjective epistemic rationality j′ (which might look a little like A→ΔB) which one would hope converges on the actual j with learning, of course utility so you know what you want to do with the second → in the signature. But the real-world implementation’s type signature would be a bit more intricate than the philosophy’s type signature.
I know philosophers of science probably duel-at-dawn about the idea that you can give a type signature to underlying reality (“physical configuration of causal arrows”) rather than to a subjective model of it.
(I have a post about all this coming out soon, will edit this comment with a link to it)
EDIT: the post is out
There are two different ways of reading Scott’s kickoff of the type signature, though.
You took it in the direction of a term j:A→B is a sort of belief about how actions turn into outcomes.
But it’s plausible to me that Scott meant “the item j from A→B is actually the underlying reality”. The idea there would be that (A→B)→A isn’t a comment that directly concerns the implementation, but it’s a philosophical statement about embedded agency. Items j needn’t be models, they could be the actual configurations of reality; agents are these terms that we can, either through proper prediction or post-hoc explanation, understand as turning physical configurations of causal arrows from actions to the world into actions. Like, it’s a thing we observe them doing. Then to implement a (A→B)→A you would need a whole bunch of machinery including subjective epistemic rationality j′ (which might look a little like A→ΔB) which one would hope converges on the actual j with learning, of course utility so you know what you want to do with the second → in the signature. But the real-world implementation’s type signature would be a bit more intricate than the philosophy’s type signature.
I know philosophers of science probably duel-at-dawn about the idea that you can give a type signature to underlying reality (“physical configuration of causal arrows”) rather than to a subjective model of it.
(I have a post about all this coming out soon, will edit this comment with a link to it) EDIT: the post is out