<div dir="ltr"><div dir="ltr"><div dir="ltr"><div>I cannot resist citing this prior work from no less than Bjarne Stroustrup (designer of C++) about the dangers of overloading (implicit coercions and the like):</div><div>  <a href="http://www.stroustrup.com/whitespace98.pdf" target="_blank">http://www.stroustrup.com/whitespace98.pdf</a></div><div><br></div><div>Apart from that I generally agree on the need and use of this kind of mechanisms.</div><div>Agda might feel slightly more conservative that Coq here, but to me this follows from the fact that Agda tends to have less distinction between proofs and programs.</div><div>In a way, proof irrelevance is less of a principle in Agda than in Coq. Programs matter and which implicit choice has been made matters too.</div><div><br></div><div>For instance if more than one coercion can be used it should make a choice which remains principled and unambiguous.</div><div>If there is really a need to give priority to some coercions, then it should be make explicit by the programmer. Maybe something similar to operator precedence.</div><div><br></div><div>To me a concrete first step would build around a Coerce record and instance arguments plus some syntactic help to use it.</div><div>Would it make sense to reuse idiom brackets?</div><div><br></div><div>Best,</div><div>Nicolas</div></div></div><br><div class="gmail_quote"><div dir="ltr">On Thu, Nov 8, 2018 at 9:16 PM Martin Escardo <<a href="mailto:m.escardo@cs.bham.ac.uk" target="_blank">m.escardo@cs.bham.ac.uk</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">... and I am sure many other people do too.<br>
<br>
Many other proof assistants have them.<br>
<br>
Is there a philosophical reason for that, or is this something that just <br>
hasn't been done yet?<br>
<br>
Real-life mathematics has them in abundance, and it would be nice to <br>
reflect this in Agda.<br>
<br>
I would like to press for a design and implementation of this in Agda. :-)<br>
<br>
Best,<br>
Martin<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div><br clear="all"></div>