On Fri, 2007-03-30 at 13:04 -0700, Tim Chevalier wrote:

On 3/30/07, skaller wrote:

...

I'm curious when and how GHC applies rewrite rules, and how expensive it is.

Have you seen the "Playing By Rules" paper? http://research.microsoft.com/~simonpj/Papers/rules.htm

If you still have questions after reading it, you can always ask here.

Thanks for that reference! FYI, the authors comment that the possibility exists for feeding reduction rules into a theorem prover but it has not been explored. This IS indeed being done right now by Felix. Felix supports axioms, lemmas, and reduction rules. Lemmas are theorems which are simple enough to be proven with an automatic theorem prover. A couple of days ago my first test case lemma was proven by Ergo and Simplify. (roughly I proved that given x + y = y + x and x + 0 = x, that 0 + x = x .. not exactly rocket science :) Felix emits all the axioms and lemmas in Why notation, which allows a large class of theorem provers to have a go at proving them, since Why translates them. Reductions aren't handled yet because doing this raised a simple syntactic problem: I have no way to distinguish whether a reduction is an axiom or a lemma. I would note also that default definitions of typeclass functions are also axioms. What would be REALLY cool is to prove that typeclass instances conform to the specified semantics. That, however, is much harder, especially in Felix (which is an imperative language ;( See also: http://why.lri.fr IMHO: connecting a programming language to a theorem prover is probably mandatory for optimisation. Obvious goals other than reduction rules are elimination of pre-condition checks for partial functions. However doing this is hard because theorem provers can be slow, so generally have to be run offline. Thus some way of caching the results for a subsequent recompilation is required. -- John Skaller <skaller at users dot sf dot net> Felix, successor to C++: http://felix.sf.net