Dynamic typing in a statically typed language

ABSTRACT

Statically typed programming languages allow earlier error checking, better enforcement of diciplined programming styles, and the generation of more efficient object code than languages where all type consistency checks are performed at run time. However, even in statically typed languages, there is often the need to deal with data whose type cannot be determined 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 explores the syntax, operational semantics, and denotational semantics of a simple language that includes the type Dynamic. We give examples of how dynamically typed values can 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: ATKINSON, M. P., AND MORRISON, R. Polymorphic names and iterations. Draft article, Sept. 1987.
• 3: BARENDREGT, H.P. The Lambda Calculus. Rev. ed. North-Holland, Amsterdam, 1984.
• 4: Andrew D. Birrell , Bruce Jay Nelson, Implementing remote procedure calls, ACM Transactions on Computer Systems (TOCS), v.2 n.1, p.39-59, February 1984 [doi>10.1145/2080.357392]
• 5: BmTWISTLE, G. M., DAHL, 0. J., MYHRHAUG, B., AND NYGAARD, K. S~mula Begin. Studentlitteratur, Lund, Sweden, 1979.
• 6: P. Borras , D. Clement , Th. Despeyroux , J. Incerpi , G. Kahn , B. Lang , V. Pascual, Centaur: the system, Proceedings of the third ACM SIGSOFT/SIGPLAN software engineering symposium on Practical software development environments, p.14-24, November 28-30, 1988, Boston, Massachusetts, United States
• 7: L Cardelli, Amber, Proc. of the thirteenth spring school of the LITP on Combinators and functional programming languages, p.21-47, October 1986, Val d'Ajol, France
• 8: CARDELLI, L., AND MACQUEEN, D. Persistence and type abstraction. In Proceedings of the Persistence and Datatypes Workshop (St. Andrews, Scotland, Aug. 1985). Dept. of Computational Science, Univ. of St. Andrews, 1985 (Persistent Program. Res. Rep. 16).
• 9: Luca Cardelli , Peter Wegner, On understanding types, data abstraction, and polymorphism, ACM Computing Surveys (CSUR), v.17 n.4, p.471-523, Dec. 1985 [doi>10.1145/6041.6042]
• 10: 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]
• 11: CARDELLI, L., DONAHUE, J., GLASSMAN, L., JORDAN, M., KALSOW, B., AND NELSON, G. Modula-3 report (revised). Res. rep. 52, DEC Systems Research Center, Palo Alto, Calif., Nov. 1989.
• 12: CHURCH, A. A formulation ofthe simple theory of types. J Symbohc Logic 5 (1940), 56-68.
• 13: CL~MENT, D., DESPEYROUX, J., DESPEYROUX, T., HASCOET, L., AND KAHN, G. Natural semantics on the computer. Tech. Rep. RR 416, INRIA, Sophia-Antipolis June 1985.
• 14: DESPEYROUX, T. Typoh A formalism to implement natural semanties. Teeh. Rep. 94, INRIA, Mar. 1988.
• 15: HARPER, R. Introduction fo Standard ML. Teeh. Rep. ECS-LFCS-86-14, Lab. for the Foundations of Computer Science, Edinburgh Univ., Edinburgh, Scotland, Sept. 1986.
• 16: J. Roger Hindley , Jonathan P. Seldin, Introduction to combinators and &lgr;-calculus, Cambridge University Press, New York, NY, 1986
• 17: G. Kahn, Natural Semantics, Proceedings of the first Franco-Japanese Symposium on Programming of future generation computers, p.237-257, August 1988, Tokyo, Japan
• 18: LAMPSON, B.. A description of the Cedar language. Tech. Rep. CSL-8345, Xerox Pale Alto Research Center, Palo Alto, Calif., 1983.
• 19: 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
• 20: 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]
• 21: MARTIN-L"F, P. Intitutionistic Type Theory. Bibliopolis, Naples, 1984.
• 22: McDONALD, D. B., FAHLMAN, S. E., AND WHOLEY, S. Internal design of CMU Common Lisp un the IBM RT PC. Tech. Rep. CMU-CS-87-157, Carnegie-Mellon Univ., School of Computer Science, Pittsburgh, Pa., Apr. 1988.
• 23: MILNER, R. A theory of type polymorphism in programming. J. Comput. Syst. Sci. 17 (Aug. 1978), 348-375.
• 24: Robin Milner , Mads Tofte , Robert Harper, The definition of Standard ML, MIT Press, Cambridge, MA, 1990
• 25: John C. Mitchell , Gordon D. Plotkin, Abstract types have existential type, ACM Transactions on Programming Languages and Systems (TOPLAS), v.10 n.3, p.470-502, July 1988 [doi>10.1145/44501.45065]
• 26: MYCROFT, A. Dynamic types in ML. Draft article, 1983.
• 27: 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]
• 28: PLOTKIN, G. Call-by-name, call-by-value, and the X-calculus. Theor. Comput. Sci. I (1975), 125-159.
• 29: PLOTKIN, G.D. A structural approach to operational semantics. Tech. Rep. DAIMI FN-19, Computer Science Dept., Aarhus Univ., Aarhus, Denmark, 1981.
• 30: J C Reynolds, Three approaches to type structure, Proc. of the international joint conference on theory and practice of software development (TAPSOFT) Berlin, March 25-29, 1985 on Mathematical foundations of software development, Vol. 1: Colloquium on trees in algebra and programming (CAAP'85), p.97-138, April 1985, Berlin, Germany
• 31: ROVNER, P. On extending Modula-2 to build large, integrated systems IEEE Softw. 3, 6 (Nov. 1986), 46-57.
• 32: SCHAFFERT, J. C. A formal definition of CLU. Master's thesls, MIT, Dept. of Computer Science, Cambridge, Mass., Jan. 1978 (Tech. Rep. MIT/LCS/TR-193).
• 33: R. Scheifler, A DENOTATIONAL SEMANTICS OF CLU, Massachusetts Institute of Technology, Cambridge, MA, 1978
• 34: Satish Thatte, Quasi-static typing, Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.367-381, December 1989, San Francisco, California, United States [doi>10.1145/96709.96747]
• 35: TOFTE, M. Operational semantics and polymorphic type inference. Ph.D. thesis, Computer Science Dept., Edinburgh Univ., Edinburgh, Scotland, 1988 (Tech. Rep. CST-52-88).
• 36: WEm, P., APO~TE, M.-V., LAWLLE, A., MAUXY, M., A~D SU~REZ, A. The CAML reference manual, Version 2.6. Tech. Rep., Projet Formel, INRIA-ENS, Paris, 1989.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs
          Subjects: Type structure

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS

General Terms:
Design, Languages, Theory

Keywords:
theory