[Agda] The joys and sorrows of abstraction

[Jesper Cockx]

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 :)

-- Jesper

On Wed, May 16, 2018 at 10: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/20180517/38e19a1e/attachment.html>