Programming with Implicit Values, Functions, and Control (or, Implicit Functions: Dynamic Binding with Lexical Scoping)

We introduce two new language features, called implicit functions and implicit control. Both generalize implicit values (or parameters) which are a typed implementation of dynamic binding. Implicit functions are bound dynamically but evaluated in the lexical scope of their binding. We show how this small generalization from regular implicit values leads to better abstraction. In particular, implicit functions encapsulate (side) effects at the definition site, as opposed to leaking them to the call site. Implicit control further generalizes implicit functions by adding the ability to return into the lexical scope of the binding or to resume to the call-site. We formalize the new features as an extension to Moreau’s calculus of dynamic binding (1998). Unifying all three language features in one framework guarantees that the interaction between implicit values, functions, and control is well-defined. We also show how our semantics correspond to a macro-translation into algebraic effect handlers.