feat: push down lets #736

brprice · 2022-10-20T14:37:52Z

This addresses #44

Notes for reviewers: I suggest going commit-by-commit, but first have a look at my comments-on-code below, some of which have come detached from the code (and thus won't show up in the commit-by-commit review) due to a rebase.

brprice · 2022-10-20T16:11:52Z

Notes-to-self:

Just the last few commits are relevant, the rest will go away when rebase onto brprice/test-merge-eval
Rip out complexity that is no longer needed due to all rules being local
I am slightly worried about performance, especially for unit_8 and unit_9, and should investigate before merging (edit: I think this can be much improved by "push&elide" so we don't build up big pointless substitutions; whilst this helps unit_8, it seems to slightly harm unit_9)
(edit) [see also the below comment feat: push down lets #736 (comment)] the fact that we fully evaluate in types before moving on to terms is more silly now. Consider (Λa.λx.t : ∀a.S->T) @A which reduces to ((let a = A in λx.t) : (let a = A in S -> T)) s: we really should be able to do one push step in the term and its annotation and then do the next beta step, rather than fully evaluating the annotation. This will need a bit of work in the evaluator, perhaps each position could say either "I'm a redex", "I'm normal" or "I'm blocked by child". I doubt I'll address this in this PR, but I have written up the issue (WIP) FR: do not be so eager to reduce in types #1097 about it
I have seen a PBT failure Use '--pattern "$NF ~ /redex independent/" --hedgehog-replay "Size 33 Seed 5711241534988400105 12645965422690476717"' to reproduce from the command-line. This is because pushing the let in let a = e in ((λx. t : A -> B) s) will break the beta redex
'--pattern "$NF ~ /redex independent/" --hedgehog-replay "Size 19 Seed 4491965300491221527 3689869688095105079"' . Fixed (iirc, was because PushLet can change into ElideLet by inner computation, e.g. let x=1 in case Nil of Nil -> emptyHole; Cons y ys -> x reduces to let x=1 in emptyHole.)
revisit comments on findNodeByID and Cxt

dhess · 2023-06-19T10:58:27Z

once we address this, let's circle back to #559, as it is affected by this PR.

primer/primer.cabal

primer/test/Tests/Eval.hs

primer/src/Primer/Eval/Redex.hs

primer/test/Tests/Eval.hs

primer/test/Tests/EvalFull.hs

primer/src/Primer/Eval/Redex.hs

primer/src/Primer/Eval/NormalOrder.hs

primer/src/Primer/Eval/Redex.hs

primer/test/Tests/Eval.hs

primer/src/Primer/Eval/Redex.hs

primer/src/Primer/Eval.hs

primer/test/Tests/EvalFull.hs

primer/test/Tests/Eval.hs

georgefst

Looks good!

I'm very relieved that performance is now okay (#736 (comment)). It would have been a shame to have to keep the old version around, given how much is simplified by avoiding non-local substitutions.

This is in preparation for rethinking how we evaluate let bindings. Signed-off-by: Ben Price <[email protected]>

There are a few tests where the upper bound on the number of eval steps to take is fairly tight. Since we will be changing eval a lot shortly and want to be able to see changes to the number of steps taken, we make these tight bounds explicit. Signed-off-by: Ben Price <[email protected]>

Now tasty will report the use site of these helpers, rather than their definition site, when they report an error. Signed-off-by: Ben Price <[email protected]>

This can be seen as an explicit-substitution style operational semantics. This change in approach means that our evaluation rules are much more local, and will enable some future simplifications. In particular we will avoid using the `Accum` machinery, simplify the eval `Cxt` and not have to have a separate eval mode for substitutions. We temporarily disable EvalFull.unit_8 and EvalFull.unit_9. They do pass (note that the step count is bumped), but takes a long time (roughly 20 minutes on my machine!). Similarly, we disable primer-benchmark's "mapEven 10". We also disable (but have not worked out the bounds currently required): Prelude.Integer.tasty_sum_prop Prelude.Integer.tasty_product_prop Prelude.Polymorphism.tasty_map_prop Prelude.Polymorphism.foldr_list_char Prelude.Polymorphism.foldr_bool Prelude.Polymorphism.foldr_right_assoc This will be massively improved shortly, by being more aggressive in eliding pointless `let`s. Some bounds on number of eval steps to take have been temporarily increased on Prelude.Integer.tasty_min_prop Prelude.Integer.tasty_max_prop Prelude.Integer.tasty_abs_prop Prelude.Integer.tasty_odd_prop Prelude.Polymorphism.tasty_const_prop which will also be reverted once we are more aggressive in eliding pointless `let`s. Signed-off-by: Ben Price <[email protected]>

Currently there is a trivial set of options, but shortly we will add some actual optionality here. Signed-off-by: Ben Price <[email protected]>

We often build terms with many adjacent `let`s: let x=... in let y=... in let z=... in f s We now can push all three of these `let` into the application in one step, rather than having to push them one-at-a-time. Note that the evaluation order ensures that (in the old mode) if we take the step of pushing `z`, then the next redex to reduce is pushing `y`, and the next is pushing `x`. Thus this option will not affect evaluation order. This change happens to reduce the required number of steps for Prelude.Integer.tasty_min_prop and Prelude.Integer.tasty_max_prop enough to undo the temporary bump. Signed-off-by: Ben Price <[email protected]>

Signed-off-by: Ben Price <[email protected]>

Before doing this, we would sometimes build up large redundant substitutions, and have to push these down to the leaves before eliding them. This leads to larger terms and extra work. This enables us to reenable unit_8 and unit_9, and primer-benchmark's "mapEven 10" as it gives a major performance increase. Whilst this reduces the number of steps taken for most examples, note that the step limit had to be increased on unit_prim_partial_map, and unit_type_preservation_BETA_regression also took more steps. These are both because of the same phenomenon caused by the interaction with treating adjacent lets as a group, causing more steps to be taken on smaller trees due to early partial elision. Note that the optimisation makes no difference on terms like let x1=_ in ... let xn=_ in xi as `xi` (an occurrence of one of the let-bound variables) is a leaf. The workload in these two tests has many such subterms which get created when pushing lets down. Aggressive elision will remove some of the lets early: for example if there was a term such as let x1=_ in ... let xn=_ in C xi xj then aggressively eliding would remove all but two of the lets (assuming they are independent) as a first step, leaving let xi=_ in let xj=_ in C xi xj but then follow all the steps that the non-aggressive eliding option would take (push all lets under the constructor, elide around the leaf `xi`, inline `xi`, elide around `xj`, inline `xj`). Note that this means that aggressively eliding lets takes an extra step for this pattern. Signed-off-by: Ben Price <[email protected]>

Since we are (optionally) eliding aggressively, we may as well not create the pointless lets in the first place. (Note that we may still create pointless lets when renaming binders.) This again noticably speeds up unit_8 and unit_9. It also speeds up "mapEven 10", tasty_abs_prop, tasty_odd_prop and tasty_const_prop enough to undo their temporary step limit bump; and speeds up tasty_sum_prop, tasty_product_prop, tasty_map_prop, tasty_foldr_list_char, tasty_foldr_bool and tasty_foldr_right_assoc enough to reenable them (these tests take roughly the same time as prior to the change to pushing down lets). Signed-off-by: Ben Price <[email protected]>

The type itself does not change, but now we only record directly-enclosing lets, rather than any enclosing binder. This fixes unit_redexes_lettype_capture, where we want to not consider a buried binder renamable. Signed-off-by: Ben Price <[email protected]>

Now we are pushing down lets, we do not need so much information about bindings. In particular, we do not need to record the original binding location, or the original binding's context, since we do not do long-range substitution where care is needed to avoid capture. Signed-off-by: Ben Price <[email protected]>

This fixes a rare issue that if one has two adjacent lets with the same name, we would only record one of them in the `Cxt`, and thus miscalculate whether a binder they immediately contain needs to be renamed before we can push the lets under. Signed-off-by: Ben Price <[email protected]>

This is because we "push down lets", rather than doing long-range substitutions. This means that all our rules are local, so we do not need two eval modes "normal" and "substitution". Signed-off-by: Ben Price <[email protected]>

brprice changed the base branch from main to brprice/test-merge-eval October 20, 2022 14:38

brprice force-pushed the brprice/test-merge-eval branch 2 times, most recently from 07745ec to f69a401 Compare October 30, 2022 22:01

brprice force-pushed the brprice/test-merge-eval branch from f69a401 to 1f43562 Compare November 16, 2022 13:14

Base automatically changed from brprice/test-merge-eval to main November 16, 2022 14:56

dhess mentioned this pull request Jan 24, 2023

Ensure API calls do not introduce shadowing #559

Merged

brprice force-pushed the brprice/explicit-subst branch 2 times, most recently from f2831da to 5dab56d Compare July 12, 2023 15:06