<html>
  <head>

    <meta http-equiv="content-type" content="text/html; charset=utf-8">
  </head>
  <body bgcolor="#FFFFFF" text="#000000">
    <p>Despite my <a
        href="https://github.com/agda/agda/issues/426#issuecomment-254111273">best
        efforts</a> to try to get around the performance problems that
      are seemingly inherent in call-by-name, I have not found a
      satisfactory solution, so I've come to agree that we need a
      different evaluation strategy. Exactly what, I don't know, but I'm
      starting to read through the Agda (Haskell) code, hoping to put
      myself in a position to help.<br>
    </p>
    <p>I'd like some explanation how the current call-by-need
      implementation, `--sharing`, works (or doesn't) and get your
      thoughts on what a promising solution might look like. <br>
    </p>
    <p>On the subject of `--sharing`, Ulf Norell mentioned <a
        href="https://github.com/agda/agda/pull/1867#issuecomment-187596312">here</a>
      that it's too problematic to continue improving. I'd like to know
      what's fundamentally wrong with it. He mentions <a
        href="https://github.com/agda/agda/issues/426#issuecomment-129023261">here</a>
      that substitution is not memoizing pointers, but I'm guessing that
      that could be fixed and is *not* what's fundamentally wrong with
      `--sharing`. In the same comment he mentions that a particular
      where clause is problematic for `--sharing` "because of lambda
      lifting". I'm unclear on how this is breaking call-by-need. Is the
      function in the where clause getting lambda lifted? Does that
      somehow lead to the top-level function not getting memoized?<br>
    </p>
    <p>What's the future of Agda's evaluation strategy?</p>
    <p>(If this should have been posted in the issue tracker, please
      continue the conversation there.)</p>
  </body>
</html>