Home » forums » LtU Forum

Effectful Code Transformations

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:

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?

By Ohad Kammar at 2010-03-22 14:59 | LtU Forum | previous forum topic | next forum topic | other blogs | 5111 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Code Transformations for Effectful Code

I would be somewhat suspicious of that latter premise. Static Single Assignment (SSA), for example, is a transformation often used for effectful code, and is used to simplify other optimizations.

But there are many large optimization that are hindered greatly by effectful source, such as those related to reordering (and parallelization), partial evaluation, and elimination of unnecessary calls (memoization, lifting complex expressions from loops, etc.). Effects can be order-dependent, so reordering can change their semantics. Partial-evaluation and elimination are both forms of reordering (elimination can be viewed as infinite delay of a computation).

Modularity and abstraction exacerbate these difficulties. Without modular abstractions, one could recognize and reason about the actual effects of code to support optimizations. With modular abstractions, one must reason about some code only via an interface to it.

That is where effect-typing steps in, allowing both the developer and the optimizer and other static analysis tools to know and reason about selected relevant properties of modular components.

Similarly, substructural typing allows optimizations that are difficult even with pure code. I.e. if a large vector is passed about linearly, then one may update it in-place. And region types can simplify garbage collection. Again, these properties can be recognized and optimized, but modular abstractions can hinder recognition. Substructural typing can enforce the properties, and allow the optimizer to take advantage of them... albeit at an oft severe cost to generality of abstraction!

Issues of modularity are diminished in context of just-in-time compilations, which allow code to potentially be specialized and optimized to actual use at runtime.

By dmbarbour at Mon, 2010-03-22 16:41 | login or register to post comments

Mind the Gap?

Regarding SSA, I'm not sure whether it qualifies as an optimisation. It strengthens/enables other optimisations, but in itself is not an optimisation. But there's no doubt it's a useful transformation.

You've named the following effectful optimisations with their side conditions. These optimisations, apart from memoization, actually appear in Benton's paper:

  • reordering corresponds to the Commuting Computations rule.
  • partial evaluation corresponds to the beta and eta rules.
  • lifting complex expressions from loops corresponds to the Pure Lambda Hoist rule.

So, if you gave a comprehensive list of current-day effectful optimisations, and if I'm not wrong in claiming that Benton's work encompass all of these, then we already have the theoretical basis for effectful optimisations.

These assumptions mean that we should see effect systems galore (and their optimisations) in compilers. But we don't, do we?

When I asked around, I was told that OCaml doesn't do much optimisations, Haskell optimises effectful code in the object language (if you consider monads as your effect system, a la Wadler's Marriage of Monads and Effects).

So why is there a gap?

By the way, thanks for highlighting memoization as (possibly) unhandled by Benton's work.

By Ohad Kammar at Mon, 2010-03-22 18:34 | login or register to post comments

Hardly a comprehensive list

if you gave a comprehensive list of current-day effectful optimisations, and if I'm not wrong in claiming that Benton's work encompass all of these, then we already have the theoretical basis for effectful optimisations

Your assertion confuses me. I stated that I was listing optimizations that are hindered by effectful code, not supported by it. And it isn't comprehensive in either case.

That said, reordering/parallelization and partial-evaluation, and others are among the most important. I've heard that "partial evaluation is the mother of all optimizations", and I've found plenty of reason to believe it.

These assumptions mean that we should see effect systems galore (and their optimisations) in compilers.

To a small degree, compilers already take advantage of effect analysis when performing optimizations. But the deeper optimizations aren't something that can be readily added "in compiler" without also achieving support from the language. Issues such as aliasing, concurrency, and modularity tend to interfere.

By dmbarbour at Mon, 2010-03-22 23:37 | login or register to post comments

Apologies

I'm sorry if I caused confusion. The optimisations that are hindered by the presence of effects are the ones that can benefit the most from effect analysis, or from a better theory of optimisations. Benton gives exact conditions when one can apply these optimisations, even in stateful computations.

By Ohad Kammar at Tue, 2010-03-23 01:19 | login or register to post comments

Analysis is Insufficient

The optimisations that are hindered by the presence of effects are the ones that can benefit the most from effect analysis, or from a better theory of optimisations.

I do not believe that 'effects analysis' is going to offer significant benefits in absence of support from the language. And by 'support from the language' I mean from its type-system or its syntactically enforced structure.

In practice, the problem of 'effects analysis' is to handle late-binding of code - modularity, polymorphism, abstraction, upgrade. Even the mere possibility of a late-binding effect will render effects-analysis blind with respect to that effect. And almost every non-trivial program involves late-binding of code (object-oriented is a whole paradigm based on that idea). Effects analysis isn't going to offer much benefit under most common conditions... not unless you do more than mere analysis, as by actually enforcing useful effect constraints in the language.

Issues such as late-binding, polymorphism, and modularity are beyond the purview of Benton's paper.

Benton gives exact conditions [...]

Benton's conditions are not 'exact'. Benton proved that given optimizations would be correct under certain conditions, but did not prove that those are the only conditions under which given optimizations would be correct.

By dmbarbour at Tue, 2010-03-23 05:25 | login or register to post comments