User loginNavigation |
Effectful Code TransformationsThis 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
|
Browse archives
Active forum topics |
Recent comments
27 weeks 1 day ago
27 weeks 2 days ago
27 weeks 2 days ago
49 weeks 3 days ago
1 year 1 week ago
1 year 3 weeks ago
1 year 3 weeks ago
1 year 5 weeks ago
1 year 10 weeks ago
1 year 10 weeks ago