## 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]