article

Open access

Dynamic typing in a statically typed language

Authors:

Martín Abadi,

Luca Cardelli,

Benjamin Pierce,

Gordon PlotkinAuthors Info & Claims

ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 13, Issue 2

Pages 237 - 268

https://doi.org/10.1145/103135.103138

Published: 01 April 1991 Publication History

PDF eReader

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 datawhose 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]

ATKINSON, M. P., AND BUNEMAN, O. P. Types and persistence in database programming languages. Comput. Surv. 19, 2 (June 1987), 105-190.

Digital Library

Google Scholar

[2]

ATKINSON, M. P., AND MORRISON, R. Polymorphic names and iterations. Draft article, Sept. 1987.

Google Scholar

[3]

BARENDREGT, H.P. The Lambda Calculus. Rev. ed. North-Holland, Amsterdam, 1984.

Google Scholar

[4]

BmR~LL, A. D., AND NELSON, B. J. Implementing remote procedure calls. ACM Trans. Comput. Syst. 2, i (Feb. 1984), 39-59.

Digital Library

Google Scholar

[5]

BmTWISTLE, G. M., DAHL, 0. J., MYHRHAUG, B., AND NYGAARD, K. S~mula Begin. Studentlitteratur, Lund, Sweden, 1979.

Google Scholar

[6]

BORRAS, P., CLEMENT, D., DESPEYROUX, T., INCERPI, J., KAHN, G., LANG, B., AND PASCUAL, V. CENTAUR: The system. In Proceedings of the 3rd Annual Symposium on Software Development Environments (SIGSOFT88) (Boston, Mass., Nov.). ACM, New York, 1988.

Digital Library

Google Scholar

[7]

CARDELLI, L. Amber. In Combinators and Functional Programming Languages, G. Cousineau, P. L. Curien, and B. Robinet, Eds. Lecture Notes in Computer Science, vol. 242. Springer-Verlag, New York, 1986.

Digital Library

Google Scholar

[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).

Google Scholar

[9]

CARDELLI, L., AND WEGNER, P. On understanding types, data abstraction, and polymorphism. Comput. Surv. 17, 4 (Dee. 1985), 471-522.

Digital Library

Google Scholar

[10]

CARDELLI, L., DONAHUE, J., JORDAN, M., KALSOW, B., AND NELSON, G. The Modula-3 type system. In Proceedings of the 16th Annual ACM Symposium on Princ~ples of Programming Languages (Austin, Tex., Jan. 11-13, 1989). ACM, New York, pp. 202-212.

Digital Library

Google Scholar

[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.

Google Scholar

[12]

CHURCH, A. A formulation ofthe simple theory of types. J Symbohc Logic 5 (1940), 56-68.

Crossref

Google Scholar

[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.

Google Scholar

[14]

DESPEYROUX, T. Typoh A formalism to implement natural semanties. Teeh. Rep. 94, INRIA, Mar. 1988.

Google Scholar

[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.

Google Scholar

[16]

HINDLEY, J. R., AND SELDIN, J. P. Introduction to Combinators and x-Calculus. London Mathematical Society Student Texts, vol. 1. Cambridge University Press, New York, 1986.

Digital Library

Google Scholar

[17]

KAH~, G. Natural Semantics. Programming of Future Generation Computers, K. Fuchi and M. Nivat, Eds., Elsevier, (North-Holland), Amsterdam, 1988, pp. 237-258.

Digital Library

Google Scholar

[18]

LAMPSON, B. A description of the Cedar language. Tech. Rep. CSL-8345, Xerox Pale Alto Research Center, Palo Alto, Calif., 1983.

Google Scholar

[19]

LISKOV, B., ATKINSON, R., BLOOM, T, MOSS, E., SCHAFFERT, J. C., SCItEIFLER, R. AND SNYDER, A. CLU Reference Manual. Springer-Verlag, New York, 1981.

Digital Library

Google Scholar

[20]

MACQUEEN, D., PLOTKIN, G., AND SETHI, e. An idea} model for recursive polymorphic types. Inf. Control, 71 (1986), 95-130.

Digital Library

Google Scholar

[21]

MARTIN-L"F, P. Intitutionistic Type Theory. Bibliopolis, Naples, 1984.

Google Scholar

[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.

Google Scholar

[23]

MILNER, R. A theory of type polymorphism in programming. J. Comput. Syst. Sci. 17 (Aug. 1978), 348-375.

Crossref

Google Scholar

[24]

MILNER, R., TOFTE, M., AND HARPER, R. The Definition of Standard ML. MIT Press, Cambridge, Mass., 1990.

Digital Library

Google Scholar

[25]

MITCHELL, J., AND PLOTKIN, G. Abstract types have existential type. ACM Trans. Prograin. Lang. Syst. 10, 3 (July 1988), 470-502.

Digital Library

Google Scholar

[26]

MYCROFT, A. Dynamic types in ML. Draft article, 1983.

Google Scholar

[27]

NEWCOMER, J.M. Efficient binary I/O of IDL objects. SIGPLAN Not. (ACM) 22, 11 (Nov. 1987), 35-42.

Digital Library

Google Scholar

[28]

PLOTKIN, G. Call-by-name, call-by-value, and the X-calculus. Theor. Comput. Sci. I (1975), 125-159.

Crossref

Google Scholar

[29]

PLOTKIN, G.D. A structural approach to operational semantics. Tech. Rep. DAIMI FN-19, Computer Science Dept., Aarhus Univ., Aarhus, Denmark, 1981.

Google Scholar

[30]

RE~NOLDS, J. Three approaches to type structure. In Mathemat~cal Foundatlons of Software Development, H. Ehrig, C Florol, M. Nivat, and J. Thatcher, Eds. Lecture Notes in Computer Science, vol. 185. Springer-Verlag, New York, 1985.

Digital Library

Google Scholar

[31]

ROVNER, P. On extending Modula-2 to build large, integrated systems IEEE Softw. 3, 6 (Nov. 1986), 46-57.

Digital Library

Google Scholar

[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).

Google Scholar

[33]

SCHEIFLER, R. W. A denotational semantics of CLU. Master's thesis, MIT, Cambridge, Mass., May 1978 (Tech. Rep. MIT/LCS/TR-201).

Digital Library

Google Scholar

[34]

T~A~TE, S. R. Quasi-static typing (preliminary report), In Proceed~ngs of the 17th ACM Symposium on Principles ofProgramm~ng Languages. ACM, New York, 1990, pp. 367-381.

Digital Library

Google Scholar

[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).

Google Scholar

[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.

Google Scholar

Cited By

View all

YE WOLIVEIRA B(2024)Type-directed operational semantics for gradual typingJournal of Functional Programming10.1017/S095679682400007834Online publication date: 26-Sep-2024
https://doi.org/10.1017/S0956796824000078
Wolfengagen VKosikov SSlieptsov I(2024)A Cognitive Type System Simulation by a Dynamically Typed LanguageProcedia Computer Science10.1016/j.procs.2018.11.069145:C(641-645)Online publication date: 12-Apr-2024
https://dl.acm.org/doi/10.1016/j.procs.2018.11.069
Labrada EToro MTanter É(2022)Gradual System FJournal of the ACM10.1145/355598669:5(1-78)Online publication date: 28-Oct-2022
https://dl.acm.org/doi/10.1145/3555986
Show More Cited By

Index Terms

Dynamic typing in a statically typed language
1. Theory of computation
  1. Semantics and reasoning
    1. Program constructs
      1. Type structures
    2. Program semantics

Recommendations

Typing dynamic typing
ICFP '02: Proceedings of the seventh ACM SIGPLAN international conference on Functional programming

Even when programming in a statically typed language we every now and then encounter statically untypable values; such values result from interpreting values or from communicating with the outside world. To cope with this problem most languages include ...
Dynamic typing in a statically-typed language
POPL '89: Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages

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, ...
Ad-hoc polymorphism and dynamic typing in a statically typed functional language
WGP '10: Proceedings of the 6th ACM SIGPLAN workshop on Generic programming

Static typing in functional programming languages such as Clean, Haskell, and ML is highly beneficial: it prevents erroneous behaviour at run time and provides opportunities for optimisations. However, dynamic typing is just as important as sometimes ...

Reviews

Reviewer: Ramaswamy Ramanujam

Checking type correctness of operations often becomes ne cessary at runtime: consider, for example, the read operation. In this paper, the authors propose the use of a data type called Dynamic. Values of this type are pairs—each pair consists of an object and its type. Thus one keeps track of representations of data objects as well as those of their types. The authors introduce a language construct dynamic for packaging a value together with its type into a Dynamic object, and a typecase construct for inspecting the type tag of a given Dynamic object. The language used is basically lambda calculus (simply typed). The paper gives a clear presentation of transition system–style operational semantics, and of ideal model-based denotational semantics. Suggestions are included for extending the theory to polymorphic lambda calculus, and implementation issues are discussed somewhat sketchily. The paper also includes a short history of various attempts to introduce dynamic typing mechanisms. The most important contribution of this paper lies in providing a rigorous and thorough study of an essential programming language feature that has had an informal existence for a long time. This paper should also serve as a guideline to programming language designers on the right questions to ask when introducing a new language construct.

Access critical reviews of Computing literature here

Become a reviewer for Computing Reviews.

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 13, Issue 2

April 1991

114 pages

ISSN:0164-0925

EISSN:1558-4593

DOI:10.1145/103135

Editor:
Susan L. Graham
Univ. of California at Berkley

Issue’s Table of Contents

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 April 1991

Published in TOPLAS Volume 13, Issue 2

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tag

theory

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

208
Total Citations
View Citations
1,669
Total Downloads

Downloads (Last 12 months)195
Downloads (Last 6 weeks)18

Reflects downloads up to 13 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

YE WOLIVEIRA B(2024)Type-directed operational semantics for gradual typingJournal of Functional Programming10.1017/S095679682400007834Online publication date: 26-Sep-2024
https://doi.org/10.1017/S0956796824000078
Wolfengagen VKosikov SSlieptsov I(2024)A Cognitive Type System Simulation by a Dynamically Typed LanguageProcedia Computer Science10.1016/j.procs.2018.11.069145:C(641-645)Online publication date: 12-Apr-2024
https://dl.acm.org/doi/10.1016/j.procs.2018.11.069
Labrada EToro MTanter É(2022)Gradual System FJournal of the ACM10.1145/355598669:5(1-78)Online publication date: 28-Oct-2022
https://dl.acm.org/doi/10.1145/3555986
Devriese DPatrignani MPiessens F(2022)Two Parametricities Versus Three Universal TypesACM Transactions on Programming Languages and Systems10.1145/353965744:4(1-43)Online publication date: 21-Sep-2022
https://dl.acm.org/doi/10.1145/3539657
Blanvillain OBrachthäuser JKjaer MOdersky M(2022)Type-level programming with match typesProceedings of the ACM on Programming Languages10.1145/34986986:POPL(1-24)Online publication date: 12-Jan-2022
https://dl.acm.org/doi/10.1145/3498698
Lubbers M(2022)Deep Embedding with ClassTrends in Functional Programming10.1007/978-3-031-21314-4_3(39-58)Online publication date: 17-Mar-2022
https://dl.acm.org/doi/10.1007/978-3-031-21314-4_3
Viering MHu REugster PZiarek L(2021)A multiparty session typing discipline for fault-tolerant event-driven distributed programmingProceedings of the ACM on Programming Languages10.1145/34855015:OOPSLA(1-30)Online publication date: 15-Oct-2021
https://dl.acm.org/doi/10.1145/3485501
Krauter NRaaf PBraam PSalkhordeh RErdweg SBrinkmann A(2021)Persistent software transactional memory in HaskellProceedings of the ACM on Programming Languages10.1145/34735685:ICFP(1-29)Online publication date: 19-Aug-2021
https://dl.acm.org/doi/10.1145/3473568
Greenwood-Thessman EGariano IRoberts RMarr SHomer MNoble JSeaton CFlückiger O(2021)Naïve transient cast insertion isn't (that) badProceedings of the 16th ACM International Workshop on Implementation, Compilation, Optimization of OO Languages, Programs and Systems10.1145/3464972.3472395(1-9)Online publication date: 13-Jul-2021
https://dl.acm.org/doi/10.1145/3464972.3472395
SIEK JTHIEMANN PWADLER P(2021)Blame and coercion: Together again for the first timeJournal of Functional Programming10.1017/S095679682100010131Online publication date: 13-Oct-2021
https://doi.org/10.1017/S0956796821000101
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

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

Abstract

References

Cited By

Index Terms

Recommendations

Typing dynamic typing