Generative Unbinding of Names
This paper is concerned with a programming language construct for
typed name binding that enforces α-equivalence. It proves a
new result about what operations on names can co-exist with this
construct. The particular form of typed name binding studied is
that used by the FreshML family of languages. Its characteristic
feature is that a name binding is represented by an abstract
(name,value)-pair that may only be deconstructed via the generation
of fresh bound names. In FreshML the only observation one can make
of names is to test whether or not they are equal. This restricted
amount of observation was thought necessary to ensure that there is
no observable difference between α-equivalent name binders.
Yet from an algorithmic point of view it would be desirable to allow
other operations and relations on names, such as a total ordering.
This paper shows that, contrary to expectations, one may add not
just ordering, but almost any relation or numerical function on
names without disturbing the fundamental correctness result about
this form of typed name binding (that object-level
α-equivalence precisely corresponds to contextual equivalence
at the programming meta-level), so long as one takes the state of
dynamically created names into account.