article

Open access

Quantified types in an imperative language

Author:

Dan GrossmanAuthors Info & Claims

ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 28, Issue 3

Pages 429 - 475

https://doi.org/10.1145/1133651.1133653

Published: 01 May 2006 Publication History

Abstract

We describe universal types, existential types, and type constructors in Cyclone, a strongly typed C-like language. We show how the language naturally supports first-class polymorphism and polymorphic recursion while requiring an acceptable amount of explicit type information. More importantly, we consider the soundness of type variables in the presence of C-style mutation and the address-of operator. For polymorphic references, we describe a solution more natural for the C level than the ML-style “value restriction.” For existential types, we discover and subsequently avoid a subtle unsoundness issue resulting from the address-of operator. We develop a formal abstract machine and type-safety proof that capture the essence of type variables at the C level.

References

[1]

Abadi, M. and Cardelli, L. 1996. A Theory of Objects. Springer-Verlag, New York, NY.]]

[2]

Appel, A. 1992. Compiling with Continuations. Cambridge University Press, Cambridge, U.K.]]

[3]

Austin, T., Breach, S., and Sohi, G. 1994. Efficient detection of all pointer and array access errors. In Proceedings of the ACM Conference on Programming Language Design and Implementation (Orlando, FL). 290--301.]]

[4]

Benton, N., Kennedy, A., and Russell, G. 1998. Compiling Standard ML to Java bytecodes. In Proceedings of the 3rd ACM International Conference on Functional Programming (Baltimore, MD). 129--140.]]

[5]

Bos, H. and Samwel, B. 2002. Safe kernel programming in the OKE. In Proceedings of the 5th IEEE International Conference on Open Architectures and Network Programming (New York, NY). 141--152.]]

[6]

Botlan, D. L. and Rémy, D. 2003. MLF: Raising ML to the power of System-F. In Proceedings of the ACM International Conference on Functional Programming (Uppsala, Sweden). 27--38.]]

[7]

Bracha, G., Odersky, M., Stoutamire, D., and Wadler, P. 1998. Making the future safe for the past: Adding genericity to the Java programming language. In Proceedings of the 13th ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (Vancouver, B.C., Canada). 183--200.]]

[8]

Bruce, K., Cardelli, L., and Pierce, B. 1999. Comparing object encodings. Inform. Computat. 155, 108--133.]]

[9]

Cardelli, L. and Wegner, P. 1985. On understanding types, data abstraction, and polymorphism. ACM Comput. Surv. 17, 4, 471--522.]]

[10]

Cejtin, H., Jagannathan, S., and Weeks, S. 2000. Flow-directed closure conversion for typed languages. In 9th European Symposium on Programming. Lecture Notes in Computer Science, vol. 1782. Springer-Verlag, Berlin, Germany, 56--71.]]

[11]

Chailloux, E., Manoury, P., and Pagano, B. 2000. Développement d'Applications avec Objective Caml. O'Reilly, Paris, France. An English translation is currently freely available online at http://caml.inria.fr/oreilly-book/.]]

[12]

Chandra, S. and Reps, T. 1999. Physical type checking for C. In Proceedings of the ACM Workshop on Program Analysis for Software Tools and Engineering (Toulouse, France). 66--75.]]

[13]

Condit, J., Harren, M., McPeak, S., Necula, G., and Weimer, W. 2003. CCured in the real world. In Proceedings of the ACM Conference on Programming Language Design and Implementation. San Diego, CA. 232--244.]]

[14]

Crary, K. 2003. Toward a foundational typed assembly language. In Proceedings of the 30th ACM Symposium on Principles of Programming Languages (New Orleans, LA). 198--212.]]

[15]

Cyclone. 2001. Cyclone user's manual. Tech. rep. 2001-1855. Department of Computer Science, Cornell University, Ithaca, NY. The current version is available online at http://www.cs.cornell.edu/projects/cyclone/.]]

[16]

DeLine, R. and Fähndrich, M. 2001. Enforcing high-level protocols in low-level software. In Proceedings of the ACM Conference on Programming Language Design and Implementation (Snowbird, UT). 59--69.]]

[17]

