Skip to main content
SpringerLink
Log in

Efficient type inference for higher-order binding-time analysis

  • Conference paper
  • First Online:
Functional Programming Languages and Computer Architecture (FPCA 1991)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 523))

Abstract

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 formulated in abstract interpretation contexts and more recently in a type-theoretic setting.

In a type-theoretic setting binding-time analysis is a type inference problem: 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 completion ê 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 characterizing 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 completions. It is a refinement of a fast unification algorithm, and an amortization 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 exponential time to almost-linear time. It also improves on Gomard's polynomial time completion algorithm by a quadratic factor and as such appears to be the first efficient algorithm that provably computes minimal completions.

This research has been supported by Esprit BRA 3124, Semantique.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. A. Aho, J. Hopcroft, and J. Ullman. The Design and Analysis of Computer Algorithms. Addison-Wesley, 1974.

    Google Scholar 

  2. A. Aho, R. Sethi, and J. Ullman. Compilers: Principles, Techniques, and Tools. Addison Wesley, 1986. Addison-Wesley, 1986, Reprinted with corrections, March 1988.

    Google Scholar 

  3. A. Bondorf, N. Jones, T. Mogensen, and P. Sestoft. Binding time analysis and the taming of self-application. Sep. 1988. To appear in Transactions on Programming Languages and Systems (TOPLAS).

    Google Scholar 

  4. A. Bondorf. Automatic autoprojection of higher order recursive equations. In N. Jones, editor, Proc. 3rd European Symp. on Programming (ESOP '90), Copenhagen, Denmark, pages 70–87, Springer, May 1990. Lecture Notes in Computer Science, Vol. 432.

    Google Scholar 

  5. A. Bondorf. Self-Applicable Partial Evaluation. PhD thesis, DIKU, University of Copenhagen, Dec. 1990.

    Google Scholar 

  6. C. Consel. New insights into partial evaluation: the Schism experiment. In Proc. 2nd European Symp. on Programming (ESOP), Nancy, France, pages 236–246, Springer, 1988. Lecture Notes in Computer Science, Vol. 300.

    Google Scholar 

  7. C. Consel. Binding time analysis for higher order untyped functional languages. In Proc. LISP and Functional Programmin (LFP), Nice, France, ACM, July 1990.

    Google Scholar 

  8. Y. Fuh and P. Mishra. Type inference with subtypes. In Proc. 2nd European Symp. on Programming, pages 94–114, Springer-Verlag, 1988. Lecture Notes in Computer Science 300.

    Google Scholar 

  9. C. Gomard and N. Jones. A partial evaluator for the untyped lambda-calculus. J. Functional Programming, 1(1):21–69, Jan. 1991.

    Google Scholar 

  10. C. Gomard. Higher Order Partial Evaluation — HOPE for the Lambda Calculus. Master's thesis, DIKU, University of Copenhagen, Denmark, September 1989.

    Google Scholar 

  11. C. Gomard. Partial type inference for untyped functional programs (extended abstract). In Proc. LISP and Functional Programming (LFP), Nice, France, July 1990.

    Google Scholar 

  12. F. Henglein. Simple type inference and unification. Oct. 1988. New York University, Computer Science Department, SETL Newsletter 232.

    Google Scholar 

  13. F. Henglein. Type inference and semi-unification. In Proc. ACM Conf. on LISP and Functional Programming (LFP), Snowbird, Utah, pages 184–197, ACM, ACM Press, July 1988.

    Google Scholar 

  14. F. Henglein. Dynamic typing. March 1991. Semantique note 90, DIKU, University of Copenhagen.

    Google Scholar 

  15. J. Hopcroft and R. Karp. An Algorithm for Testing the Equivalence of Finite Automata. Technical Report TR-71-114, Dept. of Computer Science, Cornell U., 1971.

    Google Scholar 

  16. S. Hunt and D. Sands. Binding time analysis: a new PERspective. In Proc. ACM/IFIP Symp. on Partial Evaluation and Semantics Based Program Manipulation (PEPM), New Haven, Connecticut, June 1991.

    Google Scholar 

  17. G. Huet. Résolution d'equations dans des langages d'ordre 1, 2, ..., omega. PhD thesis, Univ. Paris VII, Sept. 1976.

    Google Scholar 

  18. N. Jones, C. Gomard, A. Bondorf, O. Danvy, and T. Mogensen. A self-applicable partial evaluator for the lambda calculus. In 1990 International Conference on Computer Languages, New Orleans, Louisiana, March 1990, pages 49–58, IEEE Computer Society, 1990.

    Google Scholar 

  19. N. Jones and S. Muchnick. Binding time optimization in programming languages: some thoughts toward the design of the ideal language. In Proc. 3rd ACM Symp. on Principles of Programming Languages, pages 77–94, ACM, Jan. 1976.

    Google Scholar 

  20. N. Jones and S. Muchnick. TEMPO: A Unified Treatment of Binding Time and Parameter Passing Concepts in Programming Languages. Volume 66 of Lecture Notes in Computer Science, Springer, 1978.

    Google Scholar 

  21. N. Jones. Automatic program specialization: a re-examination from basic principles. In D. Bjorner, A. Ershov, and N. Jones, editors, Proc. Partial Evaluation and Mixed Computation, pages 225–282, IFIP, North-Holland, Oct. 1987.

    Google Scholar 

  22. N. Jones and D. Schmidt. Compiler generation from denotational semantics. In N. Jones, editor, Semantics-Directed Compiler Generation, Aarhus, Denmark, pages 70–93, Springer, 1980. Lecture Notes in Computer Science, Vol. 94.

    Google Scholar 

  23. N. Jones, P. Sestoft, and H. Sondergard. An experiment in partial evaluation: the generation of a compiler generator. SIGPLAN Notices, 20(8), Aug. 1985.

    Google Scholar 

  24. N. Jones, P. Sestoft, and H. Sondergaard. Mix: a self-applicable partial evaluator for experiments in compiler generation. LISP and Symbolic Computation, 2:9–50, 1989.

    Google Scholar 

  25. H. Kröger. Static-Scope-Lisp: splitting an interpreter into compiler and run-time system. In W. Brauer, editor, GI — 11. Jahrestagung, Munich, Germany, pages 20–31, Springer, Munich, Germany, 1981. Informatik-Fachberichte 50.

    Google Scholar 

  26. J. Launchbury. Projections for specialisation. In D. Bjorner, A. Ershov, and N. Jones, editors, Proc. Workshop on Partial Evaluation and Mixed Computation, Denmark, pages 465–483, North-Holland, Oct. 1987.

    Google Scholar 

  27. J. Launchbury. Projection Factorisations in Partial Evaluation. PhD thesis, University of Glasgow, Jan. 1990.

    Google Scholar 

  28. J. Lassez, M. Maher, and K. Marriott. Unification revisited. In J. Minker, editor, Foundations of Deductive Databases and Logic Programming, Morgan Kauffman, 1987.

    Google Scholar 

  29. J. Mitchell. Coercion and type inference. In Proc. 11th ACM Symp. on Principles of Programming Languages (POPL), 1984.

    Google Scholar 

  30. A. Martelli and U. Montanari. An efficient unification algorithm. ACM Transactions on Programming Languages and Systems, 4(2):258–282, Apr. 1982.

    Google Scholar 

  31. T. Mogensen. Partially static structures in a self-applicable partial evaluator. In D. Bjorner, A. Ershov, and N. Jones, editors, Proc. Workshop on Partial Evaluation and Mixed Computation, Denmark, pages 325–347, North-Holland, Oct. 1987.

    Google Scholar 

  32. T. Mogensen. Binding time analysis for polymorphically typed higher order languages. In J. Diaz and F. Orejas, editors, Proc. Int. Conf. Theory and Practice of Software Development (TAPSOFT), Barcelona, Spain, pages 298–312, Springer, March 1989. Lecture Notes in Computer Science 352.

    Google Scholar 

  33. H. Nielson and F. Nielson. Semantics directed compiling for functional languages. In Proc. ACM Conf. on LISP and Functional Programming (LFP), 1986.

    Google Scholar 

  34. H. Nielson and F. Nielson. Automatic binding time analysis for a typed lambda calculus. Science of Computer Programming, 10:139–176, 1988.

    Google Scholar 

  35. H. Nielson and F. Nielson. Two-level semantics and code generation. Theoretical Computer Science, 56, 1988.

    Google Scholar 

  36. M. Paterson and M. Wegman. Linear unification. J. Computer and System Sciences, 16:158–167, 1978.

    Google Scholar 

  37. S. Romanenko. A compiler generator produced by a self-applicable specializer can have a surprisingly natural and understandable structure. In D. Bjorner, A. Ershov, and N. Jones, editors, Proc. Workshop on Partial Evaluation and Mixed Computation, Denmark, pages 465–483, North-Holland, Oct. 1987.

    Google Scholar 

  38. D. Schmidt. Static properties of partial evaluation. In D. Bjorner, A. Ershov, and N. Jones, editors, Proc. Workshop on Partial Evaluation and Mixed Computation, Denmark, pages 465–483, North-Holland, Oct. 1987.

    Google Scholar 

  39. P. Sestoft. The structure of a self-applicable partial partial evaluator. In H. Ganzinger and N. Jones, editors, Programs as Data Objects, Copenhagen, Denmark, pages 236–256, Springer, 1985. published in 1986, Lecture Notices in Computer Science, Vol. 217.

    Google Scholar 

  40. R. Stansifer. Type inference with subtypes. In Proc. 15th ACM Symp. on Principles of Programming Languages, pages 88–97, ACM, San Diego, California, Jan. 1988.

    Google Scholar 

  41. R. Tarjan. Depth-first search and linear graph algorithms. SIAM J. Comput., 1(2), June 1972.

    Google Scholar 

  42. R. Tarjan. Data Structures and Network Flow Algorithms. Volume CMBS 44 of Regional Conference Series in Applied Mathematics, SIAM, 1983.

    Google Scholar 

  43. M. Wand. A simple algorithm and proof for type inference. Fundamenta Informaticae, X:115–122, 1987.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. DIKU, University of Copenhagen, Universitetsparken 1, 2100, Copenhagen Ø, Denmark

    Fritz Henglein

Authors
  1. Fritz Henglein
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

John Hughes

Rights and permissions

Reprints and permissions

Copyright information

© 1991 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Henglein, F. (1991). Efficient type inference for higher-order binding-time analysis. In: Hughes, J. (eds) Functional Programming Languages and Computer Architecture. FPCA 1991. Lecture Notes in Computer Science, vol 523. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3540543961_22

Download citation

  • DOI: https://doi.org/10.1007/3540543961_22

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-54396-1

  • Online ISBN: 978-3-540-47599-6

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation