RFC for vscode extension to optionally show refcounts

Stream: lean4

[Shreyas Srinivas]

This is probably a moonshot request, but I wondered if it is possible for the extension to tag def parameters with their reference count in the definition (shown in faded small text like the rust extension does for showing types and lifetimes). This feature could be toggled by users.

[Henrik Böving]

Shreyas Srinivas said:

This is probably a moonshot request, but I wondered if it is possible for the extension to tag def parameters with their reference count in the definition (shown in faded small text like the rust extension does for showing types and lifetimes). This feature could be toggled by users.

What do you mean by refcount here?

[Shreyas Srinivas]

I want to track whether a structure such as an array is updated in-place or a copy is made

[Shreyas Srinivas]

I understand that this happens depending on the reference count for the object

[Joachim Breitner]

Unfortunately, that's pretty moonshot: The refcount is a dynamic property that you cannot in general know until you run the program. It's at least as hard as wanting to see the value of a function's parameter, in other words, a debugger.

[Shreyas Srinivas]

Okay, but that's digging into FP's equivalent of a call stack. What about locally?

[Shreyas Srinivas]

Surely if there are two copies of an object these copies are made locally

[Shreyas Srinivas]

In some function

[Shreyas Srinivas]

What would a pathological counterexample look like?

[Henrik Böving]

Shreyas Srinivas said:

Okay, but that's digging into FP's equivalent of a call stack. What about locally?

There is no equivalent of a call stack, lean compiles to C, there is a real call stack.

Shreyas Srinivas said:

Surely if there are two copies of an object these copies are made locally

If you make a copy of something you do that because the RC was > 1 but you wanted to change it. If you mean reference then you can still not figure them out statically. If you have a branch where one side uses a value and the other does not the ref count for that value after that branch is fuzzy. Same for passing values to other functions where they might or might not be referenced in the return value etc etc.

[Mario Carneiro]

@Reed Mullanix and I have been talking about implementing something like a linter for statically analyzing the IR to identify when things marked as linear are copied, using something like quantitative type theory. But it's all still very abstract. @Marc Huisinga also had some work on this, unsure what state it ended up in though. I think it would be useful to try to get something working even if it has to be very approximate in cases, because debugging IR is no fun at all and it's not even good enough to write linear code by hand because the compiler itself breaks linearity accidentally.

[Shreyas Srinivas]

@Henrik Böving : I know this is not deterministically possible, but there must be some heuristics or some subset of cases where the extension could offer a clue by maybe just highlighting the references that are most definitely linear (in a conservative way)?

[Shreyas Srinivas]

Sorry this message was in my drafts 3 hours ago

[Shreyas Srinivas]

@Mario Carneiro : Is it viable to have a shadow type system imposed on a language that checks linearity on the side using some conservative heuristics and reports violations, but doesn't interfere in compilation otherwise? I have in mind the way liquid haskell is integrated into haskell.

[Henrik Böving]

The work by Marc mentioned by Mario is from here: https://pp.ipd.kit.edu/uploads/publikationen/huisinga23masterarbeit.pdf The closing remark reads:

Our type theory lacks support for uniqueness attributes in higher-order functions, type inference, as well as support for attribute polymorphism. Our escape analysis produces non-satisfactory results on recursive functions over recursive types, inhibiting the borrowing of arguments to such functions.

...

For higher-order functions, we have evaluated all existing approaches known to us and made a recommendation for an approach that we think is the most suitable one to implement in the future. For borrowing, we have made suggestions to improve the implementation provided in this thesis. For the topics of type inference, polymorphism and Lean 4 integration, we have outlined steps that need to be taken in order to complete the implementation thereof.

So even with this prior work there would still be a ton to do to make it feasible to have this in practice.

[Henrik Böving]

Mario Carneiro said:

Reed Mullanix and I have been talking about implementing something like a linter for statically analyzing the IR to identify when things marked as linear are copied, using something like quantitative type theory. But it's all still very abstract. Marc Huisinga also had some work on this, unsure what state it ended up in though. I think it would be useful to try to get something working even if it has to be very approximate in cases, because debugging IR is no fun at all and it's not even good enough to write linear code by hand because the compiler itself breaks linearity accidentally.

Note that the compiler does not only break linearity accidentally there are cases where it is straight up fine to break linearity. I encountered this in code where two arrays of equal size (but in fact different member type) are allocated after one another. The compiler will perform CSE on the array creating functions and copy the second array when it is modified for the first time. This is a completely fine modification as it doesn't induce any additional load that would have been there without CSE. So even properly detecting a linearity failure at runtime is non trivial. The best approach I've found so far (and how I e.g. tracked down the HashMap.erase issue) is to add a modification to the runtime that tracks "generations of cloned arrays" and if a generation chain copies arrays of non trivial size too many times in a row it is decided that its most likely a true linearity issue and I make it crash.

If anyone was able to come up with a reliable way to perfectly detect linearity issues at runtime (without modifying the runtime and making it notably slower like I did) this would already be a gigantic step forward. dbgTraceIfShared is also suboptimal as simply introducing it can lead to linearity issues in of itself.

[Mario Carneiro]

I encountered this in code where two arrays of equal size (but in fact different member type) are allocated after one another. The compiler will perform CSE on the array creating functions and copy the second array when it is modified for the first time. This is a completely fine modification as it doesn't induce any additional load that would have been there without CSE.

I assume this is only CSE after erasing types? In any case I don't really agree this is a good tradeoff, the compiler will often move array creation into statics, replacing a fresh allocation with a copy from an existing allocation, which isn't really better (the plain allocation function can often do a better job, e.g. if the fill value is a constant and can be built using calloc or memset, and the extra static allocation is pure overhead and might even cause memory issues if it's a really big fixed size array which now has to exist twice in the program).

[Henrik Böving]

Yes this is CSE after partial type erasure.

[Mario Carneiro]

Note that the compiler does not only break linearity accidentally there are cases where it is straight up fine to break linearity.

The version of this idea I was thinking about is that the user would annotate a particular variable as being unique, meaning either that the compiler should try to optimize the function with the incoming assumption that the value is unique and copy if needed before calling it rather than inside the function (this will often cut out an extra if statement in the inner loop of tight loops like List.reverseCore), or for linting purposes as an indication that any copies of the value in the function should be flagged.

[Mario Carneiro]

I think it is difficult for the compiler to do a better job of linearity analysis than it is doing already without additional annotations because the information is simply not present in the code. You might be able to do better with some kind of instrumented dynamic analysis but this doesn't sound very easy/noninvasive