
Efficient Type Inference for HigherOrder BindingTime Analysis?
Fritz Henglein
DIKU
University of Copenhagen
Universitetsparken 1
2100 Copenhagen O
Denmark
Internet: henglein@diku.dk
May 29, 1991
Abstract
Bindingtime analysis determines when variables and expressions in a program can be bound to their values, distinguishing between early (compiletime) and late (runtime) binding. Bindingtime information can be used by compilers to produce more efficient target programs by partially evaluating programs at compiletime. Bindingtime analysis has been formulated in abstract interpretation contexts and more recently in a typetheoretic setting. In a typetheoretic setting bindingtime analysis is a type inference problem: the problem of inferring a completion of a >=term e with bindingtime annotations such that e satisfies the typing rules. Nielson and Nielson and Schmidt have shown that every simply typed >=term has a unique completion ^e that minimizes late binding in TML, a monomorphic type system with explicit bindingtime annotations, and they present exponential time algorithms for computing such minimal completions.1 Gomard proves the same results for a variant of his twolevel >=calculus without a socalled 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(n3). He conjectures that the completions computed are minimal. In this paper we expand and improve on Gomard's work in the following ways.
ffl We identify the combinatorial core of type inference for bindingtime analysis in Gomard's type system with lifting" by effectively characterizing it as solving a specific class of constraints on type expressions.
ffl 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".
ffl We devise a very efficient algorithm for computing minimal completions. It is a refinement
of a fast unification algorithm, and an amortization argument shows that a fast
union/findbased implementation executes in almostlinear time, O(nff(n; n)), where
is an inverse of Ackermann's function.
?In Proc. Conference on Functional Programming Languages and Computer Architecture (FPCA), Cambridge,
Massachusetts, August 1991, pp. 448472, SpringerVerlag, Lecture Notes in Computer Science, Vol. 523. This
research has been supported by Esprit BRA 3124, Semantique.
1A (minimal) completion is called a (best) decoration in the work of Nielson and Nielson and Schmidt.