CST Part II 2013/14 Project Suggestion from Andrew Pitts

FreshML Implementation in OCaml

A project on this topic would suit someone with an interest in functional programming and programming language semantics.

Background:

FreshML [1] is an experimental, ML-like language designed to facilitate metaprogramming, that is, writing programs that operate on data that are syntactical structures in some language (called the object-language, to distinguish from the meta-language, FreshML). The object-language might for example be a logic and the meta-program part of some theorem-proving system for object-language theorems; or it might be a programming language and the meta-program might be a type-checker, a compiler, or an interpreter for object-language programs. The features that FreshML adds to ML are supposed to make it easy to deal with object-languages that feature names and name-binding constructs and where the object-language expressions are to be identified up to α-equivalence, that is, consistent renaming of bound names. In FreshML, the user gets to write functions manipulating bound names using name-abstraction patterns, but the semantics of FreshML guarantees (provably) that those functions cannot violate α-equivalence. Chapter 10 of [2] (available on request from AMP) provides more details. At the moment the only implementation of these ideas is in Fresh OCaml [3], which patches the back end of an old version of OCaml (v3.10) to provide run-time values with swappable names (the essential feature needed for FreshML); it is not maintained and is only known to compile successfully on current Linux systems, but not current Mac OSX or Windows/Cygwin systems. Examples of Fresh Ocaml programs are here.

A project on this topic could:

1. Define the syntax and operational semantics for a language with the key features of FreshML: higher-order functions (recursively defined and using various kinds of patterns) on user-declared data types featuring signle-name abstraction types for as many types of name as the user cares to declare. The operational semantics should be a small-step, environment-style abstract machine, rather than a big-step evaluation relation as in [1]. There is scope to experiment with using values that have some kind of suspended name-permutations in order to make swappable names more efficient. Optional extras: type variables and ML-style polymorphism; the generalised form of name abstraction implemented by Fresh OCaml (and described in section 4.6 of [2]).
2. Develop an implementation of the language defined in step 1, written in OCaml using only standard features and capable of being compiled under Linux, Mac OSX, or Windows/Cygwin. The implementation should include a parser, type-checker and interpreter that can be run either from an interactive top-level loop or on files from the command line. Optional extra: adapt the Tuareg emacs-mode for OCaml to be usable for this language.

Success criteria:

• Ability to run (correctly!) existing Fresh OCaml example programs (featuring generalised name abstraction, if that is implemented).
• Modular, well-documented OCaml code that can be used by others for future experiments with languages that extend FreshML.
• Clarity and simplicity is to be favoured over complexity; nevertheless it would be good to demonstrate (only by example, not by proof) that the operational semantics and implementation deal with swappable names more efficiently than does Fresh OCaml.

References:

[1] M. R. Shinwell, A. M. Pitts and M.J.Gabbay, FreshML: Programming with Binders Made Simple. In Eighth ACM SIGPLAN International Conference on Functional Programming (ICFP 2003), Uppsala, Sweden, pages 263-274 (ACM Press, 2003). [pdf]

[2] A. M. Pitts, Nominal Sets: Names and Symmetry in Computer Science, Cambridge Tracts in Theoretical Computer Science, vol. 57 (CUP, 2013)

[3] M. R. Shinwell and A. M. Pitts, Fresh Objective Caml User Manual, University of Cambridge Computer Laboratory Technical Report UCAM-CL-TR-621, February 2005. [pdf].