FreshML: programming with binders made simple

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 -equivalent pieces of object-level syntax. This ...

• Type: Conference
• Year: 2003
• Where: ICFP
• Authors: Mark R. Shinwell, Andrew M. Pitts, Murdoch Gabbay
• Keywords: Datatypes Involving Binders, ICFP 2003, Programming Languages, Static Freshness Inference