Re: [Haskell-cafe] Compiler's bane

On Sun, 2008-08-31 at 17:29 +0100, Andrew Coppin wrote:

Ryan Ingram wrote:

...

On Sun, Aug 31, 2008 at 12:46 AM, Andrew Coppin wrote:

...

Right. So if I have, say, the factorial function defined using the Y combinator, there's no way to stop the interpretter expanding an infinite number of copies of Y, even though in theory the factorial function should terminate?

Well, this is exactly what ghci is doing; you just have to choose an evaluation order that makes sense.

Lets consider a simple translation for recursive lets:

...

let x = exp1 in exp2

(where x may be free in exp1 and/or exp2)

Here's a simple translation into lambda-calculus:

...

(\x. exp2) (y (\x. exp1))

(Of course, this representation for let can lose sharing; without knowing what you have or your goals I don't know if you care).

Now, you just have to choose a y-combinator that makes sense for your evaluation order. If you do normal-order evaluation like Haskell ("non-strict"), this Y should work for you:

y = \f. (\x. f (x x)) (\x. f (x x))

...

Oh well, I guess I'll just have to live with that one. Maybe I can make the binding to expand user-selectable or something...

Now, if you are eagerly-expanding the entire expression, trying to get to head normal form, then any expression that ends up with "y" in it won't terminate. But if you use normal form evaluation order, then if a normal form exists, you will find it and terminate.

So evaluating "fact" to normal form won't terminate, but evaluating "fact 5" should.

All of this strongly suggests that if you execute things in the correct order, you can arrange it so that expressions that have a normal form will be evaluated to it. But how to decide the correct evaluation order? For the plain lambda calculus, IIRC you just have to execute the left-most, outer-most redex every time and it'll work. For a language with let-binds, it is unclear to me how to proceed...

It depends on whether you want to preserve sharing or not. If not, you can use fix to de-sugar lambdas, and then de-sugar lets using the rule let x = e in f = (\ x -> f) e and proceed as before. Or (again, if you don't care about sharing), you can descend recursively into the body of a let, remembering where the bindings were defined, and expand variables when you see them. Or keep an environment around, extend it on let, and if the left-most outermost redex is a variable, look it up. jcc