research-article

The design and implementation of typed scheme

Authors:

Sam Tobin-Hochstadt,

Matthias FelleisenAuthors Info & Claims

POPL '08: Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Pages 395 - 406

https://doi.org/10.1145/1328438.1328486

Published: 07 January 2008 Publication History

Abstract

When scripts in untyped languages grow into large programs, maintaining them becomes difficult. A lack of types in typical scripting languages means that programmers must (re)discover critical pieces of design information every time they wish to change a program. This analysis step both slows down the maintenance process and may even introduce mistakes due to the violation of undiscovered invariants.

This paper presents Typed Scheme, an explicitly typed extension of an untyped scripting language. Its type system is based on the novel notion of occurrence typing, which we formalize and mechanically prove sound. The implementation of Typed Scheme additionally borrows elements from a range of approaches, including recursive types, true unions and subtyping, plus polymorphism combined with a modicum of local inference. Initial experiments with the implementation suggest that Typed Scheme naturally accommodates the programming style of the underlying scripting language, at least for the first few thousand lines of ported code.

References

[1]

Alexander Aiken, Edward L. Wimmers, and T. K. Lakshman. Soft typing with conditional types. In POPL '94: Proceedings of the 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 163--173, New York, NY, USA, 1994. ACM Press.

Digital Library

[2]

Roberto Amadio and Luca Cardelli. Subtyping recursive types. In ACM Transactions on Programming Languages and Systems, volume 15, pages 575--631, 1993.

Digital Library

[3]

Gilad Bracha. Pluggable type systems. In Revival of Dynamic Languages Workshop at OOPSLA 2004, October 2004.

[4]

Gilad Bracha and David Griswold. Strongtalk: typechecking Smalltalk in a production environment. In OOPSLA '93: Proceedings of the Eighth Annual Conference on Object-Oriented Programming Systems, Languages, and Applications, pages 215--230, New York, NY, USA, 1993. ACM Press.

Digital Library

[5]

R. Cartwright. User-defined data types as an aid to verifying lisp programs. In Third International Colloquium on Automata, Languages and Programming, pages 228--256, 1976.

[6]

Robert Cartwright and Mike Fagan. Soft typing. In PLDI '91: Proceedings of the ACM SIGPLAN 1991 Conference on Programming Language Design and Implementation, pages 278--292, New York, NY, USA, 1991. ACM Press.

Digital Library

[7]

Karl Crary, Stephanie Weirich, and Greg Morrisett. Intensional polymorphism in type-erasure semantics. In ICFP '98: Proceedings of the Third ACM SIGPLAN International Conference on Functional Programming, pages 301--312, New York, NY, USA, 1998. ACM Press. ISBN 1--58113--024--4. doihttp://doi.acm.org/10.1145/289423.289459.

Digital Library

[8]

Ryan Culpepper, Sam Tobin-Hochstadt, and Matthew Flatt. Advanced Macrology and the Implementation of Typed Scheme. In Proceedings of the Eighth Workshop on Scheme and Functional Programming, 2007.

[9]

R. Kent Dybvig and Robert Hieb. A new approach to procedures with variable arity. Lisp and Symbolic Computation: An International Journal, 3 (3), 1990.

Digital Library

[10]

Hsianlin Dzeng and Christopher T. Haynes. Type reconstruction for variable-arity procedures. In LFP '94: Proceedings of the 1994 ACM conference on LISP and Functional Programming, pages 239--249, New York, NY, USA, 1994. ACM Press.

Digital Library

[11]

ECMA International. ECMAScript Edition 4 group wiki, 2007.

[12]

Matthias Felleisen, Robert Bruce Findler, Matthew Flatt, and Shriram Krishnamurthi. How to Design Programs. MIT Press, 2001. URL http://www.htdp.org/.

[13]

Robert Bruce Findler and Matthias Felleisen. Contracts for higher-order functions. In ICFP '02: ACM SIGPLAN International Conference on Functional Programming, pages 48--59, 2002.

Digital Library

[14]

Robert Bruce Findler, John Clements, Cormac Flanagan, Matthew Flatt, Shriram Krishnamurthi, Paul Steckler, and Matthias Felleisen. DrScheme: A programming environment for Scheme. Journal of Functional Programming, 12(2): 159--182, 2002.

