Nesting let expressions may reveal potential bugs

[gregr]

Hi, Ilya, thanks for sc-mini! I just finished reading the paper and the source, and noticed some things that didn't make sense to me, which may be unintended. By the way, this issue probably isn't a big deal since let expressions don't seem intended for use in the source language, and so won't appear in nested positions.

I noticed a few places where the handling of let expressions would cause problems if they appeared in nested positions (currently, they are only placed in outer positions during decomposition).

Based on how it's used, vnames should be extracting free variables, so should subtract the let parameter from the names retrieved from the body:

sc-mini/DataUtil.hs

Line 56 in 71388c1

vnames' (Let (_, e1) e2) = vnames' e1 ++ vnames' e2

I don't think you really want to substitute v' for v in e2' here, since v could legitimately be free in e2'. You really want the behavior you'd get from first substituting the argument for the let-bound parameter in both e2 and e2', then computing the renaming. A more efficient way of getting this would be to prime the renaming with [(v, v')] to ensure that other occurrences of v on the left, indicating that renaming v to anything else should fail; then removing this renaming since v is not actually a free variable in e2:

sc-mini/DataUtil.hs

Line 77 in 71388c1

renaming' (Let (v, e1) e2, Let (v', e1') e2') = renaming' (e1, e1') ++ renaming' (e2, e2' // [(v, Var v')])

[ilya-klyuchnikov]

Hi Greg, thanks for pointing to this subtlety. Yes, in general case such treatment of let expressions is incorrect (if they were allowed in the source language). But they are introduced only during generalization and hold following properties: - No nested let expressions are introduced in sc-mini. - For every new let expression `let v = .. in ...` the variable `v` is a globally unique variable (taken from the name supply). So, bearing in mind the mentioned properties of let expressions, this simple treatment of let expressions is correct. Feel free to correct me if I am missing something.

…

On Thu, Sep 14, 2017 at 10:44 PM, Greg Rosenblatt ***@***.***> wrote: Hi, Ilya, thanks for sc-mini! I just finished reading the paper and the source, and noticed some things that didn't make sense to me, which may be unintended. By the way, this issue probably isn't a big deal since let expressions don't seem intended for use in the source language, and so won't appear in nested positions. I noticed a few places where the handling of let expressions would cause problems if they appeared in nested positions (currently, they are only placed in outer positions during decomposition). Based on how it's used, vnames should be extracting free variables, so should subtract the let parameter from the names retrieved from the body: https://github.com/ilya-klyuchnikov/sc-mini/blob/ 71388c1/DataUtil.hs#L56 I don't think you really want to substitute v' for v in e2' here, since v could legitimately be free in e2'. You really want the behavior you'd get from first substituting the argument for the let-bound parameter in both e2 and e2', then computing the renaming. A more efficient way of getting this would be to prime the renaming with [(v, v')] to ensure that other occurrences of v on the left, indicating that renaming v to anything else should fail; then removing this renaming since v is not actually a free variable in e2: https://github.com/ilya-klyuchnikov/sc-mini/blob/pfp/DataUtil.hs#L77 — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#10>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AAQrHJFWc4EqFF4ry4qdFTUlM3s4unMLks5siZ4qgaJpZM4PYOOP> .

[gregr]

Nope, that's it. Since it's fresh in my mind, just wanted to point out a few of the more subtle places that, if fixed (along with other less subtle changes), could make it possible to include let expressions in the source language too. It's the kind of code where, if you revisit it after several years, it might be hard to remember where things could go wrong.