[Agda] I want implicit coercions in Agda

[Nicolas Pouillard]

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):
  http://www.stroustrup.com/whitespace98.pdf

Apart from that I generally agree on the need and use of this kind of
mechanisms.
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.
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.

For instance if more than one coercion can be used it should make a choice
which remains principled and unambiguous.
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.

To me a concrete first step would build around a Coerce record and instance
arguments plus some syntactic help to use it.
Would it make sense to reuse idiom brackets?

Best,
Nicolas

On Thu, Nov 8, 2018 at 9:16 PM Martin Escardo <m.escardo at cs.bham.ac.uk>
wrote:

> ... and I am sure many other people do too.
>
> Many other proof assistants have them.
>
> Is there a philosophical reason for that, or is this something that just
> hasn't been done yet?
>
> Real-life mathematics has them in abundance, and it would be nice to
> reflect this in Agda.
>
> I would like to press for a design and implementation of this in Agda. :-)
>
> Best,
> 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/20181123/f10fc4db/attachment.html>