Offtopic: holes and IDEs


#1

Continuing the discussion from Micro Pre-RFC: todo! macro:

@bjz curios, what kind of support for holes do you need from LSP? I think “code actions” pretty much cover everything one can do with a hole, no?


#2

For everyone that (like me) didn’t hear about holes until recently, I found this video to be an excellent resource: https://youtu.be/mOtKD7ml0NU


#3

That talk also shows that in Idris2 there’s a linear typing annotation that’s not just 1 and omega (that corresponds to the number of times you use a value, 1 or arbitrary) but also 0, that’s used more or less for ghost data (in a dependently type language it’s quite important to tell apart the things that will not be present in the binary, like some reified types).


#4

what kind of support for holes do you need from LSP? I think “code actions” pretty much cover everything one can do with a hole, no?

Yeah, you might be right there! I seem to have missed that, so it could be I’ve misinterpreted the protocol in the past. I’ve been through the LSP before, and seen ‘rename’ for example, but not other things, but it seems like code actions would help :thinking:. We’d also need a way of displaying information about the current holes in a file, and the currently selected hole. Can that be supported? These need to be in a nice to read pane - not like a list of errors.


#5

So, yep, you definitely need code actions here.

/aside

One of the hardest problems when building an IDE is teaching your users that a particular feature exists. IDEs have ton of smart thing, but users don’t use them because they don’t even realize such things are possible.

Intention(IntelliJ terminology) or code action (lsp term) are perfect for solving this problem: as soon as you cursor is at something which can be interacted with in a smart way, you get shown a lightbulb, which signifies “hey, I can do something smart here”

/aside

For showing arbitrary info about holes, take a look at hover an code lens.

Showing a lot of content in a separate pane is not really supported by the protocol per se, but it’s easy to extend it to do just that. See how “show syntax tree” thing is implemented in the vscode plugin for rust analyzer.