mutation without ref counter check

Stream: lean4

[Tomas Skrivan]

Is it in principle possible to have an FFI function that mutates object without checking the reference counter? This would require for the compiler to prove that the ref counter is one when passing the object and when defining such function you would have to provide two FFI implementation one for reference counter one and other for reference counter bigger than one.

[Mario Carneiro]

The compiler does not know how to do this, even for lean functions (it would be a very useful optimization). Functions always assume their inputs may be shared which means there is a branch at the start of almost all functions

[Tomas Skrivan]

That is unfortunate, maybe we can hope that the new compiler will enable something like this. I'm optimizing some code and where there is no mutation I'm 20% slower than similar implementation in C but when mutation happens the code is 4-10x slower.

[Sebastian Ullrich]

That slowdown doesn't sound right from a branch that should be perfectly predictable?

[Tomas Skrivan]

I agree that it does not sound right that the slowdown is only because of that. There has to be something else too and I should do more profiling.