A second look at polymorphic records

Martin Sulzmann

Keywords:

Hindley/Milner type system, type inference, principal types, program analysis, dimension types, binding-time analysis, equational theories, label selective and type selective lambda calculus and of course HM(X) and polymorphic field labels

Summary:

In this (informal) talk I'll cover a couple of subjects I'm currently working on. I'll cover theoretical as also asmore practical topics. I'll discuss some program analysis stuff like dimension types and binding-time analysis. Then, I'll show that unitary unification (that means we have mgu's) is sufficient to compute principal types. The trick is that we perform a kind of lazy unification in contrast to strict normalization in the common type inference algorithm W. That's why laziness beats strictness! This extends some results not previously known.

Then I'll switch to the label-selective and type-selective lambda calculus. The basic idea is as follows. We assume that we can label function arguments. When we do curried function application we can switch the order of the arguments. Furthermore, it is also possible to specify default values. As an example consider the exponentiation function.

  exp x (y:exp | 2) = y^x

Then

  exp 2 3:exp and exp 3:exp 2 yield the same result and
  exp n simply yields 2^n

I introduce the type selective lambda calculus. To my knowledge this calculus has not previously been published in the literature before. The idea behind the type selective calculus is similar. But instead of using labels to select the arguments we use the type of the arguments itself as a selection criteria. We require that the arguments types of a function are unambigous to allow an unordered, curried function application. For instance, consider the fold function

fold :: (a->b->a)->[b]->a->a

The arguments types a->b->a, [b] and a are unambigous. Therefore, we can apply these arguments in any order. That's cool, or? It turns out that we even can combine the label- and type selective calculus.

Here are some more details:

In the first part I'll finish up some stuff about dimension types. We consider the type inference problem for dimension types. We know that unfication is unitary (that means we have mgu's) for dimension types. But the common type inference algorithm W is not complete in case of dimension types. I'll show an example (due to A.J. Kennedy) where we can see why algorithm W does not compute principal types. This counter example relies on the fact that dimension types form a non--regular theory. A.J. Kennedy gives an improved algorithm W'. Under sufficient condition on the non-regular theory (Well, for regular theories, algorithm W does the job) algorithm W' computes principal types. It turns out that it is possible to generalize this result. I'll show that there is a method to compute principal types even for non-regular theories. (Of course, we require that we have mgu's). The method is based on a trick which we can play in the HM(X) framework.

I'll show that the label- and type-selective calculus can be encoded in terms of an HM(X) application. It turns out that polymorphic field labels do the job. I'll discuss some issues like type inference, complexity results, compilation calculus (!?),...

And then ... ?

[And then we'll be thrown out of room 200 for going on too long -- John]