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^xThen
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->aThe 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]