Article

Free access

Dynamic typing as staged type inference

Authors:

Simon Peyton JonesAuthors Info & Claims

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

Pages 289 - 302

https://doi.org/10.1145/268946.268970

Published: 21 January 1998 Publication History

Abstract

Dynamic typing extends statically typed languages with a universal datatype, simplifying programs which must manipulate other programs as data, such as distributed, persistent, interpretive and generic programs. Current approaches, however, limit the use of polymorphism in dynamic values, and can be syntactically awkward.We introduce a new approach to dynamic typing, based on staged computation, which allows a single type-reconstruction algorithm to execute partly at compile time and partly at run-time. This approach seamlessly extends a single type system to accommodate types that are only known at run-time, while still supporting both type inference and polymorphism. The system is significantly more expressive than other approaches. Furthermore it can be implemented efficiently; most of the type inference is done at compile-time, leaving only some residual unification for run-time.We demonstrate our approach by examples in a small polymorphic functional language, and present its type system, type reconstruction algorithm, and operational semantics. Our proposal could also be readily adapted to many other programming languages.

References

[1]

M. Abadi, L. Cardelli, B. Pierce, and G. Plotkin. Dynamic typing in a statically typed language. A CM Transactions on Programming Lan9uages and Systems, 13(2):237-268, Apr I99I.

Digital Library

[2]

M. Abadi, L. Cardelli, B. Pierce, and D. R&ny. Dynamic typing in polymorphic languages. Journal of Functional Programming, 5(1):111-130, Jan 1995.

[3]

A. Aiken and E. L. Wimmers. Type inclusion constraints and type iafexence. In Proceedings of the A CM SIGPLAN Conference on Fundional Programming Languages and Computer Architecture, pages 31- 41, 1993.

Digital Library

[4]

A. Aiken, E. L. Wimmers, and T. K. Lakshman. Soft typing with conditional types. In Proceedings of the Twenty-First Annual A CM Symposium on Principles of Programming Languages, Portland, Oregon, pages 163- 173, 1994.

Digital Library

[5]

It. Barendregt. Introduction to generalized type systems. Journal of Functional Programming, 1(2):125- 154, 1991.

[6]

H. P. Barendregt. Lambda calculi with types. In S. Abramsky, D. M. Gabbay, and T. S. tg. Maibaum, editors, Handbook of Logic in Computer Science, volume 2, chapter 2, pages 117-309. Oxford Science Publishers, 1992.

Digital Library

[7]

L. Cardelli, S. Martini, J. C. Mitchell, and A. Scedrov. An extension of system F with subtyping. Information and Computation, 109(1/2):4-56, 1994.

Digital Library

[8]

It. Cartwright and M. Fagan. Soft typing. In A CM SIGPLAN-91 Conference on Programmin9 Language Design and Implementation, Toronto, Ontario, pages 278-292. ACM Press, Jun 1991.

Digital Library

[9]

R. Davies. A temporal logic approach to bindingtime analysis. In E. Clarke, editor, Proceedings of the Eleventh Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, pages 184- 195. IEEE Computer Society Press, 3ul 1996.

Digital Library

[10]

tL Davies and F. Pfenning. A modal analysis of staged computation. In Proceedings of the 23rd Annual A CM SIQPLAN-SIGACT Symposium on Principles of Programming Languages, St. Petersburg Beach, Florida, pages 258-270. ACM Press, Jan 1996.

Digital Library

[11]

C. Dubois, F. Rouaix, and P. Weis. Extensional polymorphism. In Proceedings of th~ ~nd Annual A CM SIGPLAN-SIGAGT Symposium on Principles of Programming Languages, San 1Wancisco, California, pages 118-129. ACM Press, Jan 1995.

Digital Library

[12]

J.-Y. Girard. The system F of variable types, Fifteen years later. In G. Huet, editor, Logical Foundations of Functional Programming, The UT Year of Programruing Series, chapter 6. Addison-Wesley, 1990.

Digital Library

[13]

