The Typed Polymorphic Label-Selective Lambda-Calculus

Abstract. Formal calculi on record structures have recently been a focus of active research. However, scarcely anyone has studied formally the dual notion - i.e. argument-passing to functions by keywords, and its harmonization with currying. We have.

Recently, we introduced the label-selective lambda-calculus, a conservative extension of lambda-calculus that uses a labeling of abstractions and applications to perform unordered currying. In other words, it enables some form of commutation between arguments. This improves program legibility, thanks to the presence of labels, and efficiency, thanks to argument commuting.

In this paper, we propose a simply typed version of the calculus, then extend it to one with ML-like polymorphic types. For the latter calculus, we establish the existence of principal types and we give an algorithm to compute them. Thanks to the fact that label-selective lambda-calculus is a conservative extension of lambda-calculus by adding numeric labels to stand for argument positions, its polymorphic typing provides us with a keyword argument-passing extension of ML abviating the need of records. In this context, conventional ML syntax can be seen as a restriction of the more general keyword-oriented syntax limited to using only implicit positions instead of keywords.