rfc: allow docstrings on instance implementation members

Stream: lean4

[Alok Singh]

Was working on FPIL and ran into this issue: docstrings above pure and bind are illegal syntax. I was thinking of making an RFC where any docstrings added would be prepended with a divider marker to the docstring of the typeclass docs. presumably docs on specific impls are more concrete and informative than the abstract docs (in this case for Monad), hence handy to have around. Also handy for hover to get more specific info about something like, say, a ToString instance for floating point revealing details of just how it does it since it's famously tricky.

Example that sparked idea:

/-- A monadic action -/
abbrev ConfigIO (α) := Config → IO α

/--This is a monad because it has a pure and bind function-/
instance : Monad ConfigIO where
  /--Pure ignores the config-/
  pure a : _ := fun _ => pure a
  /--Bind takes a config and a function that takes a config and returns an IO action, and returns an IO action-/
  bind result next := fun cfg => do
    let newConfig  <- result cfg
    next newConfig cfg

[Kim Morrison]

Where are you proposing these doc-strings would go?

[Alok Singh]

On the hovers of any uses of a type class. So toString 5.0 would show float’s specific docstring for the toString call plus whatever general docstring toString has in its original declaration in a class block.

[Alok Singh]

And these more specific strings would be declared in an instance blocks like above

[Kyle Miller]

I'm not sold on docstrings on structure instance fields yet, but the docstring on the instance showing up in the hover for toString is seems interesting.

[Tomas Skrivan]

I agree that somehow showing both doc string would be nice.

Also what about go-to-definition behavior? I would like to have both options, jump either to the declaration of the class field or jump to the particular instance.

[Henrik Böving]

Thats within the LSP protocol as they have go to definition/go to implementation as separate things AFAIK so this can likely be handled

[Jovan Gerbscheid]

(deleted)

[Jovan Gerbscheid]

Tomas Skrivan said:

I would like to have both options, jump either to the declaration of the class field or jump to the particular instance.

This already exists to some degree. If I write example : (HAdd.hAdd : Nat → Nat → Nat) = HAdd.hAdd := rfl, and I go to definition on the first HAdd.hAdd one of two things can happen (depending on which of my vscode windows I'm in :thinking: )

• it goes to the definition of HAdd.hAdd
• it shows a pop up which allows me to choose between going to the defition of either HAdd.hAdd, instAdd or instAddNat.

(see also here)

[Jovan Gerbscheid]

afbeelding.png

[Jovan Gerbscheid]

Maybe it works in the Lean repository and not the Mathlib repository?