J. Hatcliff and O. Danvy. Thunks and the lambdacalculus. Journ'al of Functional Programming, 7(3):303- 319, May 1997.

Digital Library

[14]

F. Henglein and J. Rehof. Safe polymorphic type inference for a dynamically '~yped language: Trauslating Scheme to ML. In Proceedings of the A CM SIGPLAN Conference on Runctional Programming Languages and Computer Arehitedure, pages 192-203. ACM Press, Jun 1995.

Digital Library

[15]

N. D. Jones, C. K. Gomard, and P. SestofL Partial E~aluation and Automatic Program Generation. Prentice Hall Iaxtexnational, 1993.

Digital Library

[16]

P. Lee and M. Leone. Optimizing ML with rua-time code generation. In A CM SIGPLAI~-#a Conference on Programming Language Design and Implementation, pages 137-148, Philadelphia, Penasylvaaia, May 1996.

Digital Library

[17]

X. Leroy and M. Maamy. Dynamics in ML. Journal of .b'~netionaI Programming, 3(4):431-463, 1993.

[18]

Microsoft. The component object model specification. Technical report, Microsoft Corporation, 1995. o

[19]

R. Milner. A theory of type polymorphism in programming. Journal. of Computer and System Sciences, 17:348-375, 1978.

[20]

E. Moggi. A categorical accoun~ of two-level languages. In Proceedings of the Thirteenfh Annual Conference on Mathematical Foundations of Programmiz9 Semantics, Electronic No~es in Theoretical Computer Science Volume 6. Blsevier Science Publishers, 1997.

[21]

A. Mycroft. Dyn.amic types in ML. (unpublished drafe article), 1983.

[22]

F. Nielson and H. tL Nielsom Tuw-levet Functional Languages. Cambridge University Press, 1992.

Digital Library

[23]

M. Odersky and K. L~iufer. Pu~t~g type annotations to work. In Proceedings of the 23rd Annual A GM SIGPLAN-SIGAGT Symposium on Principles of Programming Languages, St. Petersburg Beach, Flo~ida, pages 54-67. ACM Press, Jan 1996.

Digital Library

[24]

J. Paterson and K. Hammond. Report or~ the Programming Language Haskell (Version 1.4), Apt 1997.

[25]

M. Shields, "i". Sheaxd, and S. Pey~on Jones. Dynamic typing as staged type inference. Technical Report TR.-I997-26, University of Glasgow, Depar~men~ of Computing Science, Aug 1997. Available from http: //~. des. gla. ac. uk/'rab s/pub / t r_97.26, ps, gz,

[26]

W. Taha and T. Shear& Mul~i-s~age programming with explicit annotations. In Partial Bvaluation and Se. mantles Based Program Analysis, pages 203-217, A0M Press, 1997'.

Digital Library

[27]

P. Wader and S. Blo~. How to make ad.hoc polymorphism less ad hoc. In Proceedings of the Six~eenD~ Annual A GM Symposium on Principles of Programming Languages, pages 60-76, 1989.

Digital Library

[28]

A. K. Wrigh~ and M. Felleisen. A syntactic approach to type soundness. Information and Computalion~ 115(1):38-94, Nov 1994.

Digital Library

Cited By

Miyazaki YSekiyama TIgarashi A(2019)Dynamic type inference for gradual Hindley–Milner typingProceedings of the ACM on Programming Languages10.1145/32903313:POPL(1-29)Online publication date: 2-Jan-2019
https://dl.acm.org/doi/10.1145/3290331
ZAKIAN TMCDONELL TCIMINI MNEWTON R(2018)Ghostbuster: A tool for simplifying and converting GADTsJournal of Functional Programming10.1017/S095679681800011428Online publication date: 22-Jun-2018
https://doi.org/10.1017/S0956796818000114
Jay B(2018)Self-Quotation in a Typed, Intensional Lambda-CalculusElectronic Notes in Theoretical Computer Science10.1016/j.entcs.2018.03.024336(207-222)Online publication date: Apr-2018
https://doi.org/10.1016/j.entcs.2018.03.024
Show More Cited By

Index Terms

