[Prev][Next][Index][Thread]
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.
Best,
-hak
@INPROCEEDINGS{garrigue:ait-kaci:94
, 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}
, ORGANIZATION = {ACM}
, PUBLISHER = {ACM}
, 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.}
}