It’s the monad arising from the currying adjunction between and attaches an environment to :
This is the type of a function that takes a state of type and outputs a result of type and a new state of type . So is the ability to depend on state and is the ability to change the state.
The natural transformation is evaluation:
takes a function and an input point and evaluates the function at that point. So we get
by evaluating the in the middle, while the unit
is just the curried identity on pairs:
I had an idea like this for training users on a capability-based UI.
I was running an I jumped over a plate an I dint crack my head! I’n't that amazing? I went weeeooo squlksh an I falled in some applesauce.
I have a swim head. My head pops off an I have a swim body.
(William rubs Bruce’s feet.)
Bruce: That feels good!
William: You say funny words!
Wm: Ba’guys punch people.
MJ: Are you a bad guy? You kicked Aidan.
Wm: Ba’guys don’t kick.
Marty (pretending to sword fight): ching ching! Ching!
Wm: (sings) Ching, ching, ching! I love to ching!
Wm (running downstairs to us): I’m NAKED!
MJ: We noticed.
Wm: Yeah. It’s funny. HA HA HA HA!
Mike (noticing Martin’s blue lip): Did you drink the gatorade we told you not to drink?
Marty: William gave it to me and said I should drink it and I drank it.
I’ll be categorifying the lambda calculus. The nicest way of doing this would be to develop a good notion of a 2-theory, of which “the theory of a cartesian closed category” would be one example. It’s already known how to do this for cartesian categories: the kind of 2-theory has products itself, and has one type, a morphism for the product in C and a morphism for the unit; and several 2-morphisms for the diagrams.
Closed categories, however, need some notion of “op,” which is contravariant. Figuring out the nicest way of doing this will be some fun research. Paul Mellies has some ideas.
Hopefully, this kind of 2-theory will also let me talk about things like the blue calculus or Tyler Close’s web calculus (where objects are web services and POST is method invocation; lambda terms are stateless objects responding to the unique “call” method) that he uses in waterken.