Abstract
Hindley/Milner-style polymorphism is a simple, natural, and flexible type discipline for functional languages, but incorporating imperative extensions is difficult. We present a new technique for typing references in the presence of polymorphism by inferring a concise summary of each expression's allocation behavior—a type effect. A simple technique for proving soundness with respect to a reduction semantics demonstrates that the type system prevents type errors. By establishing that the system corresponds to an alternate system better suited to implementation, we obtain an algorithm to perform type and effect inference.
This research was supported in part by the United States Department of Defense under a National Defense Science and Engineering Graduate Fellowship, and by NSF grant CCR 89-17022.
Chapter PDF
References
Barendregt, H. P. The Lambda Calculus: Its Syntax and Semantics, revised ed., vol. 103 of Studies in Logic and the Foundations of Mathematics. North-Holland, Amsterdam, 1984.
Damas, L., and Milner, R. Principal type schemes for functional programs. Proceedings of the 9th Annual Symposium on Principles of Programming Languages (January 1982), 207–212.
Damas, L. M. M. Type Assignment in Programming Languages. PhD thesis, University of Edinburgh, 1985.
Deutsch, A. On determining lifetime and aliasing of dynamically allocated data in higher-order functional specifications. Proceedings of the 17th Annual Symposium on Principles of Programming Languages (January 1990), 157–168.
Felleisen, M., and Friedman, D. P. A syntactic theory of sequential state. Theoretical Computer Science 69, 3 (1989), 243–287. Preliminary version in: Proceedings of the 14th Annual Symposium on Principles of Programming Languages, 1987, 314–325.
Felleisen, M., Friedman, D. P., Kohlbecker, E. E., and Duba, B. A syntactic theory of sequential control. Theoretical Computer Science 52, 3 (1987), 205–237. Preliminary version in: Proceedings of the Symposium on Logic in Computer Science, 1986, 131–141.
Felleisen, M., and Hieb, R. The revised report on the syntactic theories of sequential control and state. Tech. Rep. TR-100, Rice University, June 1989. To appear in: Theoretical Computer Science.
Hindley, R. The principal type-scheme of an object in combinatory logic. Transactions of the American Mathematical Society 146 (December 1969), 29–60.
Jouvelot, P., and Gifford, D. K. Algebraic reconstruction of types and effects. Proceedings of the 18th Annual Symposium on Principles of Programming Languages (January 1991), 303–310.
Leroy, X., and Weis, P. Polymorphic type inference and assignment. Proceedings of the 18th Annual Symposium on Principles of Programming Languages (January 1991), 291–302.
Lucassen, J. M., and Gifford, D. K. Polymorphic effect systems. Proceedings of the 15th Annual Symposium on Principles of Programming Languages (January 1988), 47–57.
Milner, R. A theory of type polymorphism in programming. Journal of Computer and System Sciences 17 (1978), 348–375.
Milner, R., and Tofte, M. Commentary on Standard ML. MIT Press, Cambridge, Massachusetts, 1991.
Milner, R., Tofte, M., and Harper, R. The Definition of Standard ML. MIT Press, Cambridge, Massachusetts, 1990.
O'Toole Jr., J. W. Type abstraction rules for references: A comparison of four which have achieved notoriety. Unpublished, 1990.
Standard ML of New Jersey release notes (version 0.75). AT&T Bell Laboratories, November 1991.
Talpin, J.-P., and Jouvelot, P. The type and effect discipline. Tech. Rep. EMP-CRI A/206, Ecole des Mines de Paris, July 1991.
Tofte, M. Type inference for polymorphic references. Information and Computation 89, 1 (November 1990), 1–34.
Wright, A. K., and Felleisen, M. A syntactic approach to type soundness. Tech. Rep. 91-160, Rice University, April 1991. To appear in: Information and Computation.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1992 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Wright, A.K. (1992). Typing references by effect inference. In: Krieg-Brückner, B. (eds) ESOP '92. ESOP 1992. Lecture Notes in Computer Science, vol 582. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-55253-7_28
Download citation
DOI: https://doi.org/10.1007/3-540-55253-7_28
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-55253-6
Online ISBN: 978-3-540-46803-5
eBook Packages: Springer Book Archive