TY - GEN
T1 - Blame for all
AU - Ahmed, Amal
AU - Findler, Robert Bruce
AU - Siek, Jeremy G.
AU - Wadler, Philip
N1 - This paper is an improved version of a paper in STOP 2009. The current paper is completely rewritten (and has lost one author and gained another). Among the more significant differences, we use type bindings as compared to a global store; and we prove the Subtyping Theorem, a conjecture in the earlier paper.
PY - 2011
Y1 - 2011
N2 - 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.
AB - 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.
KW - blame tracking
KW - casts
KW - coercions
KW - lambda-calculus
UR - http://www.scopus.com/inward/record.url?scp=79952035878&partnerID=8YFLogxK
U2 - 10.1145/1926385.1926409
DO - 10.1145/1926385.1926409
M3 - Conference contribution
SN - 978-1-4503-0490-0
SP - 201
EP - 214
BT - Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of Programming Languages (POPL '11)
PB - ACM
CY - New York, NY, USA
ER -