[Agda] I want implicit coercions in Agda

[Apostolis Xekoukoulotakis]

I wonder what is more confusing : Using "+" and "*_i" to denote addition
for Nat and addition for Integers
or "+" and "+" to denote addition for both Nat and Integers.

Using correct symbols that do not confuse is a responsibility that cannot
be avoided even without coercions.

If we are able to inspect terms of a proof , any confusion is removed
entirely, while at the same time simplifying our proof.



On Mon, Nov 19, 2018 at 6:45 AM Peter Hancock <hancock at fastmail.fm> wrote:

> On 18/11/2018 21:32, Jason -Zhong Sheng- Hu wrote:
> > 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.
>
> Someone who's opinion is worth having about the presentation of
> mathematical material is Lamport.  I am thinking about his
> specification language TLA+, and  its proof system TLP (I think).
>
> These formalisms were designed to be used by engineers, who I suppose
> are mathematicians of some kind. Stylistically, they resemble COBOL,
> with lots of upper-case keywords, etc.  IMHO, they are readable, largely
> because notational fuss is kept to a minimum.  Things are designed to be
> emailable in ASCII.
>
> Most interesting is that TLP is designed for writing informal proofs.
> At any point, you can put in an informal "handwave" (a bit like a hole).
> A "folding" metaphor is used to browse TLP proofs. You can choose to
> hide uninteresting portions of a proof, and drill down to
> particular steps in full gory detail.  Lamport says one should
> write a proof in small enough steps that everything is completely obvious,
> then provide one more level of formal proof.
>
> I presume coercions are injective functions that resolve type-clashes
> between
> things like natural numbers and signed integers, or fractions, etc.
> There are times when we want to see these things, and there are times
> when we would like them to be hidden.
> Could one have a "pedantry" knob when editing or browsing agda?
> At pedantry level 11 absolutely nothing would be hidden....
>
> Sergie's gave some examples of using "+", "*" etc to mean different
> operations in different rings.  Is this an example of coercion?
> I'm inclined to call it overloading.  (Which also helps to dispense with
> pedantic crap.)
>
>
>
> _______________________________________________
> 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/20181119/8f94ab18/attachment.html>