System F-less than or equal to is an extension of second-order typed lambda calculus, where a subtype hierarchy among types is defined, and bounded second-order lambda abstraction is allowed. This language is a basis for much of the current research on integration of typed functional languages with subtypes and inheritance. An algorithm to perform type checking for F-less than or equal to expressions has been known since the language Fun was defined. The algorithm has been proved complete, by the author acid Curien, which means that it is a semi-decision procedure for the type-checking problem. In this paper we show that this algorithm is not a decision procedure, by exhibiting a term which makes it diverge. This result was the basis of Pierce's proof of undecidability of typing for F-less than or equal to. We study the behavior of the algorithm to show that our diverging judgement is in some sense contained in any judgement which makes the algorithm diverge. On the basis of this result, and of other results in the paper, we claim that the chances that the algorithm will loop while type-checking a ''real program'' are negligible. Hence, the undecidability of F-less than or equal to type-checking should not be considered as a reason to prevent the adoption of F-less than or equal to as a basis For defining programming languages of practical interest. Finally, we show the undecidability of an important subsystem of F-less than or equal to.

Divergence of Fsub type checking

GHELLI, GIORGIO
1995

Abstract

System F-less than or equal to is an extension of second-order typed lambda calculus, where a subtype hierarchy among types is defined, and bounded second-order lambda abstraction is allowed. This language is a basis for much of the current research on integration of typed functional languages with subtypes and inheritance. An algorithm to perform type checking for F-less than or equal to expressions has been known since the language Fun was defined. The algorithm has been proved complete, by the author acid Curien, which means that it is a semi-decision procedure for the type-checking problem. In this paper we show that this algorithm is not a decision procedure, by exhibiting a term which makes it diverge. This result was the basis of Pierce's proof of undecidability of typing for F-less than or equal to. We study the behavior of the algorithm to show that our diverging judgement is in some sense contained in any judgement which makes the algorithm diverge. On the basis of this result, and of other results in the paper, we claim that the chances that the algorithm will loop while type-checking a ''real program'' are negligible. Hence, the undecidability of F-less than or equal to type-checking should not be considered as a reason to prevent the adoption of F-less than or equal to as a basis For defining programming languages of practical interest. Finally, we show the undecidability of an important subsystem of F-less than or equal to.
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/25431
 Attenzione

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

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 13
  • ???jsp.display-item.citation.isi??? 9
social impact