Blame and coercion: Together again for the first time

C#, Dart, Pyret, Racket, TypeScript, VB: many recent languages integrate dynamic and static types via gradual typing. We systematically develop four calculi for gradual typing and the relations between them, building on and strengthening previous work. The calculi are as follows: lambda B, based on the blame calculus of Wadler and Findler (2009); lambda C, inspired by the coercion calculus of Henglein (1994); lambda S inspired by the space-efficient calculus of Herman, Tomb, and Flanagan (2006); and lambda T based on the threesome calculus of Siek and Wadler (2010). While lambda B and lambda T are little changed from previous work, lambda C and lambda S are new. Together, lambda B, lambda C, lambda S, and lambda T provide a coherent foundation for design, implementation, and optimization of gradual types. We define translations from lambda B to lambda C, from lambda C to lambda S, and from lambda S to lambda T. Much previous work lacked proofs of correctness or had weak correctness criteria; here we demonstrate the strongest correctness criterion one could hope for, that each of the translations is fully abstract. Each of the calculi reinforces the design of the others: lambda C has a particularly simple definition, and the subtle definition of blame safety for lambda B is justified by the simple definition of blame safety for lambda C. Our calculus lambda S is implementation-ready: the first space-efficient calculus that is both straightforward to implement and easy to understand. We give two applications: first, using full abstraction from lambda C to lambda S to establish an equational theory of coercions; and second, using full abstraction from lambda B to lambda S to easily establish the Fundamental Property of Casts, which required a custom bisimulation and six lemmas in earlier work.