Digital Library

[15]

Cormac Flanagan and Matthias Felleisen. Componential set-based analysis. ACM Trans. Program. Lang. Syst., 21(2):370--416, 1999.

Digital Library

[16]

Cormac Flanagan, Matthew Flatt, Shriram Krishnamurthi, Stephanie Weirich, and Matthias Felleisen. Catching bugs in the web of program invariants. In PLDI '96: ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 23--32, May 1996.

Digital Library

[17]

Matthew Flatt. Composable and compilable macros: You want it when? In ICFP '02: ACM SIGPLAN International Conference on Functional Programming, pages 72--83, 2002.

Digital Library

[18]

Matthew Flatt and Matthias Felleisen. Units: Cool modules for HOT languages. In PLDI '98: ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 236--248, June 1998.

Digital Library

[19]

Matthew Flatt, Robert Bruce Findler, and Matthias Felleisen. Scheme with classes, mixins, and traits. In Asian Symposium on Programming Languages and Systems (APLAS) 2006, pages 270--289, November 2006.

Digital Library

[20]

Daniel P. Friedman and Matthias Felleisen. The Little Schemer, Fourth Edition. MIT Press, Cambridge, 1997.

[21]

Daniel P. Friedman and Matthias Felleisen. The Seasoned Schemer. MIT Press, Cambridge, 1996.

Digital Library

[22]

David Gifford, Pierre Jouvelot, John Lucassen, and Mark Sheldon. FX-87 Reference Manual. Technical Report MIT/LCS/TR-407, Massachusetts Institute of Technology, Laboratory for Computer Science, September 1987.

[23]

J. Gosling, B. Joy, G. L.Steele, and G. Bracha. The Java Language Specification, Third Edition. Addison-Welsley, 2005.

Digital Library

[24]

Timothy G. Griffin. The formulae-as-types notion of control. In POPL '90: Conf. Record 17th Annual ACM Symp. on Principles of Programming Languages, Jan 1990.

Digital Library

[25]

Robert Harper and Greg Morrisett. Compiling polymorphism using intensional type analysis. In POPL '95: ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 130--141, 1995.

Digital Library

[26]

Christopher T. Haynes. Infer: A statically-typed dialect of scheme. Technical Report 367, Indiana University, 1995.

[27]

Nevin Heintze. Set based analysis of ML programs. In LFP '94: ACM Symposium on Lisp and Functional Programming, pages 306--317, 1994.

Digital Library

[28]

Fritz Henglein and Jakob Rehof. Safe polymorphic type inference for a dynamically typed language: translating Scheme to ML. In FPCA '95: Proceedings of the Seventh International Conference on Functional Programming Languages and Computer Architecture, pages 192--203, 1995.

Digital Library

[29]

David Herman, Aaron Tomb, and Cormac Flanagan. Space-efficient gradual typing. In 8th Symposium on Trends in Functional Programming, April 2007.

[30]

Gary T. Leavens, Curtis Clifton, and Brian Dorn. A Type Notation for Scheme. Technical Report 05--18a, Iowa State University, August 2005.

[31]

Jacob Matthews. Component deployment with PLaneT: You want it where? In Proceedings of the Seventh Workshop on Scheme and Functional Programming, University of Chicago, Technical Report TR-2006-06, 2006.

[32]

Jacob Matthews, Robert Findler, Matthew Flatt, and Matthias Felleisen. A visual environment for developing context-sensitive term rewriting systems. In RTA 2004: Rewriting Techniques and Applications, 15th International Conference, Aachen, Germany, June 3-5, 2004, Proceedings, volume 3091 of Lecture Notes in Computer Science, pages 2--16. Springer-Verlag, 2004.

[33]

Philippe Meunier, Robert Bruce Findler, and Matthias Felleisen. Modular set-based analysis from contracts. In POPL '06: Conference Record of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 218--231, New York, NY, USA, 2006. ACM Press.

Digital Library

[34]

Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL - A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer, 2002.

Digital Library

[35]

