A direct algorithm for the type interference in the rank 2 fragment of the second--order λ-Calculus
Files
Main Report
Date
1993-12-01
DOI
Authors
Kfoury, A.J.
Wells, J.B.
Version
OA Version
Citation
Wells, Joe. "A Direct Algorithm for Type Inference in the Rank 2 Fragment of the Second-Order Lambda-Calculus", Technical Report BUCS-1993-017, Computer Science Department, Boston University, November 1993. [Available from: http://hdl.handle.net/2144/1475]
Abstract
We study the problem of type inference for a family of polymorphic type disciplines containing the power of Core-ML. This family comprises all levels of the stratification of the second-order lambda-calculus by "rank" of types. We show that typability is an undecidable problem at every rank k ≥ 3 of this stratification. While it was already known that typability is decidable at rank ≤ 2, no direct and easy-to-implement algorithm was available. To design such an algorithm, we develop a new notion of reduction and show how to use it to reduce the problem of typability at rank 2 to the problem of acyclic semi-unification. A by-product of our analysis is the publication of a simple solution procedure for acyclic semi-unification.