Records, sums, cases, and exceptions: Row-polymorphism at work

I will present the design of a programming language (called MLPolyR) whose type system makes significant use of row polymorphism (Rémy, 1991). MLPolyR (Blume et al. 2006) is a dialect of ML and provides extensible records as well as their exact dual, polymorphic sums with extensible first-class cases.

As I will demonstrate, first-class extensible cases enable code written in a certain style to be re-used in the context of “wider” types (sum types with more variants) than originally anticipated. This flexibility is similar to the way class-based object-oriented code can be extended by subclassing – without, however, giving up on extensibility in the dimension of “functionality” (“adding methods” in object-oriented parlor). I will argue that, taken together, these properties amount to one possible solution to the so-called “expression problem” (Wadler, 1998).

Furthermore, the resulting type system still admits sound and complete Damas-Milner-style type inference. In fact, like Ohori’s SML# (Ohori, 1995) it improves on SML’s type inference. (In SML, there is no principal type for projection from records, leading to the occasional need for programmer-supplied type annotations.)

I will briefly explain the underpinnings of an efficient translation scheme into low-level code. It is based on a variant of Ohori’s “index-passing” and on a consequent exploitation of the duality between products (records) and sums (unions). This translation mechanism is used in my prototype compiler. The compiler targets the PowerPC architecture and is used (in simplified form) as the basis for a course on compiler construction.

I will wrap up by showing how to account for exceptions and exception handling in a type system with row polymorphism, leading to a language design that retains the flexibility of higher-order functional programming, that can still be implemented efficiently using the same technology as above, and for which we can boldly claim: “Well typed programs do not have uncaught exceptions.”

(This is joint work with my student Wonseok Chae and with my colleague Umut Acar.)