Gradual typing is an approach for designing programming languages that integrate static and dynamic type checking. Gradual typing gives the programmer fine-grained control over which regions of a program are statically checked and which regions are dynamically checked. Over the last decade, there has been renewed interest in such an integration partly due to the rise in popularity of dynamic languages. They were used to create larger programs, which exposed the need for the early error detection and modularity provided by static type checking. Gradual typing provides a practical migration path for dynamically typed programs to become more statically typed. This tutorial will give a comprehensive review of the state of the art in gradual typing. It will describe a) the major challenges in the design and implementation of gradually typed languages, b) the research that has addressed many of these challenges, and c) the open problems that need to be solved. The challenges facing gradual typing include both theoretical questions and system design problems. On the theoretical side, there are challenges like characterizing what gradual typing is, what type soundness should mean, and whether relational parametricity can be preserved. On the system design side, there are challenges such as creating language runtimes that implement gradual typing in a time and space-efficient manner.
Conference DayMon 16 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
09:00 - 12:00
|The State of the Art in Gradual Typing|
Jeremy G. SiekIndiana University Bloomington