[Agda] The joys and sorrows of abstraction

[Apostolis Xekoukoulotakis]

This is really scary, for good reason. It seems that we are in a better
position now than a few years ago.

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.
Then , I found that the fundamentals were full of paradoxes.
https://en.wikipedia.org/wiki/Foundations_of_mathematics#Foundational_crisis


On Wed, May 16, 2018 at 11:36 PM, Martin Escardo <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/
>>
>> 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
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180516/b8ef4a58/attachment.html>