Gradual System F

TL;DR

This paper introduces GSF, a gradual version of System F that maintains parametricity and explores its semantics, metatheory, and potential for practical programming, addressing longstanding challenges in gradual typing with polymorphism.

Contribution

The paper presents GSF, the first gradual parametric language based on System F, with a detailed semantics, metatheory, and analysis of its properties and limitations.

Findings

GSF preserves relational parametricity in a gradual setting

The semantics and metatheory of GSF are rigorously developed

Extensions toward practical language features are discussed

Abstract

Bringing the benefits of gradual typing to a language with parametric polymorphism like System F, while preserving relational parametricity, has proven extremely challenging: first attempts were formulated a decade ago, and several designs have been recently proposed, with varying syntax, behavior, and properties. Starting from a detailed review of the challenges and tensions that affect the design of gradual parametric languages, this work presents an extensive account of the semantics and metatheory of GSF, a gradual counterpart of System F. In doing so, we also report on the extent to which the Abstracting Gradual Typing methodology can help us derive such a language. Among gradual parametric languages that follow the syntax of System F, GSF achieves a unique combination of properties. We clearly establish the benefits and limitations of the language, and discuss several extensions of GSF towards a practical programming language.