Mixing static and dynamic type checking in the same language is catching on, with the TypeScript and Flow variants of JavaScript, the MyPy and Reticulated variants of Python, the Strongtalk and Gradualtalk variants of Smalltalk, as well as Typed Racket, Typed Clojure, and Perl 6. The gradual typing approach to such mixing seeks to protect the statically typed code from the dynamically typed code, allowing compilers to leverage type information when optimizing the static code. Unfortunately, ensuring soundness requires runtime checking at the boundaries of typed and untyped code, and the cost of this checking can drown out the performance benefits of optimization. For example, in Typed Racket, some partially typed programs are 1000X slower than the untyped or fully typed version of the same program. But all is not lost! In this talk I present the results of ongoing research to tame the runtime overheads of gradual typing in the context of a prototype compiler, named Grift, that we are developing at Indiana University.

Jeremy Siek is an Associate Professor at Indiana University Bloomington. Jeremy’s areas of research include programming language design, type systems, mechanized theorem proving using proof assistants, and optimizing compilers. Jeremy’s Ph.D. thesis explored foundations for constrained templates, aka the “concepts” proposal for C++. Prior to that, Jeremy developed the Boost Graph Library, a C++ generic library for graph algorithms and data structures. Jeremy post-doc’d at Rice University where he developed the idea of gradual typing: a type system that integrates both dynamic and static typing in the same programming language. Jeremy is currently working on several open questions regarding gradual typing. Is the polymorphic blame calculus really parametric? How should gradual typing be combined with other features such as dependent types? What is the formal criteria for gradually typed languages? Is it possible to create a high-performance implementation of a gradually-typed languages? In 2009 Jeremy received the NSF CAREER award to fund his project: “Bridging the Gap Between Prototyping and Production”. In 2010 and again in 2015, Jeremy was awarded a Distinguished Visiting Fellowship from the Scottish Informatics & Computer Science Alliance.