Make it easier to see the types of expressions

[bblfish]

Agda-mode for vscode is a big improvement over emacs by allowing one to see the definitition of any expression by hovering over it with command key pressed.

But it would be great if one could also see the type of an expression and missing expressions without needing to punch in holes everywhere. (In emacs that seems to be the only way to do things). I always get a bit worried that I am going to accidentally make a mistaken change to some library by punching a hole in somewhere and have that be saved to the disk.

I guess this is a limitation of the agda compiler which I guess is providing information to the editor. I am writing it up here, as it could also be useful as a suggested improvement there.

[gallais]

In emacs that seems to be the only way to do things

Do you know about the command C-c C-d to infer the type of an expression?

[bblfish]

yes, but it does not always work. Say I want to find out the value of f on line 249 of Graphs from Agda Categories.

C-c C-d tells me it is not in scope. I have to make a hole like I did in the picture below. Then I might as well see the whole Goal.

Actually the linked-to code has 𝛌 {_ _ f} → ... on that line, and I wanted to know what the types of the two unused parameters were, so that I could understand how the function was working. To see those in the goal I had to name them. (So it would be helpful to be able to see that directly by hovering the mouse over it). The same for the various records: it would be useful to know what types they are implementing quickly.

[bblfish]

Btw here is a screenshot showing how one can hover over a part of the code in VSCode with Agda-mode when pressing the command key to get a definition. That is a very nice feature, but it does not give interesting information currently when hovering over the variables in a lambda. In that case it just repeats the definition, where what one would like would be to know the type of the expression.

[banacorn]

Inferring type by hovering on an expression is exactly what I tried to implement after go-to-definition. But as you can see, we are reaching Agda's limit. I even thought about punching a temporary hole to access those local expressions (nah, it's a bad idea).

To implement this feature, we have to either:

1. Extend the Emacs protocol
2. Extend the JSON protocol and switch to the JSON protocol (we are currently running on the Emacs protocol.)
3. Implement a proper LSP language server (standalone? or bake into Agda?)

Either way it's gonna take a lot of time and effort. But for the time being, we can allow users to inspect type by hovering over a top-level definition (using C-c C-d)

[bblfish]

For reference for people looking at this issue coming from emacs, this the info I get when hovering over the lambda variable i. Clearly that is not that useful. What I was looking for is to find out what the type of it is. If I punch a hole below I find out that it is i : GraphMorphism G₀ G.

Btw, these are quite small features (compared to the investment in the whole of Agda) but my feeling is that these types of feature (including issue 27) are quite important if one wants to get say mathematicians to teach this to undergraduates, where one wants a very smooth entry into the area (see the talk and comments on this recent tweet thread).

My background is using IntelliJ with Java and for the past 10 years (on and off) Scala.