文档介绍：Blame for All Amal Ahmed Indiana University ******@ Robert Bruce Findler Northwestern University ******@ Jeremy G. Siek University of Colorado at Boulder jeremy.******@ Philip Wadler University of Edinburgh ******@ Abstract Several programming languages are beginning to integrate static and dynamic typing, including Racket (formerly PLTScheme), Perl 6, and C# and the research languages Sage (Gronski, Knowles, Tomb, Freund, and Flanagan, 2006) and Thorn (Wrigstad, Eug- ster, Field, Nystrom, and Vitek, 2009). However, an important open question remains, which is how to add parametric polymorphism to languages bine static and dynamic typing. We present a system that permits a value of dynamic type to be cast to a polymor- phic 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. Categories and Subject [Language Constructs and Features]: Procedures, functions, and subroutines General TermsLanguages, Theory Keywordscasts, coercions, blame tracking, lambda-calculus 1. Introduction The long tradition of work that integrates static and dynamic types includes thepartial typesofThatte(1988), thedynamic typeof Abadi et al.(1991), thecoercionsofHenglein(1994), thecontracts of Findler and Felleisen(2002), thedynamic dependent typesofOu et al.(2004), thehybrid typesof Gronski et al.(2006), thegrad- ual typesof Siek and Taha(2006), themigratory typesof Tobin- Hochstadt and Felleisen(2006), themulti-languageprogramming of Matthews and Findler(2007), and theblame calculusof Wadler and Findle