%0 Conference Proceedings
%F henglein91a
%A Henglein, Fritz
%T Efficient Type Inference for Higher-Order Binding-Time Analysis
%B Proc. Conf. on Functional Programming Languages and Computer Architecture (FPCA), Cambridge, Massachusetts
%P 448-472
%X Binding-time analysis determines when variables and expressions in a program can be bound to their values, distinguishing between early (compile-time) and late (run-time) binding. Binding-time information can be used by compilers to produce more efficient target programs by partially evaluating programs at compile-time. Binding-time analysis has been for- mulated in abstract interpretation contexts and more recently in a type-theoretic setting. In a type-theoretic setting binding-time analysis is a type inference prob- lem: the problem of inferring a completion of a λ-term e with binding-time annotations such that e satisfies the typing rules. Nielson and Nielson and Schmidt have shown that every simply typed λ-term has a unique comple- tion e that minimizes late binding in TML, a monomorphic type system with explicit binding-time annotations, and they present exponential time algorithms for computing such minimal completions. Gomard proves the same results for a variant of his two-level λ-calculus without a so-called ``lifting'' rule. He presents another algorithm for inferring completions in this somewhat restricted type system and states that it can be implemented in time O(n^3 ). He conjectures that the completions computed are minimal. In this paper we expand and improve on Gomard's work in the following ways. * We identify the combinatorial core of type inference for binding-time analysis in Gomard's type system with ``lifting'' by effectively charac- terizing it as solving a specific class of constraints on type expressions. * We present normalizing transformations on these constraints that preserve their solution sets, and we use the resultant normal forms to prove constructively the existence of minimal solutions, which yield minimal completions; this sharpens the minimal completion result of Gomard and extends it to the full type system with ``lifting''. * We devise a very efficient algorithm for computing minimal comple- tions. It is a refinement of a fast unification algorithm, and an amor- tization argument shows that a fast union/find-based implementation executes in almost-linear time, O(nα(n, n)), where α is an inverse of Ackermann's function. Our results are for the two-level type system of Gomard, but we believe they are also adaptable to the Nielsons' TML. Our algorithm improves the computational complexity of computing minimal completions from expo- nential time to almost-linear time. It also improves on Gomard's polyno- mial time completion algorithm by a quadratic factor and as such appears to be the first efficient algorithm that provably computes minimal comple- tions
%U http://www.diku.dk/hjemmesider/ansatte/henglein/papers/henglein1991b.pdf
%8 August
%D 1991
%K dyntyp
%K parametricity