A calculus for overloaded functions with subtyping by Castanga et al., SIGPLAN Lisp Pointers 1992

[fikovnik]

A Calculus for Overloaded Functions with Subtyping

Giuseppe Castagna, Giorgio Ghelli, Giuseppe Longo

ACM SIGPLAN Lisp Pointers 1992

PDF

Abstract

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.
The definition of this calculus is driven by the understanding of object-oriented features and the connections between our calculus and object-orientedness are extensively stressed. We show that this calculus provides a foundation for typed object-oriented languages which solves some of the problems of the standard record-based approach. It also provides a type-discipline for a relevant fragment of the “core framework” of CLOS.

Why are you interested in it or why should it be a good idea

I got interested in types and recently in types in OOP.
I think this is a digastable paper.
Also, to continue the typing theme.