FreshML: Programming with Binders Made Simple (Abstract)
FreshML extends ML with elegant and practical constructs for
declaring and manipulating syntactical data involving
statically scoped binding operations. User-declared FreshML
datatypes involving binders are concrete, in the sense that values
of these types can be deconstructed by matching against patterns
naming bound variables explicitly. This may have the computational
effect of swapping bound names with freshly generated ones; previous
work on FreshML used a complicated static type system inferring
information about the "freshness" of names for expressions in order
to tame this effect. The main contribution of this paper is to show
(perhaps surprisingly) that a standard type system without freshness
inference, coupled with a conventional treatment of fresh name
generation, suffices for FreshML's crucial correctness property that
values of datatypes involving binders are operationally equivalent
if and only if they represent alpha-equivalent pieces of
object-level syntax. This is established via a novel denotational
semantics. FreshML without static freshness inference is no more
impure than ML and experience with it shows that it supports a
programming style pleasingly close to informal practice when it
comes to dealing with object-level syntax modulo alpha-equivalence.