Document Open Access Logo

Migratory Typing: Ten Years Later

Authors Sam Tobin-Hochstadt, Matthias Felleisen, Robert Findler, Matthew Flatt, Ben Greenman, Andrew M. Kent, Vincent St-Amour, T. Stephen Strickland, Asumu Takikawa

PDF
Thumbnail PDF

File

LIPIcs.SNAPL.2017.17.pdf
  • Filesize: 481 kB
  • 17 pages

Document Identifiers

Author Details

Sam Tobin-Hochstadt
Matthias Felleisen
Robert Findler
Matthew Flatt
Ben Greenman
Andrew M. Kent
Vincent St-Amour
T. Stephen Strickland
Asumu Takikawa

Cite AsGet BibTex

Sam Tobin-Hochstadt, Matthias Felleisen, Robert Findler, Matthew Flatt, Ben Greenman, Andrew M. Kent, Vincent St-Amour, T. Stephen Strickland, and Asumu Takikawa. Migratory Typing: Ten Years Later. In 2nd Summit on Advances in Programming Languages (SNAPL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 71, pp. 17:1-17:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
https://doi.org/10.4230/LIPIcs.SNAPL.2017.17

Abstract

In this day and age, many developers work on large, untyped code repositories. Even if they are the creators of the code, they notice that they have to figure out the equivalent of method signatures every time they work on old code. This step is time consuming and error prone. Ten years ago, the two lead authors outlined a linguistic solution to this problem. Specifically they proposed the creation of typed twins for untyped programming languages so that developers could migrate scripts from the untyped world to a typed one in an incremental manner. Their programmatic paper also spelled out three guiding design principles concerning the acceptance of grown idioms, the soundness of mixed-typed programs, and the units of migration. This paper revisits this idea of a migratory type system as implemented for Racket. It explains how the design principles have been used to produce the Typed Racket twin and presents an assessment of the project's status, highlighting successes and failures.
Keywords
  • design principles
  • type systems
  • gradual typing

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Alexander Aiken and Brian R. Murphy. Static type inference in a dynamically typed language. In Principles of Programming Languages, pages 279-290, 1991. Google Scholar
  2. Alexander Aiken, Edward L. Wimmers, and T. K. Lakshman. Soft typing with conditional types. In Principles of Programming Languages, pages 163-173, 1994. Google Scholar
  3. Esteban Allende, Oscar Callaú, Johan Fabry, Éric Tanter, and Marcus Denker. Gradual typing for Smalltalk. Science of Computer Programming, 96(P1):52-69, December 2014. Google Scholar
  4. Esteban Allende, Johan Fabry, Ronald Garcia, and Éric Tanter. Confined gradual typing. In Object-Oriented Programming Systems, Languages &Applications, pages 251-270, 2014. Google Scholar
  5. Spenser Bauman, Carl Friedrich Bolz, Robert Hirschfeld, Vasily Kirilichev, Tobias Pape, Jeremy G. Siek, and Sam Tobin-Hochstadt. Pycket: a tracing JIT for a functional language. In International Conference on Functional Programming, pages 22-34, 2015. Google Scholar
  6. Hans J. Boehm. Partial polymorphic type inference is undecidable. In Foundations of Computer Science, pages 339-345, 1985. Google Scholar
  7. Ambrose Bonnaire-Sergeant, Rowan Davies, and Sam Tobin-Hochstadt. Practical optional types for Clojure. In European Symposium on Programming, pages 68-94, 2016. Google Scholar
  8. Gilad Bracha. Pluggable type systems. In Object-Oriented Programming Systems, Languages &Applications. Companion (Workshop on Revival of Dynamic Languages), 2004. Google Scholar
  9. Gilad Bracha and David Griswold. Strongtalk: typechecking Smalltalk in a production environment. In Object-Oriented Programming Systems, Languages &Applications, pages 215-230, 1993. Google Scholar
  10. L. Cardelli. Typeful programming. Technical Report 45, Digital Systems Research Center, May 1989. Google Scholar
  11. Robert Cartwright and Mike Fagan. Soft typing. In Programming Language Design and Implementation, pages 278-292, 1991. Google Scholar
  12. William Clinger and Jonathan Rees. The revised⁴ report on the algorithmic language Scheme. ACM Lisp Pointers, 4(3), July 1991. Google Scholar
  13. Mike Fagan. Soft Typing: An Approach to Type Checking for Dynamically Typed Languages. PhD thesis, Rice University, 1991. Google Scholar
  14. Matthias Felleisen, Robert Bruce Findler, and Matthew Flatt. Semantics Engineering with PLT Redex. The MIT Press, 2009. Google Scholar
  15. Matthias Felleisen, Robert Bruce Findler, Matthew Flatt, and Shriram Krishnamurthi. The DrScheme project: An overview. ACM SIGPLAN Notices, June 1998. Invited paper. Google Scholar
  16. Matthias Felleisen, Robert Bruce Findler, Matthew Flatt, and Shriram Krishnamurthi. The TeachScheme! project: Computing and programming for every student. Computer Science Education, 14:55-77, 2004. Google Scholar
  17. Matthias Felleisen, Robert Bruce Findler, Matthew Flatt, Shriram Krishnamurthi, Eli Barzilay, Jay McCarthy, and Sam Tobin-Hochstadt. The Racket Manifesto. In First Summit on Advances in Programming Languages (SNAPL 2015), volume 32 of Leibniz International Proceedings in Informatics (LIPIcs), pages 113-128. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2015. Google Scholar
  18. Robert Bruce Findler, John Clements, Cormac Flanagan, Matthew Flatt, Shriram Krishnamurthi, Paul Steckler, and Matthias Felleisen. DrScheme: A programming environment for Scheme. J. Functional Programming, 12(2):159-182, 2002. Google Scholar
  19. Robert Bruce Findler and Matthias Felleisen. Contracts for higher-order functions. In International Conference on Functional Programming, pages 48-59, 2002. Google Scholar
  20. Cormac Flanagan. Effective Static Debugging via Componential Set-Based Analysis. PhD thesis, Rice University, 1997. Google Scholar
  21. Cormac Flanagan. Hybrid type checking. In Principles of Programming Languages, pages 245-256, January 2006. Google Scholar
  22. Cormac Flanagan and Matthias Felleisen. Componential set-based analysis. In Programming Language Design and Implementation, pages 235-248, 1997. Google Scholar
  23. Cormac Flanagan, Matthew Flatt, Shriram Krishnamurthi, Stephanie Weirich, and Matthias Felleisen. Catching bugs in the web of program invariants. In Programming Language Design and Implementation, pages 23-32, May 1996. Google Scholar
  24. Matthew Flatt, Robert Bruce Findler, and Matthias Felleisen. Scheme with classes, mixins, and traits. In Asian Symposium on Programming Languages and Systems, pages 270-289, 2006. Google Scholar
  25. Ben Greenman, Asumu Takikawa, Max S. New, Daniel Feltey, Robert Bruce Findler, Jan Vitek, and Matthias Felleisen. Performance evaluation for gradual typing. J. Functional Programming, 2016. Submitted for publication. Google Scholar
  26. Fritz Henglein. Dynamic typing: Syntax and proof theory. Science of Computer Programming, 22(3):197-230, 1994. Google Scholar
  27. Andrew M. Kent, David Kempe, and Sam Tobin-Hochstadt. Occurrence typing modulo theories. In Programming Language Design and Implementation, pages 296-309, 2016. Google Scholar
  28. Sebastian Kleinschmager, Stefan Hanenberg, Romain Robbes, Éric Tanter, and Andreas Stefik. Do static type systems improve the maintainability of software systems? An empirical study. In International Conference on Program Comprehension, pages 153-162, 2012. Google Scholar
  29. Raghavan Komondoor, G. Ramalingam, Satish Chandra, and John Field. Dependent types for program understanding. In Tools and Algorithms for the Construction and Analysis of Systems, volume 3440 of lncs, pages 157-173, 2005. Google Scholar
  30. Jacob Matthews and Robert Bruce Findler. Operational semantics for multi-language programs. ACM Transactions on Programming Languages and Systems, 31(3):1-44, 2009. Google Scholar
  31. Clemens Mayer, Stefan Hanenberg, Romain Robbes, Éric Tanter, and Andreas Stefik. An empirical study of the influence of static type systems on the usability of undocumented software. In Object-Oriented Programming Systems, Languages &Applications, pages 683-702, 2012. Google Scholar
  32. Philippe Meunier. Modular Set-Based Analysis from Contracts. PhD thesis, Northeastern University, 2006. Google Scholar
  33. Philippe Meunier, Robert Bruce Findler, and Matthias Felleisen. Modular set-based analysis from contracts. In Principles of Programming Languages, pages 218-231, 2006. Google Scholar
  34. D. Rémy. Typechecking records and variants in a natural extension of ML. In Principles of Programming Languages, 1989. Google Scholar
  35. John C. Reynolds. Types, abstraction, and parametric polymorphism. In IFIP Congress on Information Processing, pages 513-523, 1983. Google Scholar
  36. Gregor Richards, Francesco Zappa Nardelli, and Jan Vitek. Concrete types for typescript. In European Conference on Object-Oriented Programming, pages 76-100, July 2015. Google Scholar
  37. 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. Google Scholar
  38. Jeremy G. Siek and Walid Taha. Gradual typing for objects. In European Conference on Object-Oriented Programming, pages 2-27, 2007. Google Scholar
  39. Jeremy G. Siek and Manish Vachharajani. Gradual typing with unification-based inference. In Dynamic Languages Symposium, pages 1-12, 2008. Google Scholar
  40. Jeremy G. Siek, Michael M. Vitousek, and Shashank Bharadwaj. Gradual typing for mutable objects. Unpublished manuscript, available at URL: http://ecee.colorado.edu/~siek/gtmo.pdf.
  41. Vincent St-Amour, Sam Tobin-Hochstadt, Matthew Flatt, and Matthias Felleisen. Typing the numeric tower. In Practical Aspects of Declarative Languages, pages 289-303, 2012. Google Scholar
  42. Guy Lewis Steele Jr. Common Lisp - The Language. Digital Press, 1984. Google Scholar
  43. T. Stephen Strickland, Sam Tobin-Hochstadt, and Matthias Felleisen. Practical variable-arity polymorphism. In European Symposium on Programming, pages 32-46, March 2009. Google Scholar
  44. Norihisa Suzuki. Inferring types in Smalltalk. In Principles of Programming Languages, pages 187-199, 1981. Google Scholar
  45. Asumu Takikawa, Daniel Feltey, Ben Greenman, Max S. New, Jan Vitek, and Matthias Felleisen. Is sound gradual typing dead? In Principles of Programming Languages, pages 456-468, 2016. Google Scholar
  46. Asumu Takikawa, Daniel Feltey, Sam Tobin-Hochstadt, Robert Bruce Findler, Matthew Flatt, and Matthias Felleisen. Towards practical gradual typing. In European Conference on Object-Oriented Programming, pages 4-27, 2015. Google Scholar
  47. Asumu Takikawa, T. Stephen Strickland, Christos Dimoulas, Sam Tobin-Hochstadt, and Matthias Felleisen. Gradual typing for first-class classes. In Object-Oriented Programming Systems, Languages &Applications, pages 793-810, 2012. Google Scholar
  48. Sam Tobin-Hochstadt and Matthias Felleisen. Interlanguage migration: from scripts to programs. In Dynamic Language Symposium, pages 964-974, 2006. Google Scholar
  49. Sam Tobin-Hochstadt and Matthias Felleisen. The design and implementation of Typed Scheme. In Principles of Programming Languages, pages 395-406, 2008. Google Scholar
  50. Sam Tobin-Hochstadt and Matthias Felleisen. Logical types for untyped languages. In International Conference on Functional Programming, pages 117-128, 2010. Google Scholar
  51. Sam Tobin-Hochstadt, Vincent St-Amour, Ryan Culpepper, Matthew Flatt, and Matthias Felleisen. Languages as libraries. In Programming Language Design and Implementation, pages 132-141, 2011. Google Scholar
  52. Michael M. Vitousek, Jeremy G. Siek, Andrew Kent, and Jim Baker. Design and evaluation of gradual typing for Python. In Dynamic Language Symposium, pages 45-56, 2014. Google Scholar
  53. Michael M. Vitousek, Cameron Swords, and Jeremy G. Siek. Big types in little runtime. In Principles of Programming Languages, pages 762-774, 2017. Google Scholar
  54. Mitch Wand. Finding the source of type errors. In Principles of Programming Languages, pages 38-43, 1986. Google Scholar
  55. Andrew Wright. Practical Soft Typing. PhD thesis, Rice University, 1994. Google Scholar
  56. Andrew Wright and Matthias Felleisen. A syntactic approach to type soundness. Information and Computation, pages 38-94, 1994. Google Scholar
  57. Andrew K. Wright and Robert Cartwright. A practical soft type system for Scheme. In Lisp and Functional Programming, pages 250-262, June 1994. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact