CS&E Colloquium: Efficient Gradual Typing
The computer science colloquium takes place on Mondays from 11:15 a.m. - 12:15 p.m.
This week's speaker, Jeremy Siek (Indiana University), will be giving a talk titled "Efficient Gradual Typing."
Abstract
Gradual typing combines static and dynamic typing in the same program. Siek et al. (2015) describe five criteria for gradually typed languages, including type soundness and the gradual guarantee. A significant number of languages have been developed in academia and industry that support some of these criteria (TypeScript, Typed Racket, Safe TypeScript, Transient Reticulated Python, Thorn, etc.) but relatively few support all the criteria (Nom, Gradualtalk, Guarded Reticulated Python). Of those that do, only Nom does so efficiently. The Nom experiment shows that one can achieve efficient gradual typing in languages with only nominal types, but many languages have structural types: function types, tuples, record and object types, generics, etc.
In this talk, I present a compiler, named Grift, that addresses the difficult challenge of efficient gradual typing for structural types. The input language includes a selection of difficult features: first-class functions, mutable arrays, and recursive types. I show that a close-to-the-metal implementation of run-time casts inspired by Henglein's coercions eliminates all of the catastrophic slowdowns without introducing significant average-case overhead. As a result, Grift exhibits lower overheads than those of Typed Racket.
Biography
Jeremy Siek is a Professor at Indiana University. Jeremy's interests include programming language design, type systems, mechanized theorem proving, and 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 and Walid Taha developed the idea of gradual typing: a type system that integrates both dynamic and static typing in the same programming language. Jeremy taught at the University of Colorado for many years and then moved to Indiana University. Jeremy is currently working with his student on the Grift compiler, which demonstrates that gradually typed programs can be compiled into efficient executables using the latest techniques in cast compression. Jeremy is also investigating the use of denotational semantics to prove the correctness of compilers proofs mechanized in Agda. 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. From 2015 to the present Jeremy has been working with colleagues at Northeastern, Brown, and Maryland on the NSF-funded projects Gradual Typing Across the Spectrum and Performant Sound Gradual Typing.
