Type Inference: Some Results, Some Problems¹

Article type: Research Article

Authors: Giannini, Paola^a | Honsell, Furio^b | Ronchi Della Rocca, Simona^a

Affiliations: [a] Università degli Studi di Torino, Dipartimento di Informatica, Corso Svizzera 185, 10149 Torino, Italy | [b] Università degli Studi di Udine, Dipartimento di Matematica e Informatica, via Zanon 6, Udine, Italy

Note: [1] Work supported by: ESPRIT BRA 3252 “Logical Framework”; WG BRA 3230 “Common Foundation of Functional and Logic Programming”; MURST 60% 1991 “Metodi Logici per Analisi di Proprieta’ di Programmi Funzionali e Logici”; MURST 40% 1991 “Modelli della Computazione e dci Linguaggi di Programmazione”.

Abstract: In this paper we investigate the type inference problem for a large class of type assignment systems for the λ-calculus. This is the problem of determining if a term has a type in a given system. We discuss, in particular, a collection of type assignment systems which correspond to the typed systems of Barendregt’s “cube”. Type dependencies being shown redundant, we focus on the strongest of all, Fω, the type assignment version of the system Fω of Girard. In order to manipulate uniformly type inferences we give a syntax directed presentation of Fω and introduce the notions of scheme and of principal type scheme. Making essential use of them, we succeed in reducing the type inference problem for Fω to a restriction of the higher order semi-unification problem and in showing that the conditional type inference problem for Fω is undecidable. Throughout the paper we call attention to open problems and formulate some conjectures.

DOI: 10.3233/FI-1993-191-205

Journal: Fundamenta Informaticae, vol. 19, no. 1-2, pp. 87-125, 1993