Benjamin C. Pierce. Programming with intersection types, union types, and polymorphism. Technical Report CMU-CS-91-106, Carnegie Mellon University, February 1991.

[36]

Benjamin C. Pierce and David N. Turner. Local type inference. volume 22, pages 1--44, New York, NY, USA, 2000. ACM.

Digital Library

[37]

John C. Reynolds. Types, abstraction, and parametric polymorphism. In REA. Mason, editor, Information Processing 83, Paris, France, pages 513--523. Elsevier, 1983.

[38]

Michael Salib. Starkiller: A static type inferencer and compiler for Python. Master's thesis, Massachusetts Institute of Technology, Cambridge, Massachusetts, May 2004.

[39]

Olin Shivers. Control-Flow Analysis of Higher-Order Languages or Taming Lambda. PhD thesis, Carnegie Mellon University, Pittsburgh, Pennsylvania, May 1991.

Digital Library

[40]

Jeremy G. Siek and Walid Taha. Gradual typing for functional languages. In Scheme and Functional Programming Workshop, University of Chicago, Technical Report TR-2006-06, pages 81--92, September 2006.

[41]

Jens Axel Søgaard. Galore, 2006. http://planet.plt-scheme.org/.

[42]

Guy Lewis Steele Jr. Common Lisp-The Language. Digital Press, 1984.

Digital Library

[43]

Audrey Tang. Perl 6: reconciling the irreconcilable. In POPL '07: Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 1--1, New York, NY, USA, 2007. ACM Press. http://pugscode.org.

Digital Library

[44]

Sam Tobin-Hochstadt and Matthias Felleisen. Interlanguage migration: from scripts to programs. In OOPSLA '06: Companion to the 21st ACM SIGPLAN Conference on Object-oriented Programming Systems, Languages, and Applications, pages 964--974, New York, NY, USA, 2006. ACM Press.

Digital Library

[45]

Christian Urban and Christine Tasson. Nominal Reasoning Techniques in Isabelle/HOL. In Proceedings of the 20th Conference on Automated Deduction (CADE 2005), volume 3632 of Lecture Notes in Artificial Intelligence. Springer, 2005.

Digital Library

[46]

Dimitrios Vytiniotis, Stephanie Weirich, and Simon Peyton Jones. Boxy types: inference for higher-rank types and impredicativity. In ICFP '06: Proceedings of the Eleventh ACM SIGPLAN International Conference on Functional Programming, pages 251--262, New York, NY, USA, 2006. ACM Press.

Digital Library

[47]

Philip Wadler and Robert Bruce Findler. Well-typed programs can't be blamed. In Proceedings of the Eighth Workshop on Scheme and Functional Programming, 2007.

[48]

Mitchell Wand. A semantic prototyping system. In SIGPLAN '84: Proceedings of the 1984 SIGPLAN Symposium on Compiler Construction, pages 213--221, New York, NY, USA, 1984. ACM Press.

Digital Library

[49]

A. Wright and B. Duba. Pattern matching for Scheme. Technical report, Rice University, May 1995.

[50]

Andrew Wright and Matthias Felleisen. A syntactic approach to type soundness. Information and Computation, pages 38--94, 1994. First appeared as Technical Report TR160, Rice University, 1991.

Digital Library

[51]

Andrew K. Wright and Robert Cartwright. A practical soft type system for scheme. ACM Trans. Program. Lang. Syst., 19(1): 87--152, 1997.

Digital Library

Cited By

Berger FSchimpf ABieniusa AWehr SFernandez-Reyes KVoinea A(2024)Same Same but Different: A Comparative Analysis of Static Type Checkers in ErlangProceedings of the 23rd ACM SIGPLAN International Workshop on Erlang10.1145/3677995.3678189(2-12)Online publication date: 28-Aug-2024
https://dl.acm.org/doi/10.1145/3677995.3678189
Campora JKhan MChen S(2024)Type-Based Gradual Typing Performance OptimizationProceedings of the ACM on Programming Languages10.1145/36329318:POPL(2667-2699)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632931
Borkowski MVazou NJhala R(2024)Mechanizing Refinement TypesProceedings of the ACM on Programming Languages10.1145/36329128:POPL(2099-2128)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632912
Show More Cited By

Index Terms

The design and implementation of typed scheme
1. Software and its engineering
  1. Software notations and tools
    1. Formal language definitions
      1. Semantics
    2. General programming languages
      1. Language features
        Modules / packages
2. Theory of computation
  1. Semantics and reasoning
    1. Program semantics

Recommendations

The design and implementation of typed scheme
POPL '08

When scripts in untyped languages grow into large programs, maintaining them becomes difficult. A lack of types in typical scripting languages means that programmers must (re)discover critical pieces of design information every time they wish to change ...
Interpretations of the gradually-typed lambda calculus
Scheme '12: Proceedings of the 2012 Annual Workshop on Scheme and Functional Programming

Gradual typing is an approach to integrating static and dynamic type checking within the same language [Siek and Taha 2006]. Given the name "gradual typing", one might think that the most interesting aspect is the type system. It turns out that the ...
A polymorphic modal type system for lisp-like multi-staged languages
POPL '06: Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages

This article presents a polymorphic modal type system and its principal type inference algorithm that conservatively extend ML by all of Lisp's staging constructs (the quasi-quotation system). The combination is meaningful because ML is a practical ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

POPL '08: Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

January 2008

448 pages

ISBN:9781595936899

DOI:10.1145/1328438

General Chair:
George Necula
University of California, Berkeley
,
Program Chair:
Philip Wadler
University of Edinburgh

ACM SIGPLAN Notices Volume 43, Issue 1
POPL '08
January 2008
420 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/1328897
Issue’s Table of Contents

Copyright © 2008 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: 07 January 2008

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

POPL08

Sponsor:

POPL08: The 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

January 7 - 12, 2008

California, San Francisco, USA

Acceptance Rates

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

272
Total Citations
View Citations
1,064
Total Downloads

Downloads (Last 12 months)32
Downloads (Last 6 weeks)6

Reflects downloads up to 24 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

Berger FSchimpf ABieniusa AWehr SFernandez-Reyes KVoinea A(2024)Same Same but Different: A Comparative Analysis of Static Type Checkers in ErlangProceedings of the 23rd ACM SIGPLAN International Workshop on Erlang10.1145/3677995.3678189(2-12)Online publication date: 28-Aug-2024
https://dl.acm.org/doi/10.1145/3677995.3678189
Campora JKhan MChen S(2024)Type-Based Gradual Typing Performance OptimizationProceedings of the ACM on Programming Languages10.1145/36329318:POPL(2667-2699)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632931
Borkowski MVazou NJhala R(2024)Mechanizing Refinement TypesProceedings of the ACM on Programming Languages10.1145/36329128:POPL(2099-2128)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632912
Castagna GLaurent MNguyễn K(2024)Polymorphic Type Inference for Dynamic LanguagesProceedings of the ACM on Programming Languages10.1145/36328828:POPL(1179-1210)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632882
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
SU CCHEN LYANHUI LZHOU Y(2024)Static Blame for gradual typingJournal of Functional Programming10.1017/S095679682400002934Online publication date: 25-Mar-2024
https://doi.org/10.1017/S0956796824000029
New MGiovannini ELicata D(2023)Gradual Typing for Effect HandlersProceedings of the ACM on Programming Languages10.1145/36228607:OOPSLA2(1758-1786)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3622860
Lazarek LGreenman BFelleisen MDimoulas C(2023)How to Evaluate Blame for Gradual Types, Part 2Proceedings of the ACM on Programming Languages10.1145/36078367:ICFP(159-186)Online publication date: 31-Aug-2023
https://dl.acm.org/doi/10.1145/3607836
Greenman BDimoulas CFelleisen M(2023)Typed–Untyped Interactions: A Comparative AnalysisACM Transactions on Programming Languages and Systems10.1145/357983345:1(1-54)Online publication date: 5-Mar-2023
https://dl.acm.org/doi/10.1145/3579833
Castagna G(2023)Programming with Union, Intersection, and Negation TypesThe French School of Programming10.1007/978-3-031-34518-0_12(309-378)Online publication date: 11-Oct-2023
https://doi.org/10.1007/978-3-031-34518-0_12
Show More Cited By

View Options

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

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents