Blame and contracts

Philip Wadler


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.

Available in: pdf


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.

Slides: 1, 2, 3, 4.


Blame for All

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

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.

Available in: doi, pdf, redex model.


Threesomes, With and Without Blame

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

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.

Available in: doi, pdf.


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.

Available in: doi, pdf.
Slides from STOP 2009: pdf. Technical report: pdf.


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.

Available in: doi, pdf.


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.

Available in: pdf.
Slides from AOSD 2008: pdf.


Well-typed programs can't be blamed

Philip Wadler and Robby Findler. Submitted to ICFP 2008.
(See also: Scheme workshop version.)

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.

Available in: pdf.
Slides from AOSD 2008: pdf.


Well-typed programs can't be blamed

Philip Wadler and Robby Findler. Scheme workshop, ICFP, Freiburg, 30 September 2007.
(See also: ICFP version.)

We show how contracts with blame fit naturally with recent work on hybrid types and gradual types. Unlike hybrid types or gradual types, we require casts in the source code, in order to indicate where type errors may occur. Two (perhaps surprising) aspects of our approach are that refined types can provide useful static guarantees even in the absence of a theorem prover, and that type dynamic should not be regarded as a supertype of all other types. We factor the well-known notion of subtyping into new notions of positive and negative subtyping, and use these to characterise where positive and negative blame may arise. Our approach sharpens and clarifies some recent results in the literature.

Available in: pdf.


Philip Wadler, Last modified: Mon Sep 14 10:46:00 BST 2009