Lambda the Ultimate

The following will be of interest to many of us:

We are sorry to announce that Robin Milner died on Saturday 20th March, in Cambridge, just three days after the funeral of his wife, Lucy.

He will be greatly missed by his family and friends, as well as the academic community.

We are expecting there to be a symposium in due course to provide an opportunity for Robin's many academic colleagues to celebrate him and his work.

From Chloë and Barney Milner

This discussion relates to the recent Advantages of Purity discussion.

My questions can be summarised as: How are effect systems mainly used in current implementations? Are they widely used for source-level(-ish) optimisations? If yes, where? If not, why?

One of the issues raised in the Purity thread was that pure computations are easier to reason about. Effect systems has been proposed to assist reasoning about stateful computations, most prominently by Benton et. al.'s Monads, Effects and Transformations.

However, Benton only proves a limited number of identities (variants of the ones their Exceptions paper (figures 8-10). But I was interested in more equations. Thinking that effect analysis is common in compiler optimisations, I started looking for implementations of effect systems that make use of the analysis to optimise the program.

As Benton's language is a fragment of MLj's intermediate language, that seemed like a good place to start. However, it has been a while since MLj saw some activity, and besides, I couldn't find any reference to compiler optimisations based on effect analysis in MLj.

I then consulted with several colleagues about using effect type systems for optimisations. To summarise that conversation and the look around I had after it:

• Pure code has benefited greatly from optimisations via source-code transformations. e.g., Haskell, especially a la Santos's thesis: Compilation by Transformation in Non-Strict Functional Languages.
• Even in languages that apply source-code transformation optimisations, optimising effectful code is done at the object-code level, and not as source-code optimisations.

What I am wondering is why effectful transformations are not used in practice? Is it because there is missing theory about effectful transformations? Or is it simply because source-code transformations are not nearly as efficient as object-code transformations? If so, what kind of evidence backs this claim up?