WG211/M10Shan

Computational Effects across Generated Binders, Part 2: Enforcing lexical scope by Chung-chieh Shan (presenter) with Yukiyoshi Kameyama and Oleg Kiselyov

If left unchecked, side effects in code generators often interact with
generated binders badly to produce unexpectedly unbound variables, or
worse, unexpectedly bound ones. The literature and our experience is
rife with examples of these surprises, where variables with different
scopes are mixed up. To prevent such surprises while still allowing
arbitrary side effects to move open code past generated binders, we
first define a notion of lexical scope for generated code with explicit
contexts. To each generated binder, we attach a unique label that is
checked against each use occurrence of the bound variable. We then
introduce a static type system to assure that these checks will succeed.

We embedded this type system in a Haskell library. We used this library
to implement statically safe let-insertion across an arbitrary number of
binders for the first time.