Ditchfield, G. 1994. Contextual polymorphism. Ph.D. dissertation. University of Waterloo, Waterloo, Onto., Canada.]]

[18]

Garrigue, J. and Rémy, D. 1999. Semi-explicit first-class polymorphism for ML. Inform. Comput. 155, 1/2, 134--169.]]

[19]

Girard, J.-Y., Taylor, P., and Lafont, Y. 1989. Proofs and Types. Cambridge University Press, Cambridge, U.K.]]

[20]

Grossman, D. 2002. Existential types for imperative languages. In 11th European Symposium on Programming. Lecture Notes in Computer Science, vol. 2305. Springer-Verlag, Berlin, Germany, 21--35.]]

[21]

Grossman, D. 2003a. Safe programming at the C level of abstraction. Ph.D. dissertation. Cornell University, Ithaca, NY.]]

[22]

Grossman, D. 2003b. Type-safe multithreading in Cyclone. In Proceedings of the ACM International Workshop on Types in Language Design and Implementation (New Orleans, LA). 13--25.]]

[23]

Grossman, D., Morrisett, G., Jim, T., Hicks, M., Wang, Y., and Cheney, J. 2002. Region-based memory management in Cyclone. In Proceedings of the ACM Conference on Programming Language Design and Implementation (Berlin, Germany). 282--293.]]

[24]

Grossman, D., Zdancewic, S., and Morrisett, G. 2000. Syntactic type abstraction. ACM Trans. Programm. Lang. Syst. 22, 6 (Nov.), 1037--1080.]]

[25]

Harper, R. 1994. A simplified account of polymorphic references. Inform. Process. Lett. 51, 4 (Aug.), 201--206.]]

[26]

Henglein, F. 1993. Type inference with polymorphic recursion. ACM Trans. Programm. Lang. Syst. 15, 2 (Apr.), 253--289.]]

[27]

Hicks, M., Morrisett, G., Grossman, D., and Jim, T. 2004. Experience with safe manual memory-management in Cyclone. In Proceedings of the International Symposium on Memory Management (Vancouver, B.C., Canada).]]

[28]

Hicks, M., Nagarajan, A., and van Renesse, R. 2003. User-specified adaptive scheduling in a streaming media network. In Proceedings of the 6th IEEE International Conference on Open Architectures and Network Programming (San Francisco, CA). 87--96.]]

[29]

ISO. 1999. ISO/IEC 9899:1999, International Standard---Programming Languages---C. International Standards Organization, Geneva, Switzerland.]]

[30]

Jim, T., Morrisett, G., Grossman, D., Hicks, M., Cheney, J., and Wang, Y. 2002. Cyclone: A safe dialect of C. In Proceedings of the USENIX Annual Technical Conference (Monterey, CA). 275--288.]]

[31]

Jones, R. and Kelly, P. 1997. Backwards-compatible bounds checking for arrays and pointers in C programs. In Proceedings of the AADEBUG'97. Third International Workshop on Automatic Debugging. Linköping Electronic Articles in Computer and Information Science, vol. 2(9). Linköping, Sweden.]]

[32]

Jones, S. P. and Hughes, J., Eds. 1999. Haskell 98: A Non-Strict, Purely Functional Language. Available online at http://www.haskell.org/onlinereport/.]]

[33]

Kfoury, A. J., Tiuryn, J., and Urzyczyn, P. 1993. Type reconstruction in the presence of polymorphic recursion. ACM Trans. Programm. Lang. Syst. 15, 2 (Apr.), 290--311.]]

[34]

Kowshik, S., Dhurjati, D., and Adve, V. 2002. Ensuring code safety without runtime checks for real-time control systems. In Proceedings of the ACM International Conference on Compilers, Architectures and Synthesis for Embedded Systems (Grenoble, France). 288--297.]]

[35]

Läufer, K. 1996. Type classes with existential types. J. Funct. Programm. 6, 3 (May), 485--517.]]

[36]

Leroy, X. 1992. Unboxed objects and polymorphic typing. In Proceedings of the 19th ACM Symposium on Principles of Programming Languages (Albuquerque, NM). 177--188.]]

[37]

