Yasuhiko Minamide
Greg Morrisett
Robert Harper
ABSTRACT
Closure conversion is a program transformation used by compilers to separate code from data. Previous accounts of closure conversion use only untyped target languages. Recent studies show that translating to typed target languages is a useful methodology for building compilers, because a compiler can use the types to implement efficient data representations, calling conventions, and tag-free garbage collection. Furthermore, type-based translations facilitate security and debugging through automatic type checking, as well as correctness arguments through the method of logical relations.We present closure conversion as a type-directed, and type-preserving translation for both the simply-typed and the polymorphic λ-calculus. Our translations are based on a simple "closures as objects" principle: higher-order functions are viewed as objects consisting of a single method (the code) and a single instance variable (the environment). In the simply-typed case, the Pierce-Turner model of object typing where objects are packages of existential type suffices. In the polymorphic case, more careful tracking of type sharing is required. We exploit a variant of the Harper-Lillibridge "translucent type" formalism to characterize the types of polymorphic closures.
- 1.A. W. Appel. Compiling with Contmuations. Cambridge University Press, 1992. Google Scholar
Digital Library
- 2.A. W. Appel and T. Jim. Continuation-passing, closurepassing style. In A CM Syrup. on Prme#ples of Programmzng Languages, 1989. Google ScholarDigital Library
- 3.D. E. Britton. Heap storage management for the programming language Pascal. Master's thews, Universlty of Arizona, 1975.Google Scholar
- 4.L. Cardelli. The functional abstract machine. Polymorph#sm, i(i), 1983.Google Scholar
- 5.C Cousineau, P-L Curien, and M. Mauny. The categorical abstract machine. In Functional Programming Lanquages and Computer Architecture, pages 50-64, 1985. Google ScholarDigital Library
- 6.tt Friedman. Equahty between functionals. In R. Parikh, editor, Logic Colloquzum '75 Norh-Holland, 1975.Google Scholar
- 7.J.-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types, volume 7 of Cambridge Tracts #n Theoretical Computer Sczence. Cambridge University Press, Cambridge, England, 1989. Google ScholarDigital Library
- 8.J. Gosling. Java mtermediate bytecodes. In A CM StG- PLAN Workshop on Intermediate Representations (IR'95), Jan. 1995 Google ScholarDigital Library
- 9.J. Hannan. A type system for closure conversion. In The Workshop on Types for Proqram Analyszs, 1995.Google Scholar
- 10.R. Harper and M. Lillibridge. Exphcit polymorphmm and CPS conversion. In ACM Syrup. on Princzples of Programmmg Languages, 1993. Google ScholarDigital Library
- 11.R. Harper and M. Lillibridge A type-theoretic approach to higher-order modules. In A CM Syrup. on Prznc#ples of Programming Languages, pages 123-137, 1994. Google ScholarDigital Library
- 12.R. Harper, D. MacQueen, and R. Milner Standard ML Technical Report ECS-LFCS-86-2, Laboratory for the Foundations of Computer Science# Edinburgh University. Mar. 1986Google Scholar
- 13.t#. Harper and J. C. Mitchell. On the type structure of 3tandard ML A CM Transaction on Programm#n9 Languages and Systems, 15(2), 1993 Google ScholarDigital Library
- 14.R Harper and G. Morrisett. Complhng potymorphism using intensional type analysis In A CM Syrup. on Prmc#ples of Programmmg Languages, pages 130-141, 1995. Google ScholarDigital Library
- 15.T. Johnsson. Lambda lifting- Transformmg programs to recursive equations. In Functional Programming Language and Computer Architecture, LNCS 201, pages 190-203. Springer- Verlag, 1985. Google ScholarDigital Library
- 16.R. Kelsey and P. Hudak. Realistic compilation by program translation -detailed summary-. In A CM Syrup. on Pmnc#ples of Programming Languages, pages 281-292, 1989. Google ScholarDigital Library
- 17.D. Kranz et al. Orbit: An optimizing compiler for Scheme. In Proc. of the SIGPLAN '86 Syrup. on Compiler Constructzon, 1986. Google ScholarDigital Library
- 18.X. Leroy. Unboxed objects and polymorphic typing. In A CM Symp. on Principles o/Programming Languages, 1992. Google ScholarDigital Library
- 19.X. Leroy. Manifest types, modules, and separate compilation. In A CM Symp. on Pmnczples of Programming Languages, pages 109-122, 1994. Google ScholarDigital Library
- 20.D. MacQueen. Modules for Standard ML. In Proc. ACM Conf. Lisp and Functional Programmzng, pages 198-207, 1984. Revised version appears in {12}. Google ScholarDigital Library
- 21.Y. Minamide, G. Morrisett, and R. Harper. Typed closure conversion. Technical Report CMU-CS-95-171, School of Computer Science, Carnegie Mellon University, July 1995.Google Scholar
- 22.J. C. Mitchell and G. D. Plotkin. Abstract types have existential type. A CM Transactwn on Programming Languages and Systems, 10(3), 1988. Google ScholarDigital Library
- 23.G. Morrisett, M. FeIIeisen, and R. Harper. Abstract models of memory management. In Functwnal Programm,ng Languages and Computer Architecture, pages 66-77, June 1995. Google ScholarDigital Library
- 24.R. Morrison, A. Dearle, R. Connor, and A. L. Brown. An ad hoc approach to the implementation of polymorphism. A CM Transactwn on Programming Languages and Systems, 13(3), 1991. Google ScholarDigital Library
- 25.A. Ohori. A compilation method for ML-style polymorphic record calculi. In A CM Symp. on Principles of Programming Languages, 1992. Google ScholarDigital Library
- 26.B. C Pierce and D. N. T#rner. Simple type-theoretic foundations for object-oriented programming. Journal of Functzonal Programming, 4(2):207-247, Apr. 1994. A preliminary version appeared in Principles of Programming Languages, 1993, and as University of Edinburgh technical report ECS- LFCS-92-225, under the title "Object-Oriented Programming Without Recursive Types".Google ScholarCross Ref
- 27.G. D. Plotkin. Lambda-definability in the full type hierarchy. In To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism. Academic Press, 1980.Google Scholar
- 28.U. S. Reddy. Objects as closures. In Proe. ACM Conf. Lisp and Functional Programming, 1988.Google Scholar
- 29.J. C. Reynolds. Definitional interpreters for higher-order programming languages. In Proceedings of the Annual A CM Conference, pages 717-740, 1972. Google ScholarDigital Library
- 30.Z. Shao and A. W. Appel. Space-efficient closure representations. In Proc. A CM Conf. Lzsp and Functional Programming, 1994. Google ScholarDigital Library
- 31.Z. Shao and A. W. Appel. A type-based compiler for Standard ML. In Programming Language Design and Its zmplemenation, pages 116-129, 1995. Google ScholarDigital Library
- 32.R. Statman. Completeness, invariance, and lambdadefinability. Journal of Symbolic Logic, 47:17-26, 1982.Google ScholarCross Ref
- 33.R. Statman. Logical relations and the typed A-calculus. informatzon and Control, 65, 1985.Google Scholar
- 34.G. L. Steele Jr. Rabbit: A compiler for Scheme. Master's thesis, MIT, 1978.Google Scholar
- 35.W.W. Tait. Intensionat interpretation of functionals of finite type. Journal of Symbohc Logic, 32(2), 1967.Google Scholar
- 36.D. Tarditi, G. Morrisett, P. Cheng, C. Stone, R. Harper, and P. Lee. TIL: A type-directed optimizing compiler for ML. Technical report, School of Computer Science, Carnegie Mellon University, Oct. 1995. To appear.Google Scholar
- 37.A. Tolmach. Tag-free garbage collection using explicit type parameters. In Proc. A CM Conf. Lisp and Functional Programmmg, pages 1-11, June 1994. Google ScholarDigital Library
- 38.R. Wahbe, S. Lucco, T. Anderson, and S. Graham. Efficient software-based fault isolation. In 14th ACM Symposium on Operating Systems Pmnczples, Dec. 1993. Google ScholarDigital Library
- 39.M. Wand and P. Steckler. Selective and lightweight closure conversion. In A CM Symp. on Principles of Programming Languages, 1994. Google ScholarDigital Library
Index Terms
- Typed closure conversion
Recommendations
Typed closure conversion for the calculus of constructions
PLDI '18Dependently typed languages such as Coq are used to specify and verify the full functional correctness of source programs. Type-preserving compilation can be used to preserve these specifications and proofs of correctness through compilation into the ...
Typed closure conversion for the calculus of constructions
PLDI 2018: Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and ImplementationDependently typed languages such as Coq are used to specify and verify the full functional correctness of source programs. Type-preserving compilation can be used to preserve these specifications and proofs of correctness through compilation into the ...
Typed Closure Conversion for Recursively-Defined Functions
Much recent work on the compilation of statically typed languages such as ML relies on the propagation of type information from source to object code in order to increase the reliability and maintainabilty of the compiler itself and to improve the ...
Comments