[Agda] The joys and sorrows of abstraction

Martin Escardo m.escardo at cs.bham.ac.uk
Thu May 17 10:21:30 CEST 2018



On 17/05/18 10:08, Jesper at sikanda.be wrote:
> Hi Martin,
> 
> 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.
> 
> 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?
> 
> 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 :)

Thanks, this is very kind of you. I have a lists of things I would like. :-)

But let me write this properly rather than as an immediate reaction now.

Martin


> 
> -- Jesper
> 
> On Wed, May 16, 2018 at 10:36 PM, Martin Escardo 
> <m.escardo at cs.bham.ac.uk <mailto:m.escardo at cs.bham.ac.uk>> wrote:
> 
> 
> 
>     On 16/05/18 21:24, Philip Wadler wrote:
> 
>         Thanks, Martin. So which fragment do you recommend? Cheers, -- P
> 
> 
>     I can't recommend any fragment to you or anybody else. This is
>     because I don't know which type theories you understand well, and
>     because I don't know what you want to do with them (your research or
>     teaching interests).
> 
>     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.
> 
>     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.
> 
>     I use Agda to write Martin-Loef type theory constructions (and
>     usually for spartan Martin-Loef type theories).
> 
>     "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.
> 
>     (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.)
> 
>     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".
> 
>     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).
> 
>     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
> 
>     Martin
> 
> 
> 
> 
> 
> 
> 
> 
>         .   \ Philip Wadler, Professor of Theoretical Computer Science, .
>         /\ School of Informatics, University of Edinburgh .  /  \ and Senior
>         Research Fellow, IOHK . http://homepages.inf.ed.ac.uk/wadler/
>         <http://homepages.inf.ed.ac.uk/wadler/>
> 
>         On 16 May 2018 at 16:03, Martin Escardo <m.escardo at cs.bham.ac.uk
>         <mailto:m.escardo at cs.bham.ac.uk> <mailto:m.escardo at cs.bham.ac.uk
>         <mailto:m.escardo at cs.bham.ac.uk>>> wrote:
> 
> 
> 
>         On 16/05/18 20:37, Philip Wadler wrote:
> 
>         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
>         should just replace some abstract terms by their concretions, which
>         have already been type checked. Everything that was provably equal
>         before should still be equal, so why is it ok for the proof of
>         equality to now fail? Doesn't this violate stability under
>         substitution? Cheers, -- P
> 
> 
>         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.
> 
>         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.
> 
>         :-) Martin
> 
> 
> 
> 
>         The University of Edinburgh is a charitable body, registered in
>         Scotland, with registration number SC005336.
> 
> 
>     -- 
>     Martin Escardo
>     http://www.cs.bham.ac.uk/~mhe
> 
>     _______________________________________________
>     Agda mailing list
>     Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>     https://lists.chalmers.se/mailman/listinfo/agda
>     <https://lists.chalmers.se/mailman/listinfo/agda>
> 
> 

-- 
Martin Escardo
http://www.cs.bham.ac.uk/~mhe


More information about the Agda mailing list