[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