title: floating pass of fully lazy lambda lifting?
body: <p>I'm reading <a href="http://research.microsoft.com/en-us/um/people/simonpj/Papers/pj-lester-book/">implementing functional languages: a tutorial</a>, and encountered a problem when implementing floating pass of fully lazy lambda lifting.</p>
  
  <p>I would like to describe how floating works to make this question clear, if you are familiar with it, <strong>just skip to the question below</strong>.</p>
  
  <p>The concept is introduced at page 246 in the paper, and mainly implemented at page 256-257.</p>
  
  <p>In case of <code>let(rec)</code> expression, it says:</p>
  
  <blockquote>
    <p>we must put floated definitions of right-hand side before the <code>let(rec)</code> expression itself, since the right-hand side may depend on them.</p>
  </blockquote>
  
  <p>for example:</p>
  
  <pre><code>\a -&gt;
    let f = \b -&gt; b + (let $mfe = a * a in $mfe)
    in f
  </code></pre>
  
  <p>The variable <code>$mfe</code> is a <em>maximal free expression (MFE)</em> which identified by previous pass, when dealing with <code>let f</code> expression, we float <code>f</code> out as one group and append it to <code>[(1, [($mfe, a * a)])]</code>, which was obtained from right-hand side of <code>let f</code>. Here, the first component <code>1</code> indicates the <em>free level</em> of the group.</p>
  
  <p>When backtracking to <code>\a -&gt; f</code> abstraction, we found that both <code>$mfe</code> and <code>f</code> are bound by it, hence we should install them here:</p>
  
  <pre><code>\a -&gt;
    let $mfe = a * a
    in
      let f = \b -&gt; b + $mfe
      in f
  </code></pre>
  
  <h1>The Question</h1>
  
  <p>Suppose we have a program like this:</p>
  
  <pre><code>f = \x -&gt; \y -&gt;
    letrec
      a = \p -&gt; cons p (b x)
      b = \q -&gt; cons q (a y)
    in pair (a 1) (b 2)
  </code></pre>
  
  <p>The <em>free level</em> of <code>b x</code> and <code>a y</code> will be 2, since <code>y</code> has level 2 and they are in a same group.</p>
  
  <p>While <em>free level</em> of <code>cons p (b x)</code> and <code>cons q (a y)</code> is 3, thus <code>b x</code> and <code>a y</code> will be marked as MFEs (Did I make mistakes here?).</p>
  
  <p>Using the algorithm given by SPJ, the program will be transformed into:</p>
  
  <pre><code>f = \x -&gt; \y -&gt;
    let $ay = a y -- `a` is not defined yet!
    in
      let $bx = b x -- and `b`
      in
        letrec
          a = \p -&gt; cons p $bx
          b = \q -&gt; cons q $ay
        in pair (a 1) (b 2)
  </code></pre>
  
  <p>I think the MFEs in the right-hand side of <code>let(rec)</code> expression should <strong>not</strong> escape the <code>let(rec)</code> scope whenever it referenced to the left-hand side, and the correct result might like this:</p>
  
  <pre><code>f = \x -&gt; \y -&gt;
    letrec
      $ay = a y
      $bx = b x
      a = \p -&gt; cons p $bx
      b = \q -&gt; cons q $ay
    in pair (a 1) (b 2)
  </code></pre>
  
  <p>Does the paper wrong? or I just misunderstood it.</p>