Blame for All

Several programming languages now integrate static and dynamic typing, including C#4.0, Perl 6, and Racket (formerly PLT Scheme), and the research languages Sage and Thorn. However, an important open question remains, which is how to add parametric polymorphism to languages that combine static and dynamic typing. We present a system that permits a value of dynamic type to be cast to a polymorphic type and vice versa, with relational parametricity enforced by dynamic sealing. Our system includes a notion of blame, which allows us to show that when casting between a more-precise type and a less-precise type, any failure are due to the less-precisely-typed portion of the program. We also show that a cast from a subtype to its supertype cannot fail. A `Jack of all Trades’ theorem ensures that our method of mapping polymorphism into a dynamic language is sound. (Joint work with Amal Ahmed, Robby Findler, and Jeremy Siek.)

Speaker Bios

Philip Wadler is Professor of Theoretical Computer Science at the University of Edinburgh. He is an ACM Fellow and a Fellow of the Royal Society of Edinburgh, past holder of a Royal Society-Wolfson Research Merit Fellowship, and currently serves as Chair of ACM SIGPLAN. Previously, he worked or studied at Avaya Labs, Bell Labs, Glasgow, Chalmers, Oxford, CMU, Xerox Parc, and Stanford, and visited as a guest professor in Paris, Sydney, and Copenhagen. He appears at position 201 on Citeseer’s list of most-cited authors in computer science and is a winner of the POPL Most Influential Paper Award. He contributed to the designs of Haskell, Java, and XQuery, and is a co-author of XQuery from the Experts (Addison Wesley, 2004) and Generics and Collections in Java (O’Reilly, 2006). He has delivered invited talks in locations ranging from Aizu to Zurich.

Date:
Haut-parleurs:
Philip Wadler
Affiliation:
University of Edinburgh