[Agda] I want implicit coercions in Agda

[Jason -Zhong Sheng- Hu]

Since Coq has coersion, I use this functionality there. I assume that the use of coersion is not limited to the agda program text, but should also be presented in the interaction, namely in the proof window, the coersion functions would also be hidden. In this situation, another request would probably follow immediately after coersion is implemented in Agda: add a switch to (temporarily) turn it off.

Sometimes coersion can be confusing. I am not against it (since I use it), but I would say that this functionality could be very misleading if it overshoots too much, so the design of it is very important. I think the reason of this disagreement here is because there is only one view of the program text, so we either have a very high level view but abstract, or a very low level view but too verbose. If we can have a hierarchy of views, which allows us to zoom in and out of mathematics/proofs/programs, I think coersion can have way more value.

Sincerely Yours,

Jason Hu

________________________________
From: Agda <agda-bounces at lists.chalmers.se> on behalf of Martin Escardo <m.escardo at cs.bham.ac.uk>
Sent: November 18, 2018 3:43 PM
To: ulf.norell at gmail.com
Cc: Agda mailing list
Subject: Re: [Agda] I want implicit coercions in Agda



On 18/11/2018 20:35, ulf.norell at gmail.com wrote:
> On Sun, Nov 18, 2018 at 9:12 PM Martin Escardo <m.escardo at cs.bham.ac.uk
> <mailto:m.escardo at cs.bham.ac.uk>> wrote:
>
>
>     You will not solve the shortcomings of my mathematical style by
>     refusing
>     to implement implicit coercion in Agda.
>
>
> I feel that the discussion has derailed a little at this point. The
> issue isn't that some people
> are stubbornly refusing to implement this

This reply was not directed to the Agda developers, but instead to the
people who ranted against these features.

I will be happy to give a list of things for which implicit coercions
are used by mathematicians, including those of my own Agda developments.

Martin

_______________________________________________
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/20181118/5ab015a6/attachment.html>