hacspec / hax

A Rust verification tool
https://hacspec.org/blog
Apache License 2.0
198 stars 20 forks source link

`FnMut` closures are not supported yet #1060

Open franziskuskiefer opened 2 weeks ago

franziskuskiefer commented 2 weeks ago

In the code below, the test_fails functions throws errors, while test_works is fine.

struct Test {
    k: Option<u8>,
    y: u8,
}

impl Test {
    fn test_works(&mut self) {
        match self.k.take() {
            Some(k) => {
                self.y = 5;
            },
            None => (),
        }
    }

    fn test_fails(&mut self) {
        self.k.take().map(|k| {
            self.y = 5;
        });
    }
}

Open this code snippet in the playground

maximebuyse commented 1 week ago

I think it is reasonable to fail on test_fails and not on test_works because the mutation of self happens inside a closure in test_fails. Those two implementations look similar in the Rust world but if you try to "functionalize" this mutation this means the closure must return the new value of self, but then that would not go well with the closure type expected by map.

karthikbhargavan commented 1 week ago

Does that mean that we do not currently support mutation within map? If so, that would be good to document.

maximebuyse commented 1 week ago

Does that mean that we do not currently support mutation within map? If so, that would be good to document.

Yes, except maybe if the mutation is on the argument of the closure.

W95Psp commented 3 days ago

Ah yes, thanks @maximebuyse, somehow I missed that closure! Clearly, we do not support mutable closures (aka FnMut).

Some quick notes on supporting FnMuts:

  • normal closures to FP is great, the capture is a primitive feature of our target languages
    • some of our backend cannot support lambdas
    • in presence of FnMut, the environment becomes something we don't want only to consume but also to mut.
    • calling an FnMut requires the fn to be &mut