Probably. But in these languages, variable declaration is also an lambda/application : let x = t1 in t2 <=> (λx.t2) t1 So, it behaves in a sane way

Probably. But in these languages, variable declaration is also an lambda/application : let x = t1 in t2 <=> (λx.t2) t1 So, it behaves in a sane way (you have lexical scoping for local variables too). There is no "functional scope".