[Agda] evaluation strategies of the future [issue #426]

[Martin Stone Davis]

Despite my best efforts 
<https://github.com/agda/agda/issues/426#issuecomment-254111273> 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.

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.

On the subject of `--sharing`, Ulf Norell mentioned here 
<https://github.com/agda/agda/pull/1867#issuecomment-187596312> that 
it's too problematic to continue improving. I'd like to know what's 
fundamentally wrong with it. He mentions here 
<https://github.com/agda/agda/issues/426#issuecomment-129023261> 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?

What's the future of Agda's evaluation strategy?

(If this should have been posted in the issue tracker, please continue 
the conversation there.)

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20161023/f6b368d0/attachment.html