We systematically present four calculi for gradual typing: the blame calculus of Wadler and Findler (2009); a novel calculus that pinpoints blame precisely; the coercion calculus of Henglein (1994); and the threesome calculus of Siek and Wadler (2010). Threesomes are given a syntax that directly exposes their origin as coercions in normal form, a more transparent presentation than that found in Siek and Wadler (2010) or Garcia (2013).

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.

(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.

(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.

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.

Slides from STOP 2009: pdf. Technical report: pdf.

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.

(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.

Slides from AOSD 2008: pdf.

(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.

Slides from AOSD 2008: pdf.

(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.

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