[Haskell-cafe] Compiler's bane

[Ryan Ingram]

On Sun, Aug 31, 2008 at 9:29 AM, Andrew Coppin
<andrewcoppin at btinternet.com> wrote:
> 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...

What are you trying to get from the "let" binding?  Sharing?

The usual idea is that "let" represents heap allocation, and you
evaluate the leftmost-outermost redex as usual, doing let substitution
only when necessary to continue evaluation, and garbage-collecting
bindings that no longer refer to variables in the current computation.
 You also make lambda-expressions create let-bindings during
substitution to maximize sharing.

Here's an example of how an interpreter could work:

let fact_acc = \n x. (== n 0) x (fact_acc (- n 1) (* n x))
in fact_acc 3 1

The "top-level" redex is a let bind that is already in WHNF; if it
wasn't, you continue evaluation inside of it.  So instead you
substitute and lose sharing because there are no other options.

I'm going to leave all previous "lets" as "..." in this evaluation to
save typing:

(substitute because leftmost-outermost redex is a let-bind)
=> let ... in (\n x. (== n 0) x (fact_acc (- n 1) (* n x))) 3 1
(beta, beta)
=> let ...; n0 = 3; x0 = 1 in (== n0 0) x0 (fact_acc (- n0 1) (* n0 x0))
(primitive == is strict, n0 is already in normal form, evaluate ==)
=> let ... in False x0 (fact_acc (- n0 1) (* n0 x0))
(False x y = y)
=> let ... in fact_acc (- n0 1) (* n0 x0)
(substitute fact_acc, beta, beta)
=> let ...; n1 = (- n0 1); x0 = (* n0 x0) in (== n1 0) x1 (fact_acc (-
n1 1) (* n1 x1))
(primitive == is strict, evaluate its argument.
 primitive - is strict, argument is in whnf, evaluate -)
(This is a very important step; note that I am now evaluating inside
of a let bind!)
=> let ...; n1 = 2; ... in (== n1 0) x1 (fact_acc (- n1 1) (* n1 x1))
(evaluate ==)
=> let ... in False x1 (fact_acc (- n1 1) (* n1 x1))
(False x y = y)
=> let ... in fact_acc (- n1 1) (* n1 x1)
=> let ...; n2 = (- n1 1); x2 = (* n1 x1) in (== n2 0) x2 (fact_acc (-
n2 1) (* n2 x2))
=> let ...; n2 = 1; ... in (== n2 0) x2 (fact_acc (- n2 1) (* n2 x2))
=> let ... in False x2 (fact_acc (- n2 1) (* n2 x2))
=> let ... in fact_acc (- n2 1) (* n2 x2))
=> let ...; n3 = (- n2 1); x3 = (* n2 x2) in (== n3 0) x3 (fact_acc (-
n3 1) (* n3 x3))
=> let ...; n3 = 0; ... in (== n3 0) x3 (fact_acc (- n3 1) (* n3 x3))
=> let ... in True x3 (fact_acc (- n3 1) (* n3 x3))
=> let ... in x3
(We can garbage collect fact_acc and n3 here)
=> let
  n0 = 3; x0 = 1;
  n1 = 2; x1 = (* n0 x0);
  n2 = 1; x2 = (* n1 x1);
  x3 = (* n2 x2) in x3
(primitive * is strict, so we get a big spine of evaluating x3 which
requires x2 which requires x1 which requires x0 which is finally
already in head normal form)
=> let ...; x1 = (* 3 1); x2 = (* 2 x1); x3 = (* 1 x2) in x3
(garbage collect n0, n1, n2, n3)
=> let x1 = 3; x2 = (* 2 x1); x3 = (* 1 x2) in x3
(substitute & garbage collect x1)
=> let x2 = (* 2 3); x3 = (* 1 x2) in x3
=> let x2 = 6; x3 = (* 1 x3) in x3
=> let x3 = (* 1 6) in x3
=> let x3 = 6 in x3
=> 6

Does this seem like something you could do?

  -- ryan