<div dir="ltr">Thanks! If I write this up, I will use those numbers. Take this as an indication that revising the system to exploit sharing would be valuable. Cheers, -- P<div class="gmail_extra"><br clear="all"><div><div class="m_2983893001657727455gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><div><div dir="ltr">. \ Philip Wadler, Professor of Theoretical Computer Science,<br>. /\ School of Informatics, University of Edinburgh<br></div><div>. / \ and Senior Research Fellow, IOHK<br></div><div dir="ltr">. <span><a href="http://homepages.inf.ed.ac.uk/wadler/" target="_blank">http://homepages.inf.ed.ac.uk/<wbr>wadler/</a></span></div></div></div></div></div>
<br><div class="gmail_quote">On 16 May 2018 at 10:30, Ulf Norell <span dir="ltr"><<a href="mailto:ulf.norell@gmail.com" target="_blank">ulf.norell@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div>I believe the problem you've run into is that we don't have explicit sharing in the</div><div>internal terms. The normal form of `normalise 100 ⊢four` is small, but the weak-head</div><div>normal form is huge, and the type checker compares terms for equality by successive</div><div>weak-head reduction steps. The lack of explicit sharing means that evaluation won't be</div><div>shared across reduction steps.<br></div><div><br></div><div>Here are some numbers:</div><div><br></div><div>n size of whnf of `normalise n ⊢four` (#nodes in syntax tree)</div><div>1 916<br></div><div>2 122,597<br></div><div>3 53,848,821<br></div><div>4 ??</div><div>100 ????</div><span class="m_2983893001657727455HOEnZb"><font color="#888888"><div><br></div><div>/ Ulf<br></div><div><br></div></font></span></div><div class="gmail_extra"><br><div class="gmail_quote"><div><div class="m_2983893001657727455h5">On Wed, May 16, 2018 at 12:07 AM, Philip Wadler <span dir="ltr"><<a href="mailto:wadler@inf.ed.ac.uk" target="_blank">wadler@inf.ed.ac.uk</a>></span> wrote:<br></div></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div><div class="m_2983893001657727455h5"><div dir="ltr"><div>Ulf, Thanks again for your help. It is a great relief to be able to execute my proven-correct code!</div><div><br></div><div>But there seems to be a further issue. Executing `normalise 100 ⊢four` terminates quickly. However, if I paste the result into the file and ask Agda to check that `normalise 100 ⊢four` is equal to the result of its own execution then type checking still takes forever to terminate (where "forever" means "longer than five minutes"). I expect this corresponds to some spot where call-by-name is still used instead of call-by-need. Fortunately, it is not on my critical path, but I thought I should alert you to the issue.</div><div><br></div><div>I've attached the code, or you can find it at <a href="https://github.com/wenkokke/sf/src/" target="_blank">https://github.com/wenkokke<wbr>/sf/src/</a>.</div><div><br></div><div>Cheers, -- P<br></div></div><div class="gmail_extra"><span><br clear="all"><div><div class="m_2983893001657727455m_-7264721551307868910m_3328790701723824216gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><div><div dir="ltr">. \ Philip Wadler, Professor of Theoretical Computer Science,<br>. /\ School of Informatics, University of Edinburgh<br></div><div>. / \ and Senior Research Fellow, IOHK<br></div><div dir="ltr">. <span><a href="http://homepages.inf.ed.ac.uk/wadler/" target="_blank">http://homepages.inf.ed.ac.uk/<wbr>wadler/</a></span></div></div></div></div></div>
<br></span><div><div class="m_2983893001657727455m_-7264721551307868910h5"><div class="gmail_quote">On 10 May 2018 at 18:35, Philip Wadler <span dir="ltr"><<a href="mailto:wadler@inf.ed.ac.uk" target="_blank">wadler@inf.ed.ac.uk</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">Yay! I downloaded an up-to-date Agda (version 2.6.0-2f2f4f5) and it works now! A big thank you to Ulf and Wen for their help. -- P</div><div class="gmail_extra"><span><br clear="all"><div><div class="m_2983893001657727455m_-7264721551307868910m_3328790701723824216m_-4849418691487706764gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><div><div dir="ltr">. \ Philip Wadler, Professor of Theoretical Computer Science,<br>. /\ School of Informatics, University of Edinburgh<br></div><div>. / \ and Senior Research Fellow, IOHK<br></div><div dir="ltr">. <span><a href="http://homepages.inf.ed.ac.uk/wadler/" target="_blank">http://homepages.inf.ed.ac.uk/<wbr>wadler/</a></span></div></div></div></div></div>
<br></span><div class="gmail_quote"><span>On 9 May 2018 at 12:14, Ulf Norell <span dir="ltr"><<a href="mailto:ulf.norell@gmail.com" target="_blank">ulf.norell@gmail.com</a>></span> wrote:<br></span><div><div class="m_2983893001657727455m_-7264721551307868910m_3328790701723824216h5"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><br><div class="gmail_extra"><span><div class="gmail_quote">On Wed, May 9, 2018 at 3:32 PM, Philip Wadler <span dir="ltr"><<a href="mailto:wadler@inf.ed.ac.uk" target="_blank">wadler@inf.ed.ac.uk</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr">Ulf,<div><br></div><div>Any further progress with this?</div><div><br></div><div>Wen downloaded HEAD, but cannot execute even four steps of reduction on his 2010 MacBook Pro. </div><div><br></div><div>I have not downloaded HEAD (I'm cautious about Agda updates because if I break Agda I'm on my own trying to fix it). With the version below, four steps of reduction takes five minutes, and full reduction does not complete overnight.</div><div><br></div><div>I'm wondering if perhaps the issue is not version of Agda but available memory? How much is on your machine?</div><div><br></div><div>Any other progress at tracking down what the issue might be?</div></div></blockquote><br></div></span><div class="gmail_quote">I'm all but certain that the issue that makes it slow on 2.5.3 is call-by-name. Development Agda has call-by-need.<br></div><div class="gmail_quote">I've tracked down the mysterious issue that made some cases check fast and others not. The problem was that<br></div><div class="gmail_quote">we accidentally reverted back to call-by-name evaluation in some situations. I have a patch that just needs some<br></div><div class="gmail_quote">testing before deployment.<br><br></div><div class="gmail_quote">It's not a memory issue. Type checking the file that executes all the way to normal form requires less than 400M.<br></div><div class="gmail_quote">My suspicion is that there's a path issue or similar making Wen still run an old Agda. It would be helpful to see the<br></div><div class="gmail_quote">result of running<br><br></div><div class="gmail_quote"><span style="font-family:monospace,monospace">agda --version<br></span></div><div class="gmail_quote"><span style="font-family:monospace,monospace">agda Test.agda +RTS -s<br></span><br></div><div class="gmail_quote">on this Test.agda:<br><br><div style="margin-left:40px"><span style="font-family:monospace,monospace">module Test where</span><br><span style="font-family:monospace,monospace"></span><br><span style="font-family:monospace,monospace">open import Agda.Builtin.Equality</span><br><span style="font-family:monospace,monospace">open import Agda.Builtin.Bool</span><br><span style="font-family:monospace,monospace">open import TypedFresh</span><br><span style="font-family:monospace,monospace"></span><br><span style="font-family:monospace,monospace">isNormal : ∀ {M A} {⊢M : ε ⊢ M ⦂ A} → Normalise ⊢M → Bool</span><br><span style="font-family:monospace,monospace">isNormal (out-of-gas _ _) = false</span><br><span style="font-family:monospace,monospace">isNormal (normal _ _ _) = true</span><br><span style="font-family:monospace,monospace"></span><br><span style="font-family:monospace,monospace">proof : isNormal (normalise 15 ⊢four) ≡ true</span><br><span style="font-family:monospace,monospace">proof = refl</span><br></div><br></div><div class="gmail_quote">For reference, if I have up-to-date interface files for the imported modules, this takes 3s and <400M memory<br></div><div class="gmail_quote">on my machine with Agda version 2.6.0-20c3e9d.<span class="m_2983893001657727455m_-7264721551307868910m_3328790701723824216m_-4849418691487706764HOEnZb"><font color="#888888"><br><br></font></span></div><span class="m_2983893001657727455m_-7264721551307868910m_3328790701723824216m_-4849418691487706764HOEnZb"><font color="#888888"><div class="gmail_quote">/ Ulf<br></div><div class="gmail_quote"><br></div></font></span></div></div>
</blockquote></div></div></div><br></div>
</blockquote></div><br></div></div></div>
<br></div></div><span>The University of Edinburgh is a charitable body, registered in<br>
Scotland, with registration number SC005336.<br>
<br></span></blockquote></div><br></div>
</blockquote></div><br></div></div>