Skip to main content
Log in

Simple imperative polymorphism

  • Published:
LISP and Symbolic Computation

Abstract

This paper describes a simple extension of the Hindley-Milner polymorphic type discipline to call-by-value languages that incorporate imperative features like references, exceptions, and continuations. This extension sacrifices the ability to type every purely functional expression that is typable in the Hindley-Milner system. In return, it assigns the same type to functional and imperative implementations of the same abstraction. Hence with a module system that separates specifications from implementations, imperative features can be freely used to implement polymorphic specifications. A study of a number of ML programs shows that the inability to type all Hindley-Milner typable expressions seldom impacts realistic programs. Furthermore, most programs that are rendered untypable by the new system can be easily repaired.

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

Access this article

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Similar content being viewed by others

References

  1. “Standard ML of New Jersey release notes (version 0.93),” AT&T Bell Laboratories (November 1993).

  2. Damas, L. M. M.Principal Type Schemes for Functional Programs, InProceedings of the 9th Annual ACM Symposium on Principles of Programming Languages (January 1982) 207–212.

  3. Damas, L. M. M.Type Assignment in Programming Languages, PhD thesis, University of Edinburgh (1985).

  4. Greiner, J. “Standard ML weak polymorphism can be sound,” Technical Report CMU-CS-93-160R, Carnegie Mellon University (September 1993).

  5. Harper, R. and M. Lillibridge. “Explicit polymorphism and CPS conversion,” InConference Record of the 20th Annual ACM Symposium on Principles of Programming Languages (January 1993) 206–219.

  6. Harper, R., B. F. Duba, and D. MacQueen. “Typing first-class continuations in ML,”Journal of Functional Programming 3, 4 (October 1993), 465–484.

    Google Scholar 

  7. Hindley, R. “The principal type-scheme of an object in combinatory logic,”Transactions of the American Mathematical Society, 146 (December 1969) 29–60.

    Google Scholar 

  8. Hoang, M., J. Mitchell, and R. Viswanathan. “Standard ML-NJ weak polymorphism and imperative constructs,” InProceedings of the Eighth Annual Symposium on Logic in Computer Science (June 1993) 15–25.

  9. Leroy, X.Typage polymorphe d'un langage algorithmique, PhD thesis, L'Université Paris 7 (1992).

  10. Leroy, X. “Polymorphism by name for references and continuations,” InConference Record of the 20th Annual ACM Symposium on Principles of Programming Languages (January 1993) 220–231.

  11. Leroy, X. and P. Weis. “Polymorphic type inference and assignment,” InProceedings of the 18th Annual Symposium on Principles of Programming Languages (January 1991) 291–302.

  12. Milner, R. “A theory of type polymorphism in programming,”Journal of Computer and System Sciences, 17 (1978) 348–375.

    Google Scholar 

  13. Milner, R. and M. Tofte.Commentary on Standard ML, MIT Press, Cambridge, Massachusetts (1991).

    Google Scholar 

  14. Milner, R., M. Tofte, and R. Harper.The Definition of Standard ML, MIT Press, Cambridge, Massachusetts (1990).

    Google Scholar 

  15. Ohori, A. “A simple semantics for ML polymorphism,” InProceedings of the Fourth International Conference on Functional Programming Languages and Computer Architecture (September 1989) 281–292.

  16. Reppy, J. H.Higher-order Concurrency, PhD thesis, Cornell University (1991).

  17. Talpin, J.-P. and P. Jouvelot. “The type and effect discipline,” InProceedings of the Seventh Annual Symposium on Logic in Computer Science (June 1992) 162–173.

  18. Tofte, M. “Type inference for polymorphic references,”Information and Computation, 89, 1 (November 1990) 1–34.

  19. Wright, A. K. “Typing references by effect inference,” InProceedings of the 4th European Symposium on Programming, Springer-Verlag Lecture Notes in Computer Science 582 (1992) 473–491.

  20. Wright, A. K. and M. Felleisen. “A Syntactic Approach to Type Soundness,” Technical Report 91–160, Rice University (April 1991). To appear inInformation and Computation, 1994.

Download references

Author information

Authors and Affiliations

Authors

Additional information

This research was supported in part by the United States Department of Defense under a National Defense Science and Engineering Graduate Fellowship.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Wright, A.K. Simple imperative polymorphism. LISP and Symbolic Computation 8, 343–355 (1995). https://doi.org/10.1007/BF01018828

Download citation

  • Issue Date:

  • DOI: https://doi.org/10.1007/BF01018828

Keywords

Navigation