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 | 5066 reads
|
Browse archives
Active forum topics |
Recent comments
16 weeks 4 days ago
16 weeks 4 days ago
16 weeks 4 days ago
38 weeks 5 days ago
43 weeks 13 hours ago
44 weeks 4 days ago
44 weeks 4 days ago
47 weeks 2 days ago
51 weeks 6 days ago
52 weeks 55 min ago