More Web Proxy on the site http://driver.im/

Article

Free access

Dynamic typing in a statically-typed language

Authors:

G. PlotkinAuthors Info & Claims

POPL '89: Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Pages 213 - 227

https://doi.org/10.1145/75277.75296

Published: 03 January 1989 Publication History

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 and O. Peter Buneman. Types and persistence in database programming languages. Computing Surveys, 19(2):105-190, June 1987.]]

Digital Library

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

Digital Library

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

Digital Library

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

Luca Cardelli, James Donahue, Mick Jordan, Bill Kalsow, and Greg Nelson. The modula-3 type system. In Proceedinos of the Sixteenth Annual A CM Symposium on Principles of Programmin9 Lanouaoes, January 1989.]]

Digital Library

[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 and Jonathan P. Seldin. introduction to Combinator8 and A-Calculus. Cambridge University Press, 1986. London Mathematical Society Student Texts: i.]]

Digital Library

[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, R. Atkinson, T. Bloom, E. Moss, J.C. Schaffert, R. Scheifler, and A. Snyder. CLU Reference Manual. Springer-Verlag, 1981.]]

Digital Library

[18]

David MacQueen, Gordon Plotkin, and Ravi Sethi. An ideal model for recursive polymorphic types. Information and Control, 71:95-130, 1986.]]

Digital Library

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

Joseph M. Newcomer. Efficient binary I/O of IDL objects. SIGPLAN Notices, 22(11):35-42, November 1987.]]

Digital Library

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

Digital Library

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

Cited By

Ye WOliveira B(2023)Pragmatic Gradual Polymorphism with ReferencesProgramming Languages and Systems10.1007/978-3-031-30044-8_6(140-167)Online publication date: 22-Apr-2023
https://dl.acm.org/doi/10.1007/978-3-031-30044-8_6
Mooij A(2022)Static type checking without downcast operatorInformation Processing Letters10.1016/j.ipl.2022.106285(106285)Online publication date: May-2022
https://doi.org/10.1016/j.ipl.2022.106285
Zhang MAlawneh ARogers TSherwood TBerger EKozyrakis C(2021)Judging a type by its pointer: optimizing GPU virtual functionsProceedings of the 26th ACM International Conference on Architectural Support for Programming Languages and Operating Systems10.1145/3445814.3446734(241-254)Online publication date: 19-Apr-2021
https://dl.acm.org/doi/10.1145/3445814.3446734
Show More Cited By

Index Terms

Dynamic typing in a statically-typed language
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language features
        Data types and structures
2. Theory of computation
  1. Semantics and reasoning
    1. Program semantics
      1. Denotational semantics
      2. Operational semantics

Recommendations

Dynamic typing in a statically typed language

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

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

POPL '89: Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages

January 1989

352 pages

ISBN:0897912942

DOI:10.1145/75277

Editor:
CORPORATE New York, NY Association for Computing Machinery

Copyright © 1989 ACM.

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]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 03 January 1989

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Conference

POPL89

Sponsor:

POPL89: Symposium on the Principles of Programming Languages

January 11 - 13, 1989

Texas, Austin, USA

Acceptance Rates

POPL '89 Paper Acceptance Rate 30 of 191 submissions, 16%;

Overall Acceptance Rate 824 of 4,130 submissions, 20%

Upcoming Conference

POPL '25

Sponsor:
sigplan

The 52nd Annual ACM SIGPLAN Symposium on Principles of Programming Languages

January 19 - 25, 2025

Denver , CO , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

63
Total Citations
View Citations
736
Total Downloads

Downloads (Last 12 months)109
Downloads (Last 6 weeks)19

Reflects downloads up to 24 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Ye WOliveira B(2023)Pragmatic Gradual Polymorphism with ReferencesProgramming Languages and Systems10.1007/978-3-031-30044-8_6(140-167)Online publication date: 22-Apr-2023
https://dl.acm.org/doi/10.1007/978-3-031-30044-8_6
Mooij A(2022)Static type checking without downcast operatorInformation Processing Letters10.1016/j.ipl.2022.106285(106285)Online publication date: May-2022
https://doi.org/10.1016/j.ipl.2022.106285
Zhang MAlawneh ARogers TSherwood TBerger EKozyrakis C(2021)Judging a type by its pointer: optimizing GPU virtual functionsProceedings of the 26th ACM International Conference on Architectural Support for Programming Languages and Operating Systems10.1145/3445814.3446734(241-254)Online publication date: 19-Apr-2021
https://dl.acm.org/doi/10.1145/3445814.3446734
Vorreiter Pedersen MAskarov A(2019)Static Enforcement of Security in Runtime Systems2019 IEEE 32nd Computer Security Foundations Symposium (CSF)10.1109/CSF.2019.00030(335-33515)Online publication date: Jun-2019
https://doi.org/10.1109/CSF.2019.00030
Grimmer MSchatz RSeaton CWürthinger TLuján MMössenböck H(2018)Cross-Language Interoperability in a Multi-Language RuntimeACM Transactions on Programming Languages and Systems10.1145/320189840:2(1-43)Online publication date: 28-May-2018
https://dl.acm.org/doi/10.1145/3201898
Canino ALiu Y(2017)Proactive and adaptive energy-aware programming with mixed typecheckingACM SIGPLAN Notices10.1145/3140587.306235652:6(217-232)Online publication date: 14-Jun-2017
https://dl.acm.org/doi/10.1145/3140587.3062356
Vitousek MSwords CSiek J(2017)Big types in little runtime: open-world soundness and collaborative blame for gradual type systemsACM SIGPLAN Notices10.1145/3093333.300984952:1(762-774)Online publication date: 1-Jan-2017
https://dl.acm.org/doi/10.1145/3093333.3009849
Canino ALiu YCohen AVechev M(2017)Proactive and adaptive energy-aware programming with mixed typecheckingProceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/3062341.3062356(217-232)Online publication date: 14-Jun-2017
https://dl.acm.org/doi/10.1145/3062341.3062356
Vitousek MSwords CSiek JCastagna GGordon A(2017)Big types in little runtime: open-world soundness and collaborative blame for gradual type systemsProceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages10.1145/3009837.3009849(762-774)Online publication date: 1-Jan-2017
https://dl.acm.org/doi/10.1145/3009837.3009849
Sekiyama TIgarashi AGreenberg M(2017)Polymorphic Manifest Contracts, Revised and ResolvedACM Transactions on Programming Languages and Systems10.1145/299459439:1(1-36)Online publication date: 6-Feb-2017
https://dl.acm.org/doi/10.1145/2994594
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

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 Publication

Media

Figures

Other

Tables

View Table of Contents