User loginNavigation 
Parameterized Notions of ComputationParameterized Notions of Computation, Robert Atkey, JFP 2008.
Once you've programmed with monads for a while, it's pretty common to start defining parameterized families of monads  e.g., we might define a family of type constructors for IO, in which the program type additionally tracks which files the computation reads and writes from. This is a very convenient programming pattern, but the theory of it is honestly a little sketchy: on what basis do we conclude that the indices we define actually track what we intend them to? And furthermore, why can we believe that (say) the monadic equational laws still apply? That's the question Atkey lays out a nice solution to. He gives a nice categorical semantics for indexed, effectful computations, and then cooks up lambda calculi whose equational theory corresponds to the equations his semantics justifies. The application to delimited continuations is quite nice, and the type theories can also give a little insight into the basics of how stuff like Hoare Type Theory works (which uses parameterized monads, with a very sophisticated language of parameters). On a slightly tangential note, this also raises in my mind a methodological point. Over the last n years, we've seen many people identify certain type constructors, whose usage is pervasive, and greatly simplified with some syntactic extensions  monads, comonads, applicative functors, arrows, and so on. It's incredible to suggest that we have exhausted the list of interesting types, and so together they constitute a good argument for some kind of language extension mechanism, such as macros. However, all these examples also raise the bar for when a macro is a good idea, because what makes them compelling is precisely that the right syntax yields an interesting and pretty equational theory in the extended language. By neelk at 20090211 21:40  Category Theory  Lambda Calculus  Semantics  Type Theory  other blogs  13681 reads

Browse archivesActive forum topics
New forum topics

Recent comments
3 days 18 hours ago
5 days 12 hours ago
2 weeks 2 days ago
3 weeks 1 day ago
4 weeks 1 day ago
5 weeks 6 days ago
6 weeks 2 days ago
7 weeks 3 days ago
7 weeks 6 days ago
8 weeks 1 hour ago