[Agda] I want implicit coercions in Agda

[Miëtek Bak]

On Sat, Nov 17, 2018, at 11:40, Martin Escardo wrote:
> On 17/11/2018 10:29, mechvel at botik.ru wrote:
> 
> > Generally, we need to respect mathematical style.
> > It is based on experience of many centuries.
> > Most of the mathematical community really understands which book is
> > easier to read.
> > I tend to trust this approach more.
> 
> Exactly. I fully agree.

I completely disagree.  Ambiguous notation is one of the gravest sins that continue to be inflicted upon students of mathematics.

Leslie Lamport writes:

“Mathematicians think that the logic of the proofs they write is completely obvious, but our examination … shows that they are wrong. Students are expected to learn how to write logically correct proofs from examples that, when read literally, are illogical. … It is little wonder that so few of them succeed.”

“Is it crazy to think that students who cannot learn to write proofs in prose can learn to write them in an unfamiliar formal language and get a computer to check them? Anyone who finds it crazy should consider how many students learn to write programs in unfamiliar formal languages and get a computer to execute them, and how few now learn to write proofs.”

> If implicit coercions are ever implemented, I propose that the emacs 
> mode and the html rendering highlight the implicitly coerced things with 
> a different color so that the reader can see that there is a coercion 
> being applied.

Your proposal recognises that implicit coercions are detrimental to understanding.  Highlighting implicit coercions in colour would still not help the reader resolve which definitions are actually being used.  I would prefer for Agda programs to remain independently checkable, whether they are written by hand, printed out, or displayed on screen.

-- 
(mb)