Leroy, X. 1997. The effectiveness of type-based unboxing. In Proceedings of the Workshop on Types in Compilation (Amsterdam, The Netherlands). Also published as Tech. rep. BCCS-97-03. Computer Science Department, Boston College, Boston, MA.]]

[38]

Leroy, X. 2002a. The Objective Caml System Release 3.05, Documentation and User's Manual. Available online at http://caml.inria.fr/ocaml/htmlman/index.html.]]

[39]

Leroy, X. 2002b. Writing efficient numerical code in Objective Caml. Available online at http://caml.inria.fr/ocaml/numerical.html.]]

[40]

Liskov, B. et al. 1984. CLU Reference Manual. Springer-Verlag, Berlin, Germany.]]

[41]

Loginov, A., Yong, S. H., Horwitz, S., and Reps, T. 2001. Debugging via run-time type checking. In 4th International Conference on Fundamental Approaches to Software Engineering. Lecture Notes in Computer Science, vol. 2029. Springer-Verlag, Berlin, Germany, 217--232.]]

[42]

Milner, R., Tofte, M., Harper, R., and MacQueen, D. 1997. The Definition of Standard ML (Revised). MIT Press, Cambridge, MA.]]

[43]

Minamide, Y., Morrisett, G., and Harper, R. 1996. Typed closure conversion. In Proceedings of the 23rd ACM Symposium on Principles of Programming Languages (St. Petersburg, FL). 271--283.]]

[44]

Mitchell, J. 1988. Polymorphic type inference and containment. Inform. Computat. 76, 11--249.]]

[45]

Mitchell, J. and Plotkin, G. 1988. Abstract types have existential type. ACM Trans. Programm. Lang. Syst. 10, 3 (July), 470--502.]]

[46]

Morrisett, G. 1995. Compiling with types. Ph.D. dissertation, Carnegie Mellon University, Pittsburgh, PA.]]

[47]

Morrisett, G., Crary, K., Glew, N., Grossman, D., Samuels, R., Smith, F., Walker, D., Weirich, S., and Zdancewic, S. 1999a. TALx86: A realistic typed assembly language. In Proceedings of the 2nd ACM Workshop on Compiler Support for System Software (Atlanta, GA). 25--35. Published as INRIA Tech. Rep. 0288. (March 1999), Rocquencourt, France.]]

[48]

Morrisett, G., Crary, K., Glew, N., and Walker, D. 2002. Stack-based typed assembly language. J. Funct. Programm. 12, 1 (Jan.), 43--88.]]

[49]

Morrisett, G., Walker, D., Crary, K., and Glew, N. 1999b. From System F to typed assembly language. ACM Trans. Programm. Lang. Syst. 21, 3 (May), 528--569.]]

[50]

Necula, G., McPeak, S., and Weimer, W. 2002. CCured: Type-safe retrofitting of legacy code. In Proceedings of the 29th ACM Symposium on Principles of Programming Languages (Portland, OR). 128--139.]]

[51]

Patel, P. and Lepreau, J. 2003. Hybrid resource control of active extensions. In Proceedings of the 6th IEEE International Conference on Open Architectures and Network Programming (San Francisco, CA). 23--31.]]

[52]

Patel, P., Whitaker, A., Wetherall, D., Lepreau, J., and Stack, T. 2003. Upgrading transport protocols using untrusted mobile code. In Proceedings of the 19th ACM Symposium on Operating System Principles (New York, NY). 1--14.]]

[53]

Pierce, B. 1991. Programming with intersection types and bounded polymorphism. Ph.D. dissertation, Carnegie Mellon University, Pittsburgh, PA.]]

[54]

Pierce, B. and Sangiorgi, D. 2000. Behavioral equivalence in the polymorphic pi-calculus. J. Assoc. Comp. Mach. 47, 3, 531--584.]]

[55]

Pierce, B. and Turner, D. 1998. Local type inference. In Proceedings of the 25th ACM Symposium on Principles of Programming Languages (San Diego, CA). 252--265.]]

[56]

Reynolds, J. 1974. Towards a theory of type structure. In Programming Symposium. Lecture Notes in Computer Science, vol. 19. Springer-Verlag, Berlin, Germany, 408--425.]]

