[Agda] I want implicit coercions in Agda

[Jon Sterling]

I'm a little sympathetic to Mietek's point of view here,  because I've been in the boat where I found for the longest time (and still do in many cases) the conventions of mathematical writing to be just totally perplexing. Now that I'm more used to it, I find it easier going, but even so, the boundary between sensible overloading and perverse overloading is a very fine one, and rarely do mathematical texts actually walk that boundary in a satisfactory way.

But the thing that convinces me of the importance of *some* way to resolve syntactically ambiguous notations (regardless of whether it is realized through implicit coercion, unification hints, type classes, etc.) is that when building hierarchies of structures,  the specifics of how you cooked up the hierarchy (and there are always a million different ways to do this) have a huge effect on what the fully-explicit form of some operator will be. Another point worth mentioning is that even within a *single* discipline for mathematical hierarchies, there may be multiple (commuting) ways to access the same operator, so it is really not so good to be forced to choose one of those in the user-level code.

Some kind of implicit resolution of these things can do a lot to grease the wheels. With that said, I've been unsatisfied and frustrated with all attempts at such implicit resolution that I've used. But I haven't used all of them :)

---

I do not believe that one should necessarily be able to grasp everything that is happening by looking at textual code. Far from being a weakness, the fact that we can (in theory) query our IDE to show us more and more information iteratively is a *strength* of digital presentation formats for mathematics. Back in the paleolithic period, the 1980s, the proof assistant Nuprl introduced a very flexible form of notation extension which did not even require all the constituents of a piece of syntax to be represented in the displayed form -- this was possible because Nuprl used a structure editor with a lossy renderer. The idea was that you could point and click, or use some keystrokes, to explore a term, and explode it to expose more and more information, etc.

A more moderate (and possibly more sensible) version of this interaction style is within our grasp today, where we just omit whatever can be resolved by our most powerful elaborators and unification engines -- and this style is compatible with purely textual formats, not requiring any "rendering" of some more detailed format. Being able to inspect the type of something in Agda's emacs mode is only the beginning. I believe that Idris's emacs mode contains more sophisticated features along these lines, where you can even inspect code that appears quoted in an error message! (Maybe Agda has this now too, but I haven't checked.)

My experience with formalizing mathematics is that one needs to be able to interact with the artifact both at a high level (eyes squinted) and at a low level, seeing every minute detail. We should take advantage of the fact that our editing interfaces are interactive, rather than requiring all this detail to be inlined into the textual representation.

Best,
Jon


On Sat, Nov 17, 2018, at 7:25 AM, Miëtek Bak 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.
> 
> -- 
> (mb)
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda