Dynamic typing in a statically-typed language

ABSTRACT

Statically-typed programming languages allow earlier error checking, better enforcement of disciplined programming styles, and generation of more efficient object code than languages where all type-consistency checks are performed at runtime. However, even in statically-type languages, there is often the need to deal with data whose type cannot be known at compile time. To handle such situations safely, we propose to add a type Dynamic whose values are pairs of a value v and a type tag T where v has the type denoted by T. Instances of Dynamic are built with an explicit tagging construct and inspected with a type-safe typecase construct. This paper is an exploration of the syntax, operational semantics, and denotational semantics of a simple language with the type Dynamic. We give examples of how dynamically-typed values might be used in programming. Then we discuss an operational semantics for our language and obtain a soundness theorem. We present two formulations of the denotational semantics of this language and relate them to the operational semantics. Finally, we consider the implications of polymorphism and some implementation issues.

REFERENCES

• 1: Malcolm P. Atkinson , O. Peter Buneman, Types and persistence in database programming languages, ACM Computing Surveys (CSUR), v.19 n.2, p.105-170, June 1987 [doi>10.1145/62070.45066]
• 2: Malcolm P. Atkinson and Ronald Morrison. Polymorphic names and iterations. September 1987. Draft article.
• 3: H. P. Barendregt. The Lambda Ualculus. North Holland, Revised edition, 1984.
• 4: Graham M. Birtwistle, Ole-Johan Dahl, Bjorn Myhrhaug, and Kristen Nygaard. Sim ula Begirt. Studentlitteratur (Lund, Sweden)~ Bratt Institute Fuer Neues Lerned (Goch, FRG), Chartwell- Bratt Ltd (Kent, England}, 1979.
• 5: Luca Cardelli. Amber. In Guy Cousineau, Pierre-Louis Curien, and Bernard Robinet, editors, Combinators and Functional Programming Languages, Springer-Verlag, 1986. Lecture Notes in Computer Science No. 242.
• 6: Luca Cardelli, James Donahue, Lucille Glassman, Mick Jordan, Bill Kalsow, and Greg Nelson. Modula-3 Report. TechnicalReport 31, DEC Systems Research Center, 1988.
• 7: L. Cardelli , J. Donahue , M. Jordan , B. Kalsow , G. Nelson, The Modula–3 type system, Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.202-212, January 11-13, 1989, Austin, Texas, United States [doi>10.1145/75277.75295]
• 8: Luca CardeUi and David MaeQueen. Persistence and type abstraction. In Proceedin9~ of the Persiste~ee and Datatypes Workshop, August 1985. Proceedings published as University of St. Andrews, Department of Computational Science, Persistent Programming Research Report 16.
• 9: Alonzo Church. A formulation of the simple the- 1940.
• 10: Dominique Clement, Jo~lle Despeyroux, Thierry Despeyrous, and Gilles Kahn. A simple applica. rive language: mini-ML. Draft article {INRIA).
• 11: Jo~lle Despeyroux. Proof of translation in natural semantics. Draft article (INRIA).
• 12: Mike Gordon. Adding Eval to ML. circa 1980. Personal communication.
• 13: Robert Harper, Robin Milner, and Muds Tofte. The Semantics of Standard ML: Version I. Technical Report ECS-LFCS-87-36, Computer Science Department, University of Edinburgh, 1987.
• 14: J. Roger Hindley , Jonathan P. Seldin, Introduction to combinators and &lgr;-calculus, Cambridge University Press, New York, NY, 1986
• 15: Gilles Kahn, Dominique Cl6ment, Jo~lle Despeyroux, Thierry Despeyrous, and Laurent Hascoet. Natural semantics on the computer. Draft article (INRIA).
• 16: Butler Lampson. A Description of the Cedar Language. Technical Report CSL-83-15, Xerox Palo Alto Research Center, 1983.
• 17: B Liskov , E Moss , A Snyder , R Atkinson , J C. Schaffert , T Bloom , R Scheifler, CLU reference manual, Springer-Verlag New York, Inc., New York, NY, 1984
• 18: David MacQueen , Gordon Plotkin , Ravi Sethi, An ideal model for recursive polymorphic types, Information and Control, v.71 n.1-2, p.95-130, Oct/Nov. 1986 [doi>10.1016/S0019-9958(86)80019-5]
• 19: Per Martin-LSf. Intuitionistic Type Theory. Bibliopolis, 1984.
• 20: David B. McDonald, Scott E. Fahlman, and Skef Wholey. Internal Design of CMU Common Lisp on the IBM RT PC. Technical Report CMU-CS- 87-157, Carnegie Mellon University, April 1988.
• 21: Robin Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences, 1978.
• 22: Alan Mycroft. Dynamic types in ML. 1983. Draft article.
• 23: J. M. Newcomer, Efficient binary I/O of IDL objects, ACM SIGPLAN Notices, v.22 n.11, p.35-43, Nov. 1987 [doi>10.1145/39305.39309]
• 24: Gordon Plotkin. Call-by-name, call-by-value, and the A-calculus. Theoretical Computer Science, 1:125-159, 1975.
• 25: Gordon D. Plotkin. A Structural Approach to Operational Semantics. Technical Report DAIMI FN-19, Computer Science Department, Aarhus University, Aarhus, Denmark, 1981.
• 26: John Reynolds. Three approaches to type structure. In Mathematical Foundations of Software Development, Springer-Verlag, 1985. Lecture Notes in Computer Science No. 185.
• 27: Paul Rovner, Roy Levin, and John Wick. On Extending Modula-~ for Building Large, Integrated Systems. Technical Report Technical Report 3, Digital Systems Research Center, 1985.
• 28: Muds Tofte. Operational Semantics and Polymorphic Type Inference. PhD thesis, Computer Science Department, Edinburgh University, 1988. CST-52-88.

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Data types and structures

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Operational semantics; Denotational semantics

General Terms:
Design, Languages