Dynamic typing as staged type inference

Recommendations

Dynamic type inference for gradual Hindley–Milner typing

Garcia and Cimini study a type inference problem for the ITGL, an implicitly and gradually typed language with let-polymorphism, and develop a sound and complete inference algorithm for it. Soundness and completeness mean that, if the algorithm succeeds, ...
Typing dynamic typing

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

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

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

January 1998

403 pages

ISBN:0897919793

DOI:10.1145/268946

Chairmen:
David B. MacQueen
Bell Labs
,
Luca Cardelli
Digital Equipment Corp.

Copyright © 1998 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: 21 January 1998

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Conference

POPL98

Sponsor:

POPL98: Symposium on Principles of Programming Languages

January 19 - 21, 1998

California, San Diego, USA

Acceptance Rates

POPL '98 Paper Acceptance Rate 32 of 175 submissions, 18%;

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

45
Total Citations
View Citations
195
Total Downloads

Downloads (Last 12 months)87
Downloads (Last 6 weeks)14

Reflects downloads up to 10 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Miyazaki YSekiyama TIgarashi A(2019)Dynamic type inference for gradual Hindley–Milner typingProceedings of the ACM on Programming Languages10.1145/32903313:POPL(1-29)Online publication date: 2-Jan-2019
https://dl.acm.org/doi/10.1145/3290331
ZAKIAN TMCDONELL TCIMINI MNEWTON R(2018)Ghostbuster: A tool for simplifying and converting GADTsJournal of Functional Programming10.1017/S095679681800011428Online publication date: 22-Jun-2018
https://doi.org/10.1017/S0956796818000114
Jay B(2018)Self-Quotation in a Typed, Intensional Lambda-CalculusElectronic Notes in Theoretical Computer Science10.1016/j.entcs.2018.03.024336(207-222)Online publication date: Apr-2018
https://doi.org/10.1016/j.entcs.2018.03.024
Suwa TTsukada TKobayashi NIgarashi ASchultz UYallop J(2017)Verification of code generators via higher-order model checkingProceedings of the 2017 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation10.1145/3018882.3018886(59-70)Online publication date: 2-Jan-2017
https://dl.acm.org/doi/10.1145/3018882.3018886
McDonell TZakian TCimini MNewton R(2016)Ghostbuster: a tool for simplifying and converting GADTsACM SIGPLAN Notices10.1145/3022670.295191451:9(338-350)Online publication date: 4-Sep-2016
https://dl.acm.org/doi/10.1145/3022670.2951914
McDonell TZakian TCimini MNewton RGarrigue JKeller GSumii E(2016)Ghostbuster: a tool for simplifying and converting GADTsProceedings of the 21st ACM SIGPLAN International Conference on Functional Programming10.1145/2951913.2951914(338-350)Online publication date: 4-Sep-2016
https://dl.acm.org/doi/10.1145/2951913.2951914
Chen SErwig MWalkingshaw E(2014)Extending Type Inference to Variational ProgramsACM Transactions on Programming Languages and Systems10.1145/251819036:1(1-54)Online publication date: 1-Mar-2014
https://dl.acm.org/doi/10.1145/2518190
Servetto MZucca E(2014)A meta-circular language for active librariesScience of Computer Programming10.1016/j.scico.2014.05.00395:P2(219-253)Online publication date: 1-Dec-2014
https://dl.acm.org/doi/10.1016/j.scico.2014.05.003
Servetto MZucca EAlbert EMu S(2013)A meta-circular language for active librariesProceedings of the ACM SIGPLAN 2013 workshop on Partial evaluation and program manipulation10.1145/2426890.2426913(117-126)Online publication date: 21-Jan-2013
https://dl.acm.org/doi/10.1145/2426890.2426913
Necula GMcPeak SWeimer W(2012)CCuredACM SIGPLAN Notices10.1145/2442776.244278647:4a(74-85)Online publication date: 18-Mar-2012
https://dl.acm.org/doi/10.1145/2442776.2442786
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 Publication

Media

Figures

Other

Tables

View Table of Contents