Fix linting of unused let bindings #1001
Conversation
The removeUnusedBindings rule only matches the first bound variable in a nested let block (of the form "let ... let ... in ..."). This means that so far the linter missed cases like let a = 0 let b = 0 in a. This simple fix unfolds all let blocks (syntactically this means inserting `in's everywhere) before applying the linting rules; the LetInLet rule folds everything back together in the end. Applied to the example from above we now return the correct result, let a = 0 in a.
dhall/src/Dhall/Lint.hs
Outdated
| `mplus` optionalLitToSomeNone e | ||
| ) | ||
| . Dhall.Optics.rewriteOf subExpressions removeUnusedBindings |
There was a problem hiding this comment.
Are you sure that you want to compose rewriteOfs instead of using mplus? The reason I ask is that I believe using mplus ensures that we don't miss newly-exposed opportunities for rewrites.
For example, consider the generic case of:
rewriteOf optic (\e -> f e `mplus` g e)... versus:
rewriteOf optic f . rewriteOf optic gThe latter approach means that if the rewrite named f exposes new opportunities for the rewrite named g, they will be missed, whereas the former approach using mplus would still work because it will keep trying either f or g.
Or, to use regular expression notation, the former approach using mplus is sort of like:
(f + g)*
... whereas the latter approach using function composition of rewriteOf would be like:
f*g*
... which is not equivalent.
There was a problem hiding this comment.
Yea, this is not quite the intention I had when I rewrote the module like this - so it'd be good to clarify if it's essential, or if there is another option.
There was a problem hiding this comment.
Oh wait, I see why they are done sequentially. It's because unfoldNestedLets is the opposite of removeLetInLet
Is there any way to do this that doesn't require the unfoldNestedLets preprocessing pass?
There was a problem hiding this comment.
Yes. In fact I tried a direct fix first, i.e. modifying removeUnusedBindings to walk through all binders in a let block. But that turned out to get really quite complicated...
I think this is by far the cleanest solution (and time complexity wise the unfolding/folding is no more than a constant factor). One thing that I might try is rewriting lint in a more explicit fashion, with comments at each step – the point-free style is a bit hard to read.
There was a problem hiding this comment.
Alright, then we'll keep it the way you have it
| @@ -3,9 +3,6 @@ | |||
| module Dhall.Lint | |||
| ( -- * Lint | |||
| lint | |||
| , removeLetInLet | |||
| , removeUnusedBindings | |||
| , optionalLitToSomeNone | |||
There was a problem hiding this comment.
Given as the semantics of the remove* rules are a bit tricky currently I don't feel too comfortable exporting them... Shouldn't lint be enough?
There was a problem hiding this comment.
Right, originally I intended them to be exported so we could test independent passes in unit tests. E.g., does optionalLitToSomeNone do the right thing? We can test that by just using lint, but it's harder to isolate what's gone wrong. However, I didn't really anticipate the interaction between the phases!
There was a problem hiding this comment.
Good point about testing. In my opinion that shouldn't be a problem at the moment, but we might want to revisit that if the linter ever gets more complicated.
Previously we had "x@0" `freeIn` "x@1" == True (but "x@1" `freeIn` "x@0" == False). The fix is to use subst instead of shift to change occurrences of the given variable.
Whenever we remove an unused binding we need to update any references to variables outside the let block, so that let a = 0 let a = 0 in a@1 gets correctly rewritten into let a = 0 in a (a = a@0) instead of let a = 0 let a = 0 in a@1 ~> let a = 0 in a@1 ~> a@1
Find unused bindings inside nested lets
Fixes cases likelet a = 0 let b = 0 in a, that didn't get correctly linted (whereaslet a = 0 in let b = 0 in awould).Fix
Fixes Core.Dhall.freeIn -- previouslyfreeInto correctly handle de Briujn indicesfreeIn "x@0" "x@1"; as a result, the linter did not notice cases likelet a = 0 in let a = 0 in a@1.Fix
FixesremoveUnusedBindingsto update de Bruijn indicesremoveUnusedBindingsto correctly update any affected de Bruijn indices.