[57]

Reynolds, J. 1983. Types, abstraction and parametric polymorphism. In Information Processing 83. Elsevier Science Publishers, Amsterdam, The Netherlands, 513--523.]]

[58]

Smith, G. and Volpano, D. 1996. Towards an ML-style polymorphic type system for C. In 6th European Symposium on Programming. Lecture Notes in Computer Science, vol. 1058. Springer-Verlag, Berlin, Germany, 341--355.]]

[59]

Smith, G. and Volpano, D. 1998. A sound polymorphic type system for a dialect of C. Sci. Comput. Programm. 32, 2--3, 49--72.]]

[60]

Strachey, C. 1967. Fundamental concepts in programming languages. Unpublished lecture notes, Summer School in Computer Programming, Copenhagen, Denmark. Eventually published in 2003 in High. Ord. Symbol. Computat. 13, 1-2, 5--6.]]

[61]

Stroustrup, B. 2000. The C++ Programming Language, spec. ed. Addison-Wesley, Reading, MA.]]

[62]

Tarditi, D. 1996. Design and implementation of code optimizations for a type-directed compiler for Standard ML. Ph.D. dissertation. Carnegie Mellon University, Pittsburgh, PA.]]

[63]

The GHC Team. 2003. The Glasgow Haskell Compiler User's Guide, Version 6.0. Available online at http://www.haskell.org/ghc.]]

[64]

The Hugs 98 User Manual. 2002. The Hugs 98 User Manual. Available online at http://haskell.cs.yale.edu/hugs.]]

[65]

Tofte, M. 1990. Type inference for polymorphic references. Inform. Computat. 89, 1--34.]]

[66]

Wadler, P. 1989. Theorems for free&excl; In Proceedings of the 4th International Conference on Functional Programming Languages and Computer Architecture. ACM Press, New York, NY, 347--359.]]

[67]

Walker, D. and Morrisett, G. 2000. Alias types for recursive data structures. In Workshop on Types in Compilation. Lecture Notes in Computer Science, vol. 2071. Springer-Verlag, Berlin, Germany, 177--206.]]

[68]

Wells, J. 1999. Typability and type checking in System F are equivalent and undecidable. Ann. Pure Appl. Logic 98, 1--3 (June), 111--156.]]

[69]

Wells, J., Dimock, A., Muller, R., and Turbak, F. 2002. A calculus with polymorphic and polyvariant flow types. J. Funct. Programm. 12, 3 (May), 183--227.]]

[70]

Wright, A. and Felleisen, M. 1994. A syntactic approach to type soundness. Inform. Computat. 115, 1, 38--94.]]

[71]

Xi, H. 2000. Imperative programming with dependent types. In Proceedings of the 15th IEEE Symposium on Logic in Computer Science (Santa Barbara, CA). 375--387.]]

Cited By

Melo LRibeiro RGuimarães BPereira F(2020)Type Inference for CACM Transactions on Programming Languages and Systems10.1145/342147242:3(1-71)Online publication date: 13-Nov-2020
https://dl.acm.org/doi/10.1145/3421472
Chen GDong W(2020)Reactive Jamming and Attack Mitigation over Cross-Technology Communication LinksACM Transactions on Sensor Networks10.1145/341821017:1(1-25)Online publication date: 5-Nov-2020
https://dl.acm.org/doi/10.1145/3418210
Coblenz MOei REtzel TKoronkevich PBaker MBloem YMyers BSunshine JAldrich J(2020)ObsidianACM Transactions on Programming Languages and Systems10.1145/341751642:3(1-82)Online publication date: 25-Nov-2020
https://dl.acm.org/doi/10.1145/3417516
Show More Cited By

Index Terms

Quantified types in an imperative language
1. Software and its engineering
  1. Software notations and tools
    1. Formal language definitions
    2. General programming languages
      1. Language features
        Abstract data types
        Polymorphism
2. Theory of computation
  1. Formal languages and automata theory
  2. Semantics and reasoning
    1. Program constructs
      1. Type structures
    2. Program semantics
      1. Operational semantics

Recommendations

Polymorphic Typestate for Session Types
PPDP '23: Proceedings of the 25th International Symposium on Principles and Practice of Declarative Programming

Session types provide a principled approach to typed communication protocols that guarantee type safety and protocol fidelity. Formalizations of session-typed communication are typically based on process calculi, concurrent lambda calculi, or linear ...
Sound and complete bidirectional typechecking for higher-rank polymorphism with existentials and indexed types

Bidirectional typechecking, in which terms either synthesize a type or are checked against a known type, has become popular for its applicability to a variety of type systems, its error reporting, and its ease of implementation. Following principles from ...
Polymorphic type inference and abstract data types

Many statically typed programming languages provide an abstract data type construct, such as the module in Modula-2. However, in most of these languages, implementations of abstract data types are not first-class values. Thus, they cannot be assigned to ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Transactions on Programming Languages and Systems

ACM Transactions on Programming Languages and Systems Volume 28, Issue 3

May 2006

187 pages

ISSN:0164-0925

EISSN:1558-4593

DOI:10.1145/1133651

Issue’s Table of Contents

Copyright © 2006 ACM.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 May 2006

Published in TOPLAS Volume 28, Issue 3

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

17
Total Citations
View Citations
782
Total Downloads

Downloads (Last 12 months)100
Downloads (Last 6 weeks)20

Reflects downloads up to 12 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Melo LRibeiro RGuimarães BPereira F(2020)Type Inference for CACM Transactions on Programming Languages and Systems10.1145/342147242:3(1-71)Online publication date: 13-Nov-2020
https://dl.acm.org/doi/10.1145/3421472
Chen GDong W(2020)Reactive Jamming and Attack Mitigation over Cross-Technology Communication LinksACM Transactions on Sensor Networks10.1145/341821017:1(1-25)Online publication date: 5-Nov-2020
https://dl.acm.org/doi/10.1145/3418210
Coblenz MOei REtzel TKoronkevich PBaker MBloem YMyers BSunshine JAldrich J(2020)ObsidianACM Transactions on Programming Languages and Systems10.1145/341751642:3(1-82)Online publication date: 25-Nov-2020
https://dl.acm.org/doi/10.1145/3417516
Kougkas ADevarajan HSun X(2020)Bridging Storage Semantics Using Data Labels and Asynchronous I/OACM Transactions on Storage10.1145/341557916:4(1-34)Online publication date: 14-Oct-2020
https://dl.acm.org/doi/10.1145/3415579
Lin DWang QMin WXu JZhang Z(2020)A Survey on Energy-Efficient Strategies in Static Wireless Sensor NetworksACM Transactions on Sensor Networks10.1145/341431517:1(1-48)Online publication date: 12-Oct-2020
https://dl.acm.org/doi/10.1145/3414315
Uphoff CBader M(2020)Yet Another Tensor Toolbox for Discontinuous Galerkin Methods and Other ApplicationsACM Transactions on Mathematical Software10.1145/340683546:4(1-40)Online publication date: 16-Oct-2020
https://dl.acm.org/doi/10.1145/3406835
Jangda ABondhugula U(2020)An Effective Fusion and Tile Size Model for PolyMageACM Transactions on Programming Languages and Systems10.1145/340484642:3(1-27)Online publication date: 8-Nov-2020
https://dl.acm.org/doi/10.1145/3404846
Thies JRöhrig-Zöllner MOvermars NBasermann AErnst DHager GWellein G(2020)PHISTACM Transactions on Mathematical Software10.1145/340222746:4(1-26)Online publication date: 16-Oct-2020
https://dl.acm.org/doi/10.1145/3402227
Moss ASchluntz RBuhr P(2018)C: Adding modern programming language features to CSoftware: Practice and Experience10.1002/spe.262448:12(2111-2146)Online publication date: 20-Aug-2018
https://doi.org/10.1002/spe.2624
Eisenberg RPeyton Jones S(2017)Levity polymorphismACM SIGPLAN Notices10.1145/3140587.306235752:6(525-539)Online publication date: 14-Jun-2017
https://dl.acm.org/doi/10.1145/3140587.3062357
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents