<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>