Brian Hulley wrote:
Robin Green wrote:
On Wed, 29 Mar 2006 12:50:02 +0100 Jon Fairbairn <jon.fairbairn@cl.cam.ac.uk> wrote:
[snip] 1) choosing the optimal reduction strategy is undecidable
2) we shouldn't (in general) attempt to do undecidable things automatically [snip] [snip] I suggest that a Haskell program should be treated as an executable specification. In some cases the compiler can't optimise the program well enough, so we (by which I mean, ordinary programmers, not compiler geeks) should be able to explicitly provide our own optimisations, as rewrite rules (generalised ones, or specialised ones for individual functions). Democratise the means of automated optimisation!
This sounds good. The only thing I'm wondering is what do we actually gain by using Haskell in the first place instead of just a strict language? It seems that Haskell's lazyness gives a succinct but too inefficient program which then needs extra code in the form of rewrite rules/pragmas, or else a complete rewrite in terms of seq etc to get it to run fast enough without space leaks...
Thinking about this some more, I realised Jon had already answered this question in his 3rd point: On Wed, 29 Mar 2006 12:50:02 +0100 Jon Fairbairn <jon.fairbairn@cl.cam.ac.uk> wrote: > 3) Separation of concerns: Pragmatic decisions about > evaluation order should be kept separate from the > denotational aspect of the code. By this token, seq I wonder if there could be a really large repository of rewrite rules on the web somewhere, with heuristics to determine various strategies for applying them. There would also need to be some automated way of proving correctness of rewrite rules, so that if someone submitted a new one it would be sure not to introduce bugs into the optimization. In this way, the Haskell community could gradually chip away at the undecidableness of automatically optimizing Haskell programs, because it may turn out to be the case that most functions are members of a very small subset of the possible Haskell functions and could thus be handled by a finite set of rewrite rules. Regards, Brian.