Re: Summary: type inference

Jens Palsberg <palsberg@daimi.aau.dk> wrote:
> Appended is a summary of the replies I have received.  
> [...]

The following reference may be added to the list given by Jens.



	, AUTHOR = {Jacques Garrigue and Hassan A\"{\i}t-Kaci}
	, TITLE = {The Typed Polymorphic Label-Selective $\lambda$-Calculus}
	, BOOKTITLE = {Proceedings of the 21st ACM Symposium on Principles
		of Programming Languages}
	, YEAR = {1994}
	, PAGES = {35--47}
	, ADDRESS = {New York, NY}
	, MONTH = {January}
	, ABSTRACT = {Formal calculi of 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.  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
	obviating 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.}