Mark Shields
Simon Peyton Jones
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.
- 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. Google Scholar
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.Google ScholarCross Ref
- 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. Google ScholarDigital 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. Google ScholarDigital Library
- 5.It. Barendregt. Introduction to generalized type systems. Journal of Functional Programming, 1(2):125- 154, 1991.Google ScholarCross Ref
- 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. Google ScholarDigital 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. Google ScholarDigital 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. Google ScholarDigital 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. Google ScholarDigital 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. Google ScholarDigital 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. Google ScholarDigital 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. Google ScholarDigital Library
- 13.J. Hatcliff and O. Danvy. Thunks and the lambdacalculus. Journ'al of Functional Programming, 7(3):303- 319, May 1997. Google ScholarDigital 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. Google ScholarDigital Library
- 15.N. D. Jones, C. K. Gomard, and P. SestofL Partial E~aluation and Automatic Program Generation. Prentice Hall Iaxtexnational, 1993. Google ScholarDigital 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. Google ScholarDigital Library
- 17.X. Leroy and M. Maamy. Dynamics in ML. Journal of .b'~netionaI Programming, 3(4):431-463, 1993.Google Scholar
- 18.Microsoft. The component object model specification. Technical report, Microsoft Corporation, 1995. oGoogle Scholar
- 19.R. Milner. A theory of type polymorphism in programming. Journal. of Computer and System Sciences, 17:348-375, 1978.Google ScholarCross Ref
- 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.Google Scholar
- 21.A. Mycroft. Dyn.amic types in ML. (unpublished drafe article), 1983.Google Scholar
- 22.F. Nielson and H. tL Nielsom Tuw-levet Functional Languages. Cambridge University Press, 1992. Google ScholarDigital 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. Google ScholarDigital Library
- 24.J. Paterson and K. Hammond. Report or~ the Programming Language Haskell (Version 1.4), Apt 1997.Google Scholar
- 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,Google Scholar
- 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'. Google ScholarDigital 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. Google ScholarDigital Library
- 28.A. K. Wrigh~ and M. Felleisen. A syntactic approach to type soundness. Information and Computalion~ 115(1):38-94, Nov 1994. Google ScholarDigital Library
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 programmingEven 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