Blame for all

Amal Ahmed*, Robert Findler, Jeremy G. Siek, Philip Wadler

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contribution

13 Scopus citations

Abstract

Several programming languages are beginning to integrate static and dynamic typing, including Racket (formerly PLT Scheme), Perl 6, and C# 4.0 and the research languages Sage (Gronski, Knowles, Tomb, Freund, and Flanagan, 2006) and Thorn (Wrigstad, Eugster, Field, Nystrom, and Vitek, 2009). 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 a kind of dynamic sealing along the lines proposed by Matthews and Ahmed (2008) and Neis, Dreyer, and Rossberg (2009). 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 cast failures 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.

Original languageEnglish (US)
Title of host publicationPOPL'11 - Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
Pages201-214
Number of pages14
DOIs
StatePublished - 2010
Event38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'11 - Austin, TX, United States
Duration: Jan 26 2011Jan 28 2011

Publication series

NameConference Record of the Annual ACM Symposium on Principles of Programming Languages
ISSN (Print)0730-8566

Other

Other38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'11
CountryUnited States
CityAustin, TX
Period1/26/111/28/11

Keywords

  • Blame tracking
  • Casts
  • Coercions
  • Lambda-calculus

ASJC Scopus subject areas

  • Software

Fingerprint Dive into the research topics of 'Blame for all'. Together they form a unique fingerprint.

Cite this