<div dir="ltr"><div>Hi Martin,</div><div><br></div><div>I can easily see why you'd want to limit yourself to such a subset of Agda, and I hope we will be able to support this style of using Agda even better in the future (e.g. having more flags to turn on/off specific features). At the same time, I hope you also understand why we must keep pushing the boundaries of what's possible in Agda, in the hope that one day these 'unsafe' features can also enter the divine realm of commonly accepted type theory.</div><div><br></div><div>One thing I'm wondering is whether you make any use of mutual definitions in your code, specifically inductive-recursive and inductive-inductive definitions. These are often used for universe constructions and extend the power of the type theory quite a bit, but Agda currently has no flags to limit or disable them. Would people be interested in such a flag?<br></div><div><br></div><div>Also, if you have any other flags you would like to see, just let us know and I promise we'll at least consider them seriously :)</div><div><br></div><div>-- Jesper<br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Wed, May 16, 2018 at 10: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=""><br>
<br>
On 16/05/18 21:24, Philip Wadler wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;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:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="">
<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="">
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="">
The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.<br>
<br>
</span></blockquote><span class="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="HOEnZb"><div class="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>