Department of Computer Science and Technology

Technical reports

Names and higher-order functions

Ian Stark

April 1995, 140 pages

This technical report is based on a dissertation submitted December 1994 by the author for the degree of Doctor of Philosophy to the University of Cambridge, Queens’ College.

DOI: 10.48456/tr-363

Abstract

Many functional programming languages rely on the elimination of ‘impure’ features: assignment to variables, exceptions and even input/output. But some of these are genuinely useful, and it is of real interest to establish how they can be reintroducted in a controlled way. This dissertation looks in detail at one example of this: the addition to a functional language of dynamically generated “names”. Names are created fresh, they can be compared with each other and passed around, but that is all. As a very basic example of “state”, they capture the graduation between private and public, local and global, by their interaction with higher-order functions.

The vehicle for this study is the “nu-calculus”, an extension of the simply-typed lambda-calculus. The nu-calculus is equivalent to a certain fragment of Standard ML, omitting side-effects, exceptions, datatypes and recursion. Even without all these features, the interaction of name creation with higher-order functions can be complex and subtle.

Various operational and denotational methods for reasoning about the nu-calculus are developed. These include a computational metalanguage in the style of Moggi, which distinguishes in the type system between values and computations. This leads to categorical models that use a strong monad, and examples are devised based on functor categories.

The idea of “logical relations” is used to derive powerful reasoning methods that capture some of the distinction between private and public names. These techniques are shown to be complete for establishing contextual equivalence between first-order expressions; they are also used to construct a correspondingly abstract categorical model.

All the work with the nu-calculus extends cleanly to Reduced ML, a larger language that introduces integer references: mutable storage cells that are dynamically allocated. It turns out that the step up is quite simple, and both the computational metalanguage and the sample categorical models can be reused.

Full text

PS (0.3 MB)
DVI (0.2 MB)

BibTeX record

@TechReport{UCAM-CL-TR-363,
  author =	 {Stark, Ian},
  title = 	 {{Names and higher-order functions}},
  year = 	 1995,
  month = 	 apr,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-363.ps.gz},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-363},
  number = 	 {UCAM-CL-TR-363}
}