Revertible thunks as function II: fix recursive overriding #940

yannham · 2022-11-23T17:35:53Z

Revertible thunks are functions

Closes #908.

Follow-up of #924: bring the presentation of revertible thunks as just functions memoization devices to its logical conclusion by providing helper to explicitly rebuild the represented function and apply it. This explicit application was required to fix recursive overriding in the general case, see #908. Now, the implementation faithfully expresses general merging of recursive fields as common_field = fun self => (left_field self) & (right_field self), when recursive record fields are understood as functions of self (representing the ambient record).

Revertible thunks representation

This PR also reworks the representation of revertible thunks. They used to store the cached data as an Rc<Closure>, initialized as soon as the revertible thunks was initialized. This doesn't model revertible thunks faithfully: the cached value should be owned (as it is for normal thunks), and as long as the revertible thunks hasn't be "patched" (or, when seen as a function, applied), the cached value is meaningless and may contain free variables, id est unbound identifiers.

The cached value should never be used before full initialization. This PR sets the cached value to be an Option<Closure>, and to panic if it used before initialization. It also ensures that initialization is done only once. The previous implementation wouldn't complain about such violation. Note that we have no choice to perform the construction of a revertible thunks in two steps, and thus observe a transitory state where the cached value is not initialized, because we are potentially building cyclic values. However, if the implementation is correct, the state where the cached value is set to None shouldn't really be observable.

src/eval/lazy.rs

src/eval/merge.rs

vkleen

I've just found some more typos in the comments. The logic seems good, as far as I can tell 👍

src/eval/lazy.rs

src/eval/merge.rs

matthew-healy

As far as I can tell, this looks good, though I have to say my mental model for exactly what's going on & how it all fits together isn't great and as such I don't feel qualified to give an approving review.

I left one or two small comments but just for minor things. I don't think they need to block merging.

src/eval/lazy.rs

Revertible thunks used Rc<Closure> for the cached data. But when the revertible thunk is first created, the cached data aren't meaningful and can't be used as it is (it has free variables which need to be bound). This change better reflects this reality by using an Option, and by panicking in some illegal patterns (using the cached term before the revertible thunk is properly constructed or trying to build the cached data multiple times). Previously, we would silently accept such operations with the risk of getting spurious unbound variable errors later on.

Some multistep overriding patterns weren't handled correctly broken (see #908). Revertible thunks are to be understood as function, and the previous implementation was trying to away with actually introducing explicit function and application, by patching directly the environment of expressions with free variables. The examples presented in #908 makes it clear that this simplification doesn't work for all cases: this commit fixes the issue by introducing explicit functions and applications in the general case of merging two record fields, instead of relying on environment patching.

Co-authored-by: Viktor Kleen <viktor.kleen@tweag.io>

yannham changed the title ~~Refactor/revthunks are functions 2~~ Revertible thunks as function II: fix recursive overriding Nov 23, 2022

github-actions bot temporarily deployed to pull request November 23, 2022 17:39 Inactive

github-actions bot temporarily deployed to pull request November 24, 2022 13:37 Inactive

github-actions bot temporarily deployed to pull request November 24, 2022 14:33 Inactive

github-actions bot temporarily deployed to pull request November 24, 2022 14:59 Inactive

yannham force-pushed the refactor/revthunks-are-functions-2 branch from 41639fa to b5818dd Compare November 24, 2022 17:54

github-actions bot temporarily deployed to pull request November 24, 2022 17:58 Inactive

yannham marked this pull request as ready for review November 24, 2022 18:04

yannham commented Nov 24, 2022

View reviewed changes