Jump to : Download | Abstract | See also | Keywords | Contact | BibTex reference | EndNote reference |


Fritz Henglein. Efficient Type Inference for Higher-Order Binding-Time Analysis. In Proc. Conf. on Functional Programming Languages and Computer Architecture (FPCA), Cambridge, Massachusetts, Pages 448-472, August 1991.


Download paper: Adobe portable document (pdf) pdf

Copyright notice:This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.


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

See also

[ fpca91 ]


[ Dyntyp ] [ Parametricity ]


Fritz Henglein

BibTex Reference

   Author = {Henglein, Fritz},
   Title = {Efficient Type Inference for Higher-Order Binding-Time Analysis},
   BookTitle = {Proc. Conf. on Functional Programming Languages and Computer Architecture (FPCA), Cambridge, Massachusetts},
   Pages = {448--472},
   Month = {August},
   Year = {1991}

EndNote Reference [help]

Get EndNote Reference (.ref)