Mutable Value Semantics vs. FBIP

Stream: general

[Somo S.]

Does anyone know how Mutable Value Semantics (MVS) differs from Lean4's Functional But In-Place (FBIP) paradigm?

MVS is implemented in val-lang and defined in this paper.

[Mario Carneiro]

Lean does not have anything like MVS. From what I can tell by reading the paper, this is a way of indicating that a value or part of a value is mutable and there are operations that perform mutations of the parts. By contrast, FBIP is an optimization, where the user writes code that never mutates values explicitly, but certain patterns can reuse the storage of a consumed value and hence reconstruct mutation at the low level.

There are advantages and disadvantages to making it an optimization instead of a change in semantics. An advantage is that the user doesn't have to be explicitly bothered about mutation, they can just write functional code (and reason about the code at that level) and the compiler does its best to make sense of the code. So it can fire even in code that is not using mutable variable patterns explicitly. A disadvantage is that because it is an optimization, you have no guarantee that it will occur, and small changes to the code or the compiler can cause spurious copies and performance instability. Lean has let mut in the do notation, but this is just syntax for (more or less) a state monad. It would be nice if it could include sufficient annotations so as to ensure FBIP; then one could achieve MVS by using let mut and approved combinators.

[Mauricio Collares]

https://www.microsoft.com/en-us/research/uploads/prod/2023/07/fip.pdf is also related

[Somo S.]

@Mauricio Collares said:

https://www.microsoft.com/en-us/research/uploads/prod/2023/07/fip.pdf is also related

@Mario Carneiro said:

A disadvantage is that because it is an optimization, you have no guarantee that it will occur, and small changes to the code or the compiler can cause spurious copies and performance instability.

My (crude) understanding of the new paper above is it provides precisely basis for making those guarantees? This is neat stuff thanks for sharing and explaining I'm quite new to all this.

[Somo S.]

I have been trying to get a better sense for how lean compares to Rust in terms of memory management (not safety but more along the lines of performance). I had initially thought FBIP is meant to offer the kinds of memory guarantees that rust compiler does.. But I see that that is not the case, ... perhaps if this newer FIP research is incorporated?

[Henrik Böving]

Rust is more in the uniqueness type corner. The master thesis by Marc Huisinga does explore these topics but it is sadly not integrated with the main system yet.

[Max Nowak 🐉]

I’d love to explore some guaranteed compiler optimizations, akin to rust, with users having a lot of control (via the type system) how their lean code gets mapped to low level code.