# Blame and contracts

### Blame, coercions, and threesomes: together again for the first time

Jeremy Siek, Peter Thiemann, and Philip Wadler. Draft, October 2014.

We present four calculi for gradual typing: $\lambda\B$, based on the blame calculus of Wadler and Findler~(2009); $\lambda\C$, based on the coercion calculus of Henglein~(1994); and $\lambda\T$ and $\lambda\W$, based on the threesome calculi with and without blame of Siek and Wadler~(2010). We define translations from $\lambda\B$ to $\lambda\C$, from $\lambda\C$ to $\lambda\T$, and from $\lambda\T$ to $\lambda\W$. We show each of the translations is fully abstract —far stronger correctness results than have previously appeared.

### Integrating Static and Dynamic Type Systems

Lecture series, PhD Open, Warsaw, November—December 2011 and Summer School on Types and Programming Languages, St Andrews, June 2012.

Both Meijer and Bracha argue in favor of mixing dynamic and static typing, and such mixing is now supported in Microsoft's .NET framework. Much recent work has focused on integrating dynamic and static typing using the contracts of Findler and Felleisen, including the gradual types of Siek and Taha, the hybrid types of Flanagan, and the manifest contracts of Greenberg, Pierce, and Weirich. This course will focus on the blame calculus, which unifies the above approaches, permitting one to integrate several strengths of type system: dynamically typed languages, Hindley-Milner typed languages, and refinement types. We will cover the basics of the blame calculus, its extension to support parametric polymorphism, and implementation techniques based on threesomes.

### Blame for All

Amal Ahmed, Robert Bruce Findler, Jeremy G. Siek, and Philip Wadler. Symposium on Principles of Programming Languages (POPL), Austin, January 2011.

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 selaing along the line 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 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.

### Threesomes, With and Without Blame

Jeremy G. Siek and Philip Wadler, Symposium on Principles of Programming Languages (POPL), Madrid, January 2010.

How to integrate static and dynamic types? Recent work focuses on casts to mediate between the two. However, adding casts may degrade tail calls into a non-tail calls, increasing space consumption from constant to linear in the depth of calls.

We present a new solution to this old problem, based on the notion of a threesome. A cast is specified by a source and a target type---a twosome. Any twosome factors into a downcast from the source to an intermediate type, followed by an upcast from the intermediate to the target---a threesome. Any chain of threesomes collapses to a single threesome, calculated by taking the greatest lower bound of the intermediate types. We augment this solution with blame labels to map any failure of a threesome back to the offending twosome in the source program.

Herman, Tomb, and Flanagan (2007) solve the space problem by representing casts with the coercion calculus of Henglein (1994). While they provide a theoretical limit on the space overhead, there remains the practical question of how best to implement coercion reduction. The threesomes presented in this paper provide a streamlined data structure and algorithm for representing and normalizing coercions. Furthermore, threesomes provide a typed-based explanation of coercion reduction.

### Blame for all

Amal Ahmed, Robert Bruce Findler, Jacob Matthews, and Philip Wadler, Workshop on Script to Program Evolution (STOP), Genova, 2009.

We present a language that integrates statically and dynamically typed components, similar to the gradual types of Siek and Taha (2006), and extend it to incorporate parametric polymorphism. Our system permits a dynamically typed value to be cast to a polymorphic type, with the type enforced by dynamic sealing along the lines proposed by Pierce and Sumii (2000), Matthews and Ahmed (2008), and Neis, Dreyer, and Rossberg (2009), in a way that ensures all terms satisfy relational parametricity. Our system includes a notion of blame, which allows us to show that when more-typed and less-typed portions of a program interact, that any type failures are due to the less-typed portion.

### Threesomes, With and Without Blame

Jeremy G. Siek and Philip Wadler. Workshop on Script to Program Evolution (STOP), Genova, 2009.

The blame calculus of Wadler and Findler gives a high-level semantics to casts in higher-order languages. The coercion calculus of Henglein, on the other hand, provides an instruction set for casts whose normal forms ensure space efficiency. In this paper we address two questions: 1) can space efficiency be obtained in a high-level semantics? and 2) can we precisely characterize the relationship between the high and low-level semantics of casts? Towards answering both of these questions, we design a cast calculus that summarizes a sequence of casts as a threesome cast that contains a source type, a target type, and a third middle type that is the greatest lower bound of all the types in the sequence. We show that the threesome calculus is equivalent to the blame calculus and to one of the coercion-based, blame-tracking calculi of Siek, Garcia, and Taha. We also show that the threesome calculus is space efficient and obtain a tighter bound than that of Herman, Tomb, and Flanagan.

### Well-typed programs can't be blamed

Philip Wadler and Robert Bruce Findler. ESOP 2009.
(See also: Scheme workshop version, ICFP submission.)

We introduce the blame calculus, which adds the notion of blame from Findler and Felleisen's contracts to a system similar to Siek and Taha's gradual types and Flanagan's hybrid types. We characterise where positive and negative blame can arise by decomposing the usual notion of subtype into positive and negative subtyping, and show that these recombine to yield naive subtyping. Naive typing has previously appeared in type systems that are unsound, but we believe this is the first time naive subtyping has played a role in establishing type soundness.

### Well-typed programs can't be blamed

Philip Wadler and Robby Findler. Submitted to ICFP 2008.

We introduce the blame calculus, which adds the notion of blame from Findler and Felleisen's contracts to a system similar to Siek and Taha's gradual types and Flanagan's hybrid types. We characterise where positive and negative blame can arise by decomposing the usual notion of subtype into positive and negative subtyping, and show that these recombine to yield naive subtyping. Naive typing has previously appeared in type systems that are unsound, but we believe this is the first time naive subtyping has played a role in establishing type soundness.

### Well-typed programs can't be blamed

Philip Wadler and Robby Findler. Scheme workshop, ICFP, Freiburg, 30 September 2007.