[Agda] I want implicit coercions in Agda

[Martin Escardo]

If you want mathematicians to use proof assistants, you have to 
implement the notations they use, not the notations that computer 
scientists / engineers find convenient to write computer programs. Martin

On 17/11/2018 15:25, mietek at bak.io wrote:
> 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.
> 

-- 
Martin Escardo
http://www.cs.bham.ac.uk/~mhe