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

Date

April 30, 2007

Speaker

Matthias Blume

Affiliation

Toyota Technological Institute at Chicago

Overview

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.)

Speakers

Matthias Blume

Matthias Blume is currently an Assistant Professor of Computer Science at the Toyota Technological Institute at Chicago (TTI-C). He holds an undergraduate degree in Mathematics from Humboldt-Universität zu Berlin, an MA in Computer Science from Princeton University, and a Ph.D. in Computer Science, also from Princeton University. He has held post-doctoral positions at Princeton University and Kyoto University. Before assuming his current position at TTI-C he spent two years as a Member of Technical Staff at Lucent Technologies, Bell Laboratories.Matthias is active in the Programming Language research community. He has worked on compilation management (resulting in CM, the compilation manager for Standard ML of New Jersey), compiler optimization (with A. Appel), foreign-function interfaces, design and implementation of domain-specific languages for unusual hardware, e.g., network processors (with L. George), semantics of contracts (with D. McAllester, R. Findler, and M. Felleisen), semantics and implementation of self-adjusting computation (with U. Acar, G. Blelloch, R. Harper, K. Tangwongsan, and J. Donham), type inference in the presence of modules (with D. Dreyer), and row-polymorphism in language design (with W. Chae and U. Acar).

People