Type safe incremental rebinding

摘要

We extend the simply-typed lambda-calculus with a mechanism for dynamic and incrementalrnrebinding of code. Fragments of open code which can be dynamically rebound are values.rnDifferently from standard static binding, which is done on a positional basis, rebinding isrndone on a nominal basis, that is, free variables in open code are associated with names whichrndo not obey α-equivalence. Moreover, rebinding is incremental, that is, just a subset of namesrncan be rebound, making possible code specialization, and rebinding can even introduce newrnnames. Finally, rebindings, which are associations between names and terms, are first-classrnvalues, and can be manipulated by operators such as overriding and renaming. We define arntype system in which the type for a rebinding, in addition to specify an association betweenrnnames and types (similarly to record types), is also annotated. The annotation says whetherrnor not the domain of the rebinding having this type may contain more names than the onesrnthat are specified in the type. We show soundness of the type system.