Okay, so since I was travelling for five hours for Memorial Day weekend then I wanted to do something kind of easy in the car on the way here.
It's a paper that everyone should have (and probably has) read: Moggi's paper on monads and the computational lambda calculus.
The most basic point of this paper is a pretty well known story: strong monads act as generalized let-statements in the internal language of a category. Why do they need to be strong? Well, the strength essentially acts as a way of ensuring that you can "copy" the context from the binding part of the let-statement to be available in the final expression.
Okay, yay, monads!
Well, no, there's more to it than that. One thing that really jumped out at me when I was rereading this paper in the car was the methodical, elegant development that built up the internal language alongside the models by adding richer categorical constructions. It was really cute, but also an approach I see very rarely done in CS literature even though to me it feels very constructive and enlightening. I feel like that's the kind of approach I want to have to my own research once, y'know, I actually start publishing (*cough cough*). So, anyway, even if you already know the whole story of using monads in semantics I think there's something to be said for sitting down and working through this paper. It's really well structured, which I think is probably a good bit of why it was influential.
No comments:
Post a Comment