[Haskell-cafe] Compiler's bane

[Jonathan Cast]

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
> > <andrewcoppin at btinternet.com> 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