[Agda] The joys and sorrows of abstraction

[Martin Escardo]

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/
> 
> On 16 May 2018 at 16:03, Martin Escardo <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