rfc: show arity of current function

Stream: lean4

[Kenny Lau]

One thing that could make code-writing more convenient would be a way to show the arity of the current function, because functions in Mathlib often has 10+ typeclasses and 3+ implicit arguments, which makes it hard to count how many underscores I need to apply.

Consider the following mini-example:

theorem foo {α β γ : Type}
    [Add α] [Mul α] [Add β] [Mul β] [Add γ] [Mul γ] (h₁ : α = β) (h₂ : β = γ) : α = γ :=
  h₁.trans h₂

example : Nat = Nat :=
  foo

Right now, Lean already has a very helpful feature, where if you put the cursor at the end of foo in Line 6, wait a while, and then press space, then it shows you all the (remaining) arguments of the current function:

image.png

so maybe a way to implement my suggestion would be just to use that existing window, but add a newline at the bottom with the text "2 explicit arguments remaining".

[Eric Wieser]

I think graying out the Implicit arguments would go a long way here

[Marc Huisinga]

Eric Wieser said:

I think graying out the Implicit arguments would go a long way here

This is not supported by either the signature help request in LSP or the VS Code API. I'd also prefer not to make this popup any larger than it needs to be by adding another line to it since it will then also cover more code.

I think a decent improvement would be to highlight the first explicit argument instead, which is supported by the protocol. Since the delaborator and the pretty-printer currently don't retain any of this position information, we'd have to delaborate the implicit prefix, the first explicit argument and everything after that separately and then join the outputs.

[Eric Wieser]

What's the mechanism to do the highlighting?

[Marc Huisinga]

SignatureInformation.activeParameter

[Michael Rothgang]

In #26221, Patrick and I got Kyle Miller to write a version of '#check` that only shows explicit arguments. Would this solve your need?

[Michael Rothgang]

(I share your pain of counting the remaining arguments, particularly in differential geometry, where a declaration easily has 10 arguments, but at most 2 or 3 explicit ones.)

[Kenny Lau]

well i would still have to copy it and then #check it outside as i can't #check in the middle of a sentence

[Marc Huisinga]

(deleted)

[Michael Rothgang]

Given there's a #check tactic (i.e., works in the middle of a proof), #check' could also become one.

[Kenny Lau]

maybe we'll need a check% in the middle of a term

[Kenny Lau]

like unironically

[Julian Berman]

Is using Code Lens a possibility here to consider? Maybe having an optional separate code lens which says the arity?

[Kenny Lau]

what's a code lens?

[Julian Berman]

I think the ones you see in VSCode today are related to git information, but here's a googled old list of few examples (from other languages clearly) https://code.visualstudio.com/blogs/2017/02/12/code-lens-roundup

[Kenny Lau]

what if when we right click on an identifier of a decl it just shows "function arity: 4"?

[Kenny Lau]

as in, above the whole menu

[Kenny Lau]

image.png

[Kenny Lau]

above the "Go to Definition"

[Kenny Lau]

also, maybe formatting is not supported in the "space info", but it's supported in the hover info right

[Kenny Lau]

image.png

[Kenny Lau]

since I see blue colour here

[Kenny Lau]

can we make the implicit arguments gray here?

[Kenny Lau]

related: #lean4 > rfc: on hover, show the type before the error

[Marc Huisinga]

Kenny Lau said:

can we make the implicit arguments gray here?

We serve the types in hovers as a markdown code block with language ID lean, the highlighting for which is provided by the Lean 4 VS Code extension TextMate grammar.
If you want implicit parameters to be highlighted differently in hovers, you have to define a custom TextMate grammar that parses arbitrary Lean pretty-printer output, identifies implicit arguments in a way that doesn't lead to false-positives with other notation using {} or [], contribute that to the VS Code extension with a custom language ID and then change the hovers provided by the language server to produce markdown code blocks with the new language ID. When the pretty-printer changes in a new Lean version, you will then also likely have to update the client-side TextMate grammar.

TextMate grammars are absolutely horrible to maintain as they are just bundles of unreadable regexes, so I don't think this is really worth the initial effort or the maintenance burden.

[Kenny Lau]

I see, that's another unfortunate situation.

[Eric Wieser]

Marc Huisinga said:

identifies implicit arguments in a way that doesn't lead to false-positives with other notation using {} or []

We essentially had this in Lean 3, but it was reverted, I think due to false positives for things like

(x : Fin "oops)".length)

[Eric Wieser]

We'd also need a textmate scope to attach to the implicit arguments, and one doesn't immediately spring to mind

[Kenny Lau]

Marc Huisinga said:

We serve the types in hovers as a markdown code block with language ID lean, the highlighting for which is provided by the Lean 4 VS Code extension TextMate grammar.

can this be changed?

[Kenny Lau]

for example, can we have two code blocks?

[Eric Wieser]

What would the two blocks show?

[Kenny Lau]

it was a hypothetical question, I wanted to know what can be customised, because that response made it sound like it was not tweakable at all

[Marc Huisinga]

Eric Wieser said:

Marc Huisinga said:

identifies implicit arguments in a way that doesn't lead to false-positives with other notation using {} or []

We essentially had this in Lean 3, but it was reverted, I think due to false positives for things like

(x : Fin "oops)".length)

There's another trick that I know of that could be used to get a more maintainable solution to at least part of this problem: while LSP itself only supports Markdown hovers, VS Code also allows rendering a safe subset of HTML tags in the Markdown hover you provide if you set a specific flag (e.g. as in this experiment).

The language server could then define a generic and simple non-HTML format for tagging implicit parameters in the Markdown it produces, which we'd then parse in the language client middleware and convert to HTML that styles implicit parameters accordingly. AFAICT, these HTML tags also have access to VS Code's theme CSS variables, so the styling could be consistent with the current theme.
All of this would have to be locked behind a client capability so that clients that don't support parsing this extended Markdown syntax still get the regular Markdown hovers.

The downside of this is that VS Code obviously won't render the HTML in Markdown code blocks, so while you gain the implicit parameter highlighting, you lose all highlighting that VS Code provides via our TextMate grammar for Lean. We'd have to re-implement much of the highlighting from this grammar in a custom semantic highlighting language for hovers to adequately replace the current implementation. Perhaps this will be the way to go at some point, but I'd need a few more good reasons than just implicit parameter highlighting for it to be worth it :-)

[Kenny Lau]

Marc Huisinga said:

I'd need a few more good reasons

May I present to you these reasons:

image.png

[Eric Wieser]

I don't understand the relevence of that screenshot; did you mean to capture the hover?

[Kenny Lau]

I meant, look at all these wonderful colours we can have

[Aaron Liu]

so colourful

[Aaron Liu]

but is all this really gonna show up in hover info

[Kenny Lau]

well if it shows up here then i take it to mean that the infrastructure already exists? i also kinda know (or at least i think) that these colours are in part server-generated and not based on grammar

[Eric Wieser]

Unfortunately the highlighting is a hybrid of those two systems, and vscode provides no API to execute the textmate system.

[Kenny Lau]

if it looks like monospace font and has spaces in the right places then it is a highlighted code(?)