Skip to content

Gradual Typing & Polymorphism Papers

Jump to bottom
Brandon Kase edited this page Feb 10, 2021 · 19 revisions

The first paper introducing gradual typing formally. Gradual typing for functional languages based on the intuition that the structure of a type may be partially known/unknown at compile-time and we wish to find incompatibilities between the known parts. The static parts of programs are both safe and performant, the dynamic part gives flexibility. Introduces a type consistency relation which is more or less type equality but allows dynamic types.

Adds more formalism on top of the first paper to clarify semantics: Gradual Guarantee -- If a gradually typed program is well-typed, then removing type annotations always produces a program that is still well-typed. A program remains well-typed so long as only correct type annotations are added. "correct" means the annotation agrees with the corresponding annotation in some fully annotated and well-typed version of the program. Soundness guarantee for gradual typing in terms of blame: upcasts never result in blame, only downcasts or cross-casts. Runtime semantics in this paper assign blame labels properly. The paper then reviews existing languages' claims of gradual typing against the gradual guarantee.

This paper develops System F_G a gradually typed system F. And proves that System F_G satisfies most of the Gradual Guarantee defined above. Define type consistency of System F_G as an extension of System F. Polymorphic types can be consistent with nonpolymorphic ones only if the nonpolymorphic one contains the dynamic type: Because of this, the paper is an "explicitly polymorphic" system. Introduces the notion of quasi-polymorphism -- types that are polymorphic or contain the dynamic type. Includes discussion that you have to be careful to keep parametricity when evaluating programs that include the dynamic type using runtime type bindings but can erase them when annotations are given (so as to not sacrifice performance).

This paper shows a declarative and algorithmic higher-rank predicative polymorphic language with bidirectional typing that is sound, complete, and simple. Type checking and synthesis judgements are standard -- there's also a separate type application judgement. Completeness and soundness are subject to beta-eta equality. Type annotations are needed only on bindings of polymorphic type. Substitution: We can freely inline let-bindings and analysis and synthesis doesn't change. Inverse Substitution: We can extract any subterm to a let-binding if we add an annotation. Annotation Removal: so we can still not require annotations for some of the let-bindings. The algorithmic type system takes the rules that guess the types and create existential type variables -- not quite unification variables; uses ordered algorithmic contexts. Context extension governs the idea that we only add information to contexts. Judgements are only added.

This paper extends the original Gradual Typing for Functional Languages paper with support for polymorphic subtyping and subsumes the original definition -- note this is an "implicitly polymorphic" system not an explicit one as described above. Proves that the new calculus satisfies all static aspects of the refined criteria for gradual typing. Provides a bidirectional system ala Complete and Easy above: Differs in (1) Adds unknown type \star, (2) Matching judgement, (3) Gradual inference only produces static types. This paper only really thinks about the statics. New consistent subtyping relation is built from consistency and subtyping orthogonally: Solve by doing subtype, consistency, subtype. Relates consistent subtyping to alternative approaches in other papers: Static subtyping, precision. Dynamic part of the gradual guarantee is still in question.

Clone this wiki locally