Write a Blog >>
Thu 21 Jan 2016 15:35 - 16:00 at Grand Bay South - Track 2: Types, Generally or Gradually Chair(s): Tiark Rompf

Programmers have come to embrace dynamically typed languages for prototyping and delivering large and complex systems. When it comes to maintaining and evolving these systems, the lack of explicit static typing becomes a bottleneck. In response, researchers have explored the idea of gradually typed programming languages which allow the post-hoc addition of type annotations to software written in one of these “untyped” languages. Some of these new hybrid languages insert run-time checks at the boundary between typed and untyped code to establish type soundness for the overall system. With sound gradual typing programmers can rely on the language implementation to provide meaningful error messages when “untyped” code misbehaves.

While most research on sound gradual typing has remained theoretical, the few emerging implementations incur performance overheads due to these checks. Indeed, none of the publications on this topic come with a comprehensive performance evaluation; a few report disastrous numbers on toy benchmarks. In response, this paper proposes a methodology for evaluating the performance of gradually typed programming languages. The key is to explore the performance impact of adding type annotations to different parts of a software system. The methodology takes takes the idea of a gradual conversion from untyped to typed seriously and calls for measuring the performance of all possible conversions of a given untyped benchmark. Finally the paper validates the proposed methodology using Typed Racket, a mature implementation of sound gradual typing, and a suite of real-world programs of various sizes and complexities. Based on the results obtained in this study, the paper concludes that, given the state of current implementation technologies, sound gradual typing is dead. Conversely, it raises the question of how implementations could reduce the overheads associated with ensuring soundness and how tools could be used to steer programmers clear from pathological cases.

Poster: Performance Evaluation for Gradual Typing (gtposter.pdf)1.29MiB

Thu 21 Jan

POPL-2016-papers
14:20 - 16:00: Research Papers - Track 2: Types, Generally or Gradually at Grand Bay South
Chair(s): Tiark RompfPurdue & Oracle Labs
POPL-2016-papers145338240000014:20 - 14:45
Talk
Sheng ChenUniversity of louisiana at Lafayette, Martin ErwigOregon State University
Media Attached
POPL-2016-papers145338390000014:45 - 15:10
Talk
Ronald GarciaUniversity of British Columbia, Alison M. Clark, Éric TanterUniversity of Chile, Chile
Link to publication Media Attached
POPL-2016-papers145338540000015:10 - 15:35
Talk
Matteo CiminiIndiana University, Jeremy G. SiekIndiana University
Media Attached
POPL-2016-papers145338690000015:35 - 16:00
Talk
Asumu TakikawaNortheastern University, Daniel FelteyNortheastern University, Ben GreenmanNortheastern University, Max New, Jan VitekNortheastern University, Matthias FelleisenNortheastern University
Pre-print Media Attached File Attached