View publication

Title Plausible Sealing for Gradual Parametricity
Authors Elizabeth Labrada, Matías Toro, Éric Tanter, Dominique Devriese
Publication date April 2022
Abstract Graduality and parametricity have proven to be extremely
challenging notions to bring together. Intuitively, enforcing parametricity
gradually requires possibly sealing values in order to detect violations of
uniform behavior. Toro et al. (2019) argue that the two notions are
incompatible in the context of System F, where sealing is transparently
driven by potentially imprecise type information, while New et al. (2020)
reconcile both properties at the cost of abandoning the syntax of System F
and requiring user-provided sealing annotations that are not subject to
graduality guarantees. Furthermore, all current proposals rely on a global
form of dynamic sealing in order to enforce parametric behavior at runtime,
which weakens parametric reasoning and breaks equivalences in the static
language. Based on the observation that the tension between graduality and
parametricity comes from the early commitment to seal values based on type
information, we propose plausible sealing as a new intermediate language
mechanism that allows postponing such decisions to runtime. We propose an
intermediate language for gradual parametricity, Funky, which supports
plausible sealing in a simplified setting where polymorphism is restricted
to instantiations with base and variable types. We prove that Funky
satisfies both parametricity and graduality, mechanizing key lemmas in Agda.
Additionally, we avoid global dynamic sealing and instead propose a novel
lexically-scoped form of sealing realized using a representation of evidence
inspired by the category of spans. As a consequence, Funky satisfies a
standard formulation of parametricity that does not break System F
equivalences. In order to show the practicality of plausible sealing, we
describe a translation from Funk, a source language without explicit
sealing, to Funky, that takes care of inserting plausible sealing forms. We
establish graduality of Funk, subject to a restriction on type applications,
and explain the source-level parametric reasoning it supports. Finally, we
provide an interactive prototype along with illustrative examples both novel
and from the literature.
Pages 70:1-70:28
Volume 6
Journal name Proceedings of the ACM Programming Languages
Publisher ACM Press (New York, NY, USA)
Reference URL View reference page