A Pronominal Approach to Binding and Computation

Abstract

There has been a great deal of research on programming languages for computing with binding and scope (bound variables, α-equivalence, capture-avoiding substitution). These languages are useful for a variety of tasks, such as implementing domain-specific languages and formalizing the metatheory of programming languages. Functional programming with binding and scope involves two different notions of function: functions-as-data and functions-as-computation. Functions-as-data, used to represent abstract syntax with variable binding, have an intensional, syntactic, character, in the sense that they can be inspected in ways other than function application. For example, many algorithms that process abstract syntax recur under binders, treating variables symbolically. On the other hand, functions-as-computation, the usual functions of functional programming, have an extensional character—a function from A to B is a black box that, when given an A, delivers a B.