We present a simple extension of typed lambda-calculus where functions can be overloaded by putting different ''banches of codes'' together. When the function is applied, the branch to execute is chosen according to a particular selection rule which depends on the type of the argument. The crucial feature of the present approach is that the branch selection depends on the ''run-time type'' of the argument, which may differ from its compile-time type, because of the existence of a subtyping relation among types. Hence overloading cannot be eliminated by a static analysis of code, but it is an essential feature to be dealt with during computation. We obtain in this way a type-dependent calculus, which differs from the various lambda-calculi where types to not play any role during computation. We prove confluence and a generalized subject-reduction theorem for this calculus. We prove strong normalization for a ''stratified'' subcalculus. The definition of this calculus is guided by the understanding of object-oriented features and the connections between our calculus and object-orientedness are extensive stressed. We show that this calculus provides a foundation for types object-oriented languages which solves some of the problems of the standard record-based approach.

A Calculus for Overloaded Functions with Subtyping

GHELLI, GIORGIO;
1995

Abstract

We present a simple extension of typed lambda-calculus where functions can be overloaded by putting different ''banches of codes'' together. When the function is applied, the branch to execute is chosen according to a particular selection rule which depends on the type of the argument. The crucial feature of the present approach is that the branch selection depends on the ''run-time type'' of the argument, which may differ from its compile-time type, because of the existence of a subtyping relation among types. Hence overloading cannot be eliminated by a static analysis of code, but it is an essential feature to be dealt with during computation. We obtain in this way a type-dependent calculus, which differs from the various lambda-calculi where types to not play any role during computation. We prove confluence and a generalized subject-reduction theorem for this calculus. We prove strong normalization for a ''stratified'' subcalculus. The definition of this calculus is guided by the understanding of object-oriented features and the connections between our calculus and object-orientedness are extensive stressed. We show that this calculus provides a foundation for types object-oriented languages which solves some of the problems of the standard record-based approach.
Castagna, G.; Ghelli, Giorgio; Longo, G.
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/11568/25968
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 68
  • ???jsp.display-item.citation.isi??? 43
social impact