A calculus for overloaded functions with subtyping
Giuseppe Castagna, Giorgio Ghelli, Giuseppe O. Longo · 1992
We present a simple extension of typed λ-claculus where functions can be overloaded by adding different “pieces of code”. In short, the code of an overloaded function is formed by several branches of code; the branch to execute is chosen, when the function is applied, according to a particular selection rule which depends on the type of the argument. The crucial feature of the present approach is that a subtyping relation is defied among types, such that the type of a term generally decreases during computation, and this fact induces a distinction between the “compile-time” type and the “run-time”type of a term. We study the case of overloaded functions where the branch selection depends on the run-time type of the argument, so that overloading cannot be eliminated by a static analysis of code, but is an essential feature to be dealt with during computation. We prove Confluence and Strong Normalization for this calculus as well as a generalized Subject-Reduction theorem (but proofs are ommitted in this abstract.