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: λB, based on the blame calculus of Wadler and Findler (2009); λC, inspired by the coercion calculus of Henglein (1994); λS inspired by the space-efficient calculus of Herman, Tomb, and Flanagan (2006); and λT based on the threesome calculus of Siek and Wadler (2010). While λB and λT are little changed from previous work, λC and λS are new. Together, λB, λC, λS, and λT provide a coher- ent foundation for design, implementation, and optimization of gradual types. We define translations from λB to λC, from λC to λS, and from λS to λ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: λC has a particularly simple definition, and the subtle definition of blame safety for λB is justified by the simple definition of blame safety for λC. Our calculus λ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 λC to λS to establish an equational theory of coercions; and second, using full abstraction from λB to λS to easily establish the Fundamental Property of Casts, which required a custom bisimulation and six lemmas in earlier work.
This paper introduces λdB, a blame calculus with dependent types. It supports dependent functions, predicate refinement at all types, the dynamic type, and full blame tracking. It is inspired by and extends previous work on hybrid types and Sage, by Flanagan and others; manifest contracts, by Greenberg, Pierce, and Weyrich; and blame calculus by Wadler and Findler. While previous work only allows refinement over base types, λdB supports refinement over any type. We introduce novel techniques in order to prove blame safety for this language, including a careful analysis that reduces open judgments on terms to closed ones on values, and the idea of ‘subtyping with a witness’, which fix flaws in the previous work of Wadler and Findler. These technical contributions mean that we can achieve a completely inductive (finitistic) account of the metatheory of our language, and thereby avoid many of the subtle technical issues which have bedevilled earlier work in this area.
# Available in: pdf.Session types are a rich type discipline, based on linear types, that lifts the sort of safety claims that come with type systems to communications. However, web-based applications and microservices are often written in a mix of languages, with type disciplines in a spectrum between static and dynamic typing. Gradual session types address this mixed setting by providing a framework which grants seamless transition between statically typed handling of sessions and any required degree of dynamic typing. We propose Gradual GV as a gradually typed extension of the functional session type system GV. Following a standard framework of gradual typing, Gradual GV consists of an external language, which relaxes the type system of GV using dynamic types; an internal language with casts, for which operational semantics is given; and a cast-insertion translation from the former to the latter. We demonstrate type and communication safety as well as blame safety, thus extending previous results to functional languages with session-based communication. The interplay of linearity and dynamic types requires a novel approach to specifying the dynamics of the language.
# Available in: pdf, doi.Gradual typing has emerged as the tonic for programmers with a thirst for a blend of static and dynamic typing. Contracts provide a lightweight form of gradual typing as they can be implemented as a library, rather than requiring a gradual type system.
Intersection and union types are well suited to static and dynamic languages: intersection encodes over- loaded functions; union encodes uncertain data arising from branching code. We extend the untyped lambda calculus with contracts for monitoring higher-order intersection and union types, for the first time giving a uniform treatment to both. Each operator requires a single reduction rule that does not depend on the constituent types or the context of the operator.
We present a new method for defining contract satisfaction based on blame behaviour. A value positively satisfies a type if applying a contract of that type can never elicit positive blame. A continuation negatively satisfies a type if applying a contract of that type can never elicit negative blame. We supplement our definition of satisfaction with a series of monitoring properties that satisfying values and continuations should have.
# Available in: pdf, doi.The polymorphic blame calculus integrates static typing, including universal types, with dynamic typing. The primary challenge with this integration is preserving parametricity: even dynamically-typed code should satisfy it once it has been cast to a universal type. Ahmed et al. (2011) employ runtime type generation in the polymorphic blame calculus to preserve parametricity, but a proof that it does so has been elusive. Matthews and Ahmed (2008) gave a proof of parametricity for a closely related system that combines ML and Scheme, but later found a flaw in their proof. In this paper we present an improved version of the polymorphic blame calculus and we prove that it satisfies relational parametricity. The proof relies on a step-indexed Kripke logical relation. The step-indexing is required to make the logical relation well-defined in the case for the dynamic type. The possible worlds include the mapping of generated type names to their types and the mapping of type names to relations. We prove the Fundamental Property of this logical relation and that it is sound with respect to contextual equivalence. To demonstrate the utility of parametricity in the polymorphic blame calculus, we derive two free theorems.
Available in: pdf, doi.Session types are a rich type discipline, based on linear types, that lift the sort of safety claims that come with type systems to communications. However, web-based applications and micro services are often written in a mix of languages, with type disciplines in a spectrum between static and dynamic typing. Gradual session types address this mixed setting by providing a framework which grants seamless transition between statically typed handling of sessions and any required degree of dynamic typing. We propose GradualGV as an extension of the functional session type system GV with dynamic types and casts. We demonstrate type and communication safety as well as blame safety, thus extending previous results to functional languages with session-based communication. The interplay of linearity and dynamic types requires a novel approach to specifying the dynamics of the language.
Available in: pdf, doi.TypeScript participates in the recent trend among programming languages to support gradual typing. The DefinitelyTyped Repository for TypeScript supplies type definitions for over 2000 popular JavaScript libraries. However, there is no guarantee that implementations conform to their corresponding declarations. We present a practical evaluation of gradual typing for TypeScript. We have developed a tool for use with TypeScript, based on the polymorphic blame calculus, for monitoring JavaScript libraries and TypeScript clients against the TypeScript definition. We apply our tool, TypeScript TPD, to those libraries in the DefinitelyTyped Repository which had adequate test code to use. Of the 122 libraries we checked, 62 had cases where either the library or its tests failed to conform to the declaration. Gradual typing should satisfy non-interference. Monitoring a program should never change its behaviour, except to raise a type error should a value not conform to its declared type. However, our experience also suggests serious technical concerns with the use of the JavaScript proxy mechanism for enforcing contracts. Of the 122 libraries we checked, 22 had cases where the library or its tests violated non-interference.
# Available in: pdf, doi, artifact.The data abstraction mechanism of Miranda may be adapted to a dynamically typed programming language by applying ideas from gradual typing.
# Available in: pdf, doi.We connect three ways to achieve relational parametricity: uni- versal types, runtime type generation, and cryptographic sealing. We study a polymorphic blame calculus, λB, inspired by that of Ahmed, Findler, Siek, and Wadler (2011), that ties universal types to runtime type generation; and a cryptographic lambda calculus, λK, inspired by that of Pierce and Sumii (2000), that relies on cryptographic sealing. Our λB calculus avoids the "topsy turvy" aspects of Ahmed et al., who evaluate terms one would expect to be values, and leave as values terms one would expect to be evaluated. We present translations from λB to λK and back that we show to be simulations. We extract from λB the subset λG that corresponds to the polymorphic lambda calculus λF of Girard (1972) and Reynolds (1974); λG is also a subset of the system G studied by Neis, Dreyer, and Rossberg (2009). We present translations from λF to λG and back that we show to be fully abstract. Further, we shed light on the embedding given by Pierce and Sumii of λF into λK, describing how it is related to the composition of our translations from λF to λG and λB to λK, and that the conversions and casts of λB relate to the C and G components of their embedding.
C#, Dart, Pyret, Racket, TypeScript, VB: many recent languages integrate dynamic and static types via gradual typing. We systematically develop three calculi for gradual typing and the relations between them, building on and strengthening previous work. The calculi are: λB, based on the blame calculus of Wadler and Findler (2009); λC, inspired by the coercion calculus of Henglein (1994); λS inspired by the space-efficient calculus of Herman, Tomb, and Flanagan (2006) and the threesome calculus of Siek and Wadler (2010). While λB is little changed from previous work, λC and λS are new. Together, λB, λC, and λS provide a coherent foundation for design, implementation, and optimisation of gradual types.
We define translations from λB to λC and from λC to λS. 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: λC has a particularly simple definition, and the subtle definition of blame safety for λB is justified by the simple definition of blame safety for λC. Our calculus λ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 λC to λS to validate the challenging part of full abstraction between λB and λC; and, second, using full abstraction from λB to λS to easily establish the Fundamental Property of Casts, which required a custom bisimulation and six lemmas in earlier work.
Contracts, gradual typing, and hybrid typing all permit less-precisely typed and more-precisely typed code to interact. Blame calculus encompasses these, and guarantees blame safety: blame for type errors always lays with less-precisely typed code. This paper serves as a complement to the literature on blame calculus: it elaborates on motivation, comments on the reception of the work, critiques some work for not properly attending to blame, and looks forward to applications. No knowledge of contracts, gradual typing, hybrid typing, or blame calculus is assumed.
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.
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.
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.
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.
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.
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.
Last modified: Mon Sep 14 10:46:00 BST 2009