<div dir="ltr"><div><div>This is really scary, for good reason. It seems that we are in a better position now than a few years ago.<br><br></div>I do remember as an undergraduate, thinking that all I need is to start from the fundamentals of Mathematics and then prove all of the rest.<br></div>Then , I found that the fundamentals were full of paradoxes.<br><a href="https://en.wikipedia.org/wiki/Foundations_of_mathematics#Foundational_crisis">https://en.wikipedia.org/wiki/Foundations_of_mathematics#Foundational_crisis</a><br><br></div><div class="gmail_extra"><br><div class="gmail_quote">On Wed, May 16, 2018 at 11:36 PM, Martin Escardo <span dir="ltr"><<a href="mailto:m.escardo@cs.bham.ac.uk" target="_blank">m.escardo@cs.bham.ac.uk</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="gmail-"><br>
<br>
On 16/05/18 21:24, Philip Wadler wrote:<br>
<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
Thanks, Martin. So which fragment do you recommend? Cheers, -- P<br>
</blockquote>
<br></span>
I can't recommend any fragment to you or anybody else. This is<br>
because I don't know which type theories you understand well, and<br>
because I don't know what you want to do with them (your research or teaching interests).<br>
<br>
I can tell you which fragments I work with, and why. I prefer to restrict to fragments of Agda corresponding to well-understood Martin-Loef type theories.<br>
<br>
This is not for dogmatic reasons, but instead because my current research involves them as the base for univalent mathematics, and I use Agda as tool for this research.<br>
<br>
I use Agda to write Martin-Loef type theory constructions (and usually for spartan Martin-Loef type theories).<br>
<br>
"With", instance arguments, "abstract", sized types, irrelevant fields, among others, don't belong to the type theories I understand well, or that people have precisely defined, or that have the blessing of the community as finished things. So I don't use them, either because of ignorance or lack of trust or lack of precise definition.<br>
<br>
(I tried instance arguments, but then my code that compiled in one version of Agda failed in the next, and because I never saw a convincing definition of them, I decided to abandon them, as a non-reliable, non-stable feature.)<br>
<br>
Moreover, I use the options --exact-split and --without-K. The former because I would like to think that, even if I indulge in using (well-founded) recursive definitions by pattern matching, my code should, in principle, be automatically translatable to code that uses "Martin-Loef combinators" only. The latter is because of my current particular field of interest, which allows types that don't necessarily satisfy "uniqueness of identity proofs".<br>
<br>
As an exception, although I don't think implicit-argument resolution is well defined (independently of the Agda implementation), I do use implicit arguments, because they are very convenient. And I don't think they can give rise to serious problems (although I faced a bug once). However, I have observed, and reported, that sometimes new versions of Agda fail to infer implicit arguments that were (correctly) inferred in previous versions. It is a worry that 15000 lines of code may break in the future because of changes in implicit argument resolution (that is, we are not working in a well-defined, stable, type theory for implicit arguments).<br>
<br>
I can say the same for pattern matching, as an exception, but this has been ameliorated with the options --exact-split and --without-K, already mentioned<br>
<br>
Martin<br>
<br>
<br>
<br>
<br>
<br>
<br>
<br>
<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><span class="gmail-">
<br>
. \ Philip Wadler, Professor of Theoretical Computer Science, .<br>
/\ School of Informatics, University of Edinburgh . / \ and Senior<br>
Research Fellow, IOHK . <a href="http://homepages.inf.ed.ac.uk/wadler/" rel="noreferrer" target="_blank">http://homepages.inf.ed.ac.uk/<wbr>wadler/</a><br>
<br></span><span class="gmail-">
On 16 May 2018 at 16:03, Martin Escardo <<a href="mailto:m.escardo@cs.bham.ac.uk" target="_blank">m.escardo@cs.bham.ac.uk</a> <mailto:<a href="mailto:m.escardo@cs.bham.ac.uk" target="_blank">m.escardo@cs.bham.ac.u<wbr>k</a>>> wrote:<br>
<br>
<br>
<br>
On 16/05/18 20:37, Philip Wadler wrote:<br>
<br>
Thanks for following up. It is the latter case. But I don't understand why it should be ok for that to fail. Removing abstract<br>
should just replace some abstract terms by their concretions, which<br>
have already been type checked. Everything that was provably equal<br>
before should still be equal, so why is it ok for the proof of<br>
equality to now fail? Doesn't this violate stability under<br>
substitution? Cheers, -- P<br>
<br>
<br>
It is because of things such as this that I prefer to restrict my usage of Agda to a fragment corresponding to a well-understood type theory.<br>
<br>
This may be limiting in terms of expressivity, conciseness, and efficiency, but at least one can tell whether something is a bug or not, rather than a bug or a feature.<br>
<br>
:-) Martin<br>
<br>
<br>
<br>
<br></span><span class="gmail-">
The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.<br>
<br>
</span></blockquote><span class="gmail-HOEnZb"><font color="#888888">
<br>
-- <br>
Martin Escardo<br>
<a href="http://www.cs.bham.ac.uk/~mhe" rel="noreferrer" target="_blank">http://www.cs.bham.ac.uk/~mhe</a></font></span><div class="gmail-HOEnZb"><div class="gmail-h5"><br>
______________________________<wbr>_________________<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/mail<wbr>man/listinfo/agda</a><br>
</div></div></blockquote></div><br></div>