Row Polymorphism and First-class Matches Seminars/Workshops

Abstract

I will present an early report on a variant of the ML programming language with row polymorphism for both record and sum types. The main innovation of this language is its use of a new type constructor which acts as an alternative form of the function arrow. Values of the alternative function type are called "matches", and the familiar CASE construct acts as the type's elimination form. The expressive power of matches stems from their status as first-class values combined with the availability of operations that functionally extend, modify, or narrow them.

The combination of these new features together with a restricted form of equi-recursion at the type level as well as Hindley-Milner type inference (based on the existence of principal types) turns out to be quite powerful. It gives rise to a simple and natural encoding of certain forms of type refinement and also enables a very simple programming pattern for a principled attack on the so-called "expression problem".

Despite its expressive power, the language has an efficient implementation strategy based on techniques pioneered by Ohori and later refined by Gaster and Jones. We have constructed a native code compiler, compiling to the PowerPC architecture. Time permitting I will briefly discuss some of the techniques used in this compiler.

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