Henry G. Baker
ABSTRACT
Type inference is the process by which an expression in an untyped computer language such as the lambda-calculus, Lisp, or a functional language can be assigned a static data type in order to improve the code generated by a compiler. Storage use inference is the process by which a program in a computer language can be statically analyzed to model its run-time behavior, particularly the containment and sharing relations among its run-time data structures. The information generated by storage use information can also be used to improve the code generated by a compiler, because knowledge of the containment and sharing relations of run-time data structures allows for methods of storage allocation and deallocation which are cheaper than garbage-collected heap storage and allows for the in-place updating of functional aggregates.
Type inference and storage use inference have traditionally been considered orthogonal processes, with separate traditions and literature. However, we show in this paper than this separation may be a mistake, because the best-known and best-understood of the type inferencing algorithms—Milner's unification method for ML—already generates valuable sharing and containment information which is then unfortunately discarded. We show that this sharing information is already generated by standard unification algorithms with no additional overhead during unification; however, there is some additional work necessary to extract this information. We have not yet precisely characterized the resolving power of this sharing and containment information, but we believe that it is similar to that generated by researchers using other techniques. However, our scheme seems to only work for functional languages like pure Lisp.
The unification of type and storage inferencing yields new insights into the meaning of “aggregate type”, which should prove valuable in the design of future type systems.
- Ada. Reference Manual for the Ada r Programming Language. American National Standards Institute, New York, 1983.]] Google Scholar
Digital Library
- Aho, A.V., Sethi, R., and Ullman, J.D. Compilers: Principles, Techniques, and Tools. Addision- Wesley, Reading, MA, 1986.]] Google ScholarDigital Library
- Appel, A.W., Ellis, J.R., and Li, K. "Real-time concurrent garbage collection on stock multiprocessors". S{GPLAN PLDI, June, 1988.]] Google ScholarDigital Library
- Baase, S. Computer Algorithms: Introduction to Design and Analysis. Addison-Wesley, Reading, MA, 1978.]] Google ScholarDigital Library
- Baker, H.G. "List processing in real time on a serial computer". CACM 21,4 (April 1978),280-294.]] Google ScholarDigital Library
- Baker, H.G. "The Nimble Type Inferencer for Common Lisp-84". Nimble Computer Corl~ration, 1990, in preparation.]]Google Scholar
- Barth, J.M. "Shifting garbage collection overhead to compile time". CACM 20,7 (July 1977),513-518.]] Google ScholarDigital Library
- Bloss, A. "Update Analysis and the Efficient Implementation of Functional Aggregates". 4'th ACM/IFIP Conf. on Funct. Prog. and Cornp. Arch., London, Sept. 1989, 26-38.]] Google ScholarDigital Library
- Boehm, H.-J., and Demers, A. "Implementing Russell". ACM Sigplan '86 Syrup. on Compiler Constr., Sigplan Notices 21,7 (July 1986),186-195.]] Google ScholarDigital Library
- Chase, David R. Garbage Collection and Other Optimizations. Ph.D. Thesis, Rice University, August, 1987.]] Google ScholarDigital Library
- Goto, Eiichi. "Monocopy and Associative Algorithms in an Extended Lisp". Info. Sci. Lab., Univ. of Tokyo, 1974.]]Google Scholar
- Hederman, Lucy. Compile Time Garbage Collection. M.S. Thesis, Rice Univ. Comp. Sci. Dept., Sept. 1988.]]Google Scholar
- Horowitz, S., Pfeiffer, P., and Reps, T. "Dependence Analysis for Pointer Variables". ACM Sigplan '89 Conf. on Prog. Lang. Design and Impl., S igplan Notices 24,7 (July I989),28-40.]] Google ScholarDigital Library
- Hudak, P., and B loss, A. "The aggregate update problem in functional programming systems". 12'th ACM POPL, January, 1985.]] Google ScholarDigital Library
- Hudak, P. "A Semantic Model of Reference Counting and its Abstraction". 1986 ACM Lisp and Functional Programming Conference, Cambridge, MA,351-363.]] Google ScholarDigital Library
- Ichbiah, J.D., et al. "Rationale for the Design of the Ada Programming Language". ACM Sigplan Notices 14,6 (June 1979), Part B.]] Google ScholarDigital Library
- Inoue, K, Seki, H., and Yagi, H. "Analysis of functional programs to detect run-time garbage cells". ACM TOPLAS 10,4 (Oct. 1988), 555-578.]] Google ScholarDigital Library
- Jones, N.D., and Muchnick, $.S. "Flow Analysis and Optimization of Lisp-like Structures". 6'th A CM POPL, jan. 1979,244-256.]] Google ScholarDigital Library
- Jones, N.D., and Muchnick, S.S. "A flexible approach to interprocedural data flow analysis and programs with recursive data structures". 9'th ACM POPL, 1982,66-74.]] Google ScholarDigital Library
- Jones, S.B., and Le Metayer, D. "Compile-time garbage collection by sharing analysis". ACM Func. Prog. Langs. and Comp. Arch. (FPCA), 1989, 54-74.]] Google ScholarDigital Library
- Kanellakis, P.C., and Mitchell, J.C. "Polymorphic unification and ML typing". 16'th ACM POPL, January 1989,105-115.]] Google ScholarDigital Library
- Larus, James Richard. Restructuring Symbolic Programs for Concurrent Execution on Multiprocessors. Ph.D. Thesis, UC Berkeley, also published as Rep. No. UCB/CSD/89/502, May, 1989.]] Google ScholarDigital Library
- Lieberman, H., and Hewitt, C. "A real-time garbage collector based on the lifetime of objects". CACM 26,6 (June 1983),419-429.]] Google ScholarDigital Library
- Mairson, H.G. "Deciding ML Typability is Complete for Deterministic Exponential Time". 17'th ACM POPL, January 1990, 382-401.]] Google ScholarDigital Library
- Mason, Ian A. The Semantics of Destructive Lisp. Center for the Study of Language and Information, Stanford, 1986.]] Google ScholarDigital Library
- Milner, R. "A theory of type polymorphism in programming". JCSS 17,3 (1978),348-375.]]Google ScholarCross Ref
- Mitchell, J.C. "Coercion and Type Inference". I l'th ACM POPL, 1984, 175-185.]] Google ScholarDigital Library
- Moon, D. "Garbage collection in a large Lisp system". ACM Lisp and Functional Programming Conf., 1984,pp.235-246.]] Google ScholarDigital Library
- Muchnik, S. S., and Jones, N.D. "Binding time optimizations in programming languages: some thoughts toward the design of an ideal language". ACM POPL, 1976.]] Google ScholarDigital Library
- Muchnik, S., and Jones, N. "Flow analysis and optimization of LISP-like structures". In Program Flow Analysis: Theory and Applications, by the same authors, Prentice-Hall, Englewood Cliffs, NJ, 1981.]]Google Scholar
- Peyton-Jones, S.L. The Implementation of Functional Programming Languages. Prentice-Hall, NY, 1987.]]Google Scholar
- Pleban, Uwe F. Preexecution Analysis Based on Denotational Semantics. Ph.D. Thesis, University of Kansas, 1981.]] Google ScholarDigital Library
- Ruggieri, Christina. Dynamic Memory Allocation Techniques Based on the Lifetimes of Objects. Ph.D. Thesis, Purdue University, August, 1987.]] Google ScholarDigital Library
- Ruggieri, C. and Murtagh, T. "Lifetime analysis of dynamically allocated objects". 15'th ACM POPL, January, 1988.]] Google ScholarDigital Library
- Schwartz, J.T. "Optimization of very high level languages, Part II: Deducing relationships of inclusion and membership". Computer Languages 1,3 (1975),197-218.]]Google Scholar
- Steele, G.L., Jr. Rabbit: A compiler for Scheme. AI Memo 474, MIT, May 1978.]] Google ScholarDigital Library
- Suzuki, N. "Inferring types in Smalltalk". 8'th ACM POPL, 1981,p. 187-199.]] Google ScholarDigital Library
- Ungar, D. "Generation scavenging: A non-disruptive high performance storage reclamation algorithm". ACM Software Eng. Symp. on Prac. Software Dev. Envs., SIGPLAN Notices 19,5 (May 1984),157-167.]] Google ScholarDigital Library
- Wand, M. "A Semantic Prototyping System". Proc. of ACM Sigplan '84 Syrup. on Compiler Constr., Sigplan Notices 19,6 (June 1984),213-221.]] Google ScholarDigital Library
- Wand, M., and O'Keefe, P. "On the Complexity of Type Inference with Coercion". ACM Func. Prog. Langs. and Cornp. Arch. (FPCA), 1989, 293-297.]] Google ScholarDigital Library
Index Terms
- Unify and conquer
Recommendations
To unify or not to unify: a case study on unified builds (in WebKit)
CC 2019: Proceedings of the 28th International Conference on Compiler ConstructionUnified builds are a simple but effective technique to reduce the build time of large software projects. Unified builds generate large compiler tasks by bundling multiple source files into one, resulting in a significant reduction in build time through ...
Type checking and inference for polymorphic and existential types
CATS '09: Proceedings of the Fifteenth Australasian Symposium on Computing: The Australasian Theory - Volume 94This paper proves undecidability of type checking and type inference problems in some variants of typed lambda calculi with polymorphic and existential types. First, type inference in the domain-free polymorphic lambda calculus is proved to be ...
Comments