Skip to content

Gradual Typing & Polymorphism Papers

Jump to bottom
Cyrus Omar edited this page Feb 2, 2023 · 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); compiles to System F_C.

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.

Uses a different algorithm based on worklists for implementing the DK system (from the paper above). Claims that this makes proofs simpler, and it may be a more straightforward implementation technique as well.

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.

This paper reviews the challenges around gradually typing System F and introduces "Gradual System F" (or GSF). It establishes the benefits and limitations of the unique properties of this system. Contributions: (1) Studies existing design issues, (2) applies a general methodology to gradualize PLs onto a language similar to System F, (3) introduces gradual parametricity -- which enforces parametricity at runtime even when it's not provable statically, "cheap theroems" instead of free theorems understood modulo errors and divergence; enforces soundness (and shows how GSF satisfies this), (4) Derives GSF from SF via a Galois connection between "abstraction" and "concretization" functions over SF -- ala Abstracting Gradual Typing (Garcia, Clark, Canter. SIGPLAN 2016). The approach uses careful tracking of evidence and definitions of consistent transitivity which leads to stronger parametricity properties than other Gradual System Fs before. However, approach doesn't track blame during evaluation. (5) satisfies static part of gradual guarantee and a weaker form of the dynamic part of the gradual guarantee -- also known as Weak Graduality: allows only for extrinsic precision loss (dynamic type can't appear in binders only ascriptions). The paper shows that System F syntax and strong Graduality are at odds with one another, (6) Shows you can embed a language with dynamic sealing (7) Explores a novel technique for implementing implicit polymorphism dynamically and (8) studies the addition of existential types to GSF.

This paper shows that by modifying the syntax of System F+extistentials to make type name gen explicit and introducing dynamic sealing and unsealing primitives for each type, we can get an explicitly polymorphic language that satisfies strong graduality and parametricity. Contributions: (1) identify type-directed computation as the common cause of graduality and parametricity violations in prior work -- pure gradual System F needs type-directed computation so we cannot get the free lunch (2) and it shows that GSF can exhibit non-parametric behavior (3) presents a new language PolyG^v: supports universal and existential types with a notion of type-binding and the dynamic sealing/unsealing primitives. For existentials, we're used to the burden of manual sealing and unsealing (ala newtypes in Haskell). For universals, it's a bit awkward. The party that instantiates the abstract type is the party that determines which values are sealed and unsealed. For existential types this is the module, for universal types it's the continuation of the instantiation. Some judgments have a context that is generated as a result of type bindings -- scope expands outwards (4) Elaborates PolyG^v into an explicit cast calculus PolyC^v -- unique in that it has two forms of casts: upcast and downcast (5) gives a translation of PolyC^v into a call-by-push-value with polymorphism and extensible sum types language to give it meaning and (6) develop a novel logical relation that proves graduality and parametricity for PolyG^v -- parametricity is the reflexive case of the graduality theorem. There are two interesting relevant remarks towards the end of the paper: (1) There is an alternate design of PolyG^v which avoids the outwards binding and makes type-bindings' scope explicit with a let-binding and (2) one can introduce sealing combinators to the surface syntax to slightly improve the syntactic burden of manually placing seals and unseals.

This paper extends the idea of Typed holes with Explicit Polymorphism through PolyG^v and Hazel. Major considerations: (1) Unspecified formal type parameters are assigned a fresh type variable X' for the type forall X'. A, (2) Term syntax is extended with \Lambda .M so incomplete programs with explicit type instantiation don't reduce, (3) Programs M containing unbound term or type variables by putting them inside holes and giving them different type environments. The combined language is elaborated into a cast calculus similar to the above paper and progress and preservation is proven. Future work: Considering edit actions -- they note that a challenge is environments around non-empty holes which are assumed as oracles in the paper.

Introduces the idea of a maybeSealed to address both graduality and parametricity together.

Clone this wiki locally