<div dir="ltr">Thanks!  This is very interesting.  (And thanks all for sources.)<div><br></div><div>I'm still digesting this, but have one question already:</div><div>> Clearly, we should use NbE/environment machines for evaluation, and implement conversion checking in the semantic domain.</div><div><br></div><div>Does this mean that we can't be agnostic about whether or not we're supporting HoTT, because we either have to pick set theory/irrelevant equality proofs or cubical (or some other model of HoTT) when normalizing proofs of equality?</div><div><br></div><div>> I'd be very interested in your findings about proof assistant performance.</div><div><br></div><div>I'd be happy to share once I have my thesis in a sufficiently ready state!  Broadly, the message of my thesis is that performance of (dependently-typed) proof assistants / interactive theorem provers is an interesting area of research sorely in need of systematic study.  (My thesis will also include some of the research work I've done, which can be rendered as "how to work around some of the asymptotics in Coq without needing to change the system", but I think that's a bit less broadly interesting.)</div><div><br></div><div>-Jason</div><div><br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Fri, May 8, 2020 at 4:55 AM András Kovács <<a href="mailto:kovacsandras@inf.elte.hu">kovacsandras@inf.elte.hu</a>> wrote:<br></div><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"><div dir="ltr">Hi Jason,<div><br></div><div>You may be interested in my github repos: <a href="https://github.com/AndrasKovacs/smalltt" target="_blank">smalltt</a>, <a href="https://github.com/AndrasKovacs/normalization-bench" target="_blank">normalization-bench</a>. I haven't yet updated the smalltt repo, but there's a <a href="https://gist.github.com/AndrasKovacs/a0e0938113b193d6b9c1c0620d853784" target="_blank">simplified implementation</a> of its evaluator, which seems to have roughly the same performance but which is much simpler to implement. </div><div><br></div><div>The basic idea is that in elaboration there are two primary computational tasks, one is conversion checking and the other is generating solutions for metavariables. Clearly, we should use NbE/environment machines for evaluation, and implement conversion checking in the semantic domain. However, when we want to generate meta solutions, we need to compute syntactic terms, and vanilla NbE domain only supports quote/readback to normal forms. Normal forms are way too big and terrible for this purpose. Hence, we extend vanilla NbE domain with lazy non-deterministic choice between two or more evaluation strategies. In the simplest case, the point of divergence is whether we unfold some class of definitions or not. Then, the conversion checking algorithm can choose to take the full-unfolding branch, and the quoting operation can choose to take the non-unfolding branch. At the same time, we have a great deal of shared computation between the two branches; we avoid recomputing many things if we choose to look at both branches.</div><div><br></div><div>I believe that a feature like this is absolutely necessary for robust performance. Otherwise, we choke on bad asymptotics, which is surprisingly common in dependent settings. In Agda and Coq, even something as trivial as elaborating a length-indexed vector expression has quadratic complexity in the length of the vector. </div><div><br></div><div>It is also extremely important to stick to the spirit of Coquand's semantic checking algorithm as much as possible. In summary: core syntax should support *no* expensive computation: no substitution, shifting, renaming, or other ad-hoc term massaging. Core syntax should be viewed as immutable machine code, which supports evaluation into various semantic domains, from which sometimes we can read syntax back; this also leaves it open to swap out the representation of core syntax to efficient alternatives such as bytecode or machine code. </div><div><br></div><div>Only after we get  the above two basic points right, can we start to think about more specific and esoteric optimizations. I am skeptical of proposed solutions which do not include these. Hash consing has been brought up many times, but it is very unsatisfying compared to non-deterministic NbE, because of its large constant costs, implementation complexity, and the failure to handle sharing loss from beta-redexes in any meaningful way (which is the most important source of sharing loss!). I am also skeptical of exotic evaluators such as interaction nets and optimal beta reducers; there is a good reason that all modern functional languages run on environment machines instead of interaction nets. </div><div><br></div><div>If we want to support type classes, then <a href="https://arxiv.org/pdf/2001.04301.pdf" target="_blank">tabled instance resolution</a> is also a must, otherwise we are again smothered by bad asymptotics even in modestly complex class hierarchies. This can be viewed as a specific instance of hash-consing (or rather  "memoization"), so while I think ubiquitous hash-consing is bad, some focused usage can do good. </div><div><br></div><div>Injectivity analysis is another thing which I believe has large potential impact. By this I mean checking whether functions are injective up to definitional equality, which is decidable, and can be used to more precisely optimize unfolding in conversion checking.</div><div><br></div><div>I'd be very interested in your findings about proof assistant performance. This has been a topic that I've been working on on-and-off for several years. I've recently started to implement a system which I intend to be eventually "production strength" and also as fast as possible, and naturally I want to incorporate existing performance know-how.</div><div><br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">Jason Gross <<a href="mailto:jasongross9@gmail.com" target="_blank">jasongross9@gmail.com</a>> ezt írta (időpont: 2020. máj. 8., P, 0:20):<br></div><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">I'm in the process of writing my thesis on proof assistant performance bottlenecks (with a focus on Coq).  I'm having some trouble finding prior work on performance engineering and/or benchmarking of proof assistants (other than the paper on the Lean tactic language (<a href="https://leanprover.github.io/papers/tactic.pdf" target="_blank">https://leanprover.github.io/papers/tactic.pdf</a>)), and figured I'd reach out to these lists.<div><br></div><div>Does anyone have references for prior work on performance analysis or engineering of proof assistants or dependently typed languages?  (Failing that, I'd also be interested in papers about compile-time performance of compilers.)<div class="gmail_quote"><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"><div></div></div>
</blockquote></div></div><div><br></div><div>Thanks,</div><div>Jason</div></div>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>
</div>
</blockquote></div>