archives

Admin notes

Several changes in the discussion dynamics on LtU require attention, I think.

First, and most important, is that the core business of LtU - the home page blog items posted by contributing editors - have been dwindling. What is more, the discussion forum, whose goal was to support the blog, have become very active, and often only tangentially on topic for LtU.

I have received complaints from long time members about the declining quality of the discussions, and while I haven't done any serious comparative analysis I do know that I now regularly skip threads, especially highly active threads and threads that are dominated by only a few members. I think I am not alone in this. I encourage long time members to continue publicly pointing out when threads become un-LtU-like, and remind everyone that these notes should not usually serve as opportunity for meta-discussions about policy.

I urge the LtU contributing editors to make an extra effort in the next few months to post quality items to the home page. It seems that without more emphasis on the blog, LtU will lose its relevance. I call on all members to keep in mind the style and policies of LtU (do read the spirit page, if you haven't already), and move inappropriate discussions to other forums.

The second issue is - of course - spam. We are constantly bombarded by spam, most of which you don't see since me and Anton manage usually to block the spam accounts from posting, and when spam does slip through we delete it fairly quickly. Still, in the last few days some spam messages did appear on the site, and took awhile to delete, despite our continued efforts. I apologize for that.

In previous discussions of this issue it was decided not to require approval for all new messages (however, I do moderate posts from suspicious accounts). Spam does not survive a long time on LtU, since the site is active and threads that are posted to automatically appear in the tracker, and is thus not a great concern most of the time.

I don't think the last attack was enough of a problem for us to change our policies, or spend time writing code to support advanced spam handling (there are many more exciting things we can be doing for LtU). If someone wants to help with the process of identifying suspicious accounts, deleting spam, and blocking ips, please volunteer. Help with running LtU is always appreciated.

Parameterized Notions of Computation

Parameterized Notions of Computation, Robert Atkey, JFP 2008.

Moggi's Computational Monads and Power et al's equivalent notion of Freyd category have captured a large range of computational effects present in programming languages. Examples include non-termination, non-determinism, exceptions, continuations, side-effects and input/output. We present generalisations of both computational monads and Freyd categories, which we call parameterised monads and parameterised Freyd categories, that also capture computational effects with parameters.

Examples of such are composable continuations, side-effects where the type of the state varies and input/output where the range of inputs and outputs varies. By also considering structured parameterisation, we extend the range of effects to cover separated side-effects and multiple independent streams of I/O. We also present two typed λ-calculi that soundly and completely model our categorical definitions — with and without symmetric monoidal parameterisation — and act as prototypical languages with parameterised effects.

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.