undefined | Better HN

0 pointsnmadden1y ago0 comments

The example given in the article is:

    counter = 0
    counter = counter + 1

This is very different to shadowing where there is a clear scope to the rebinding. In this case, I cannot employ equational reasoning within a scope but must instead trace back through every intervening statement in the scope to check whether the variable is rebound.

0 comments

4 comments · 2 top-level

tonyg1y ago· 1 in thread

It's a straightforward syntactic transformation. The two are equivalent. The scope of the rebound variable begins at the rebinding and ends when the surrounding scope ends. Perfectly clear - the only difference is a "let" keyword.

  counter = 0
  ...
  counter = counter + 1
  ...

  let counter = 0 in
  ...
  let counter = counter + 1 in
  ...

nmaddenOP1y ago

The ellipses in your straightforward transformation are doing some heavy lifting there. Typically the let…in construct has some way to indicate where the scope of the “in” part ends: indentation (Haskell), explicit “end” marker (SML) etc. Even with that, shadowing does make equational reasoning harder (you have to look at more surrounding context) and should generally be avoided.

xavxav1y ago· 1 in thread

Sure, scopes are not as easily syntactically visible, but each assignment is creating a new scope, that doesn't change anything for equational reasoning which has to account for captures / substitutions anyways.

nmaddenOP1y ago

> each assignment is creating a new scope

No, it’s rebinding the variable within the same scope. Even if you view it as implicitly creating a new scope, the implicit part means it can happen on any line so you have to scan them all and mentally keep track of what changes where, (almost) exactly as you would for imperative code.

j / k navigate · click thread line to collapse