Plausible sealing for gradual parametricity
summary
Proposes plausible sealing: postpone sealing decisions by inserting “maybe-seal” evidence so runtime, not static imprecision, decides whether a value is sealed. Builds an intermediate language Funky, models evidence as sets of category-theory–style spans with partial pullback composition, proves both parametricity and graduality (mechanized in Agda), and gives a translation from source Funk (instantiations limited to base types and type variables). Provides an interactive prototype and explains when transitivity fails as a runtime error.
AI-written summary · about
chapters (24)
- 0:00Plausible sealing introduction
- 0:22Parametric polymorphism
- 1:48Relational parametricity
- 2:31Gradual typing basics
- 3:33Graduality challenges
- 4:14Why gradual parametricity hard
- 5:38Global dynamic sealing
- 6:42Seal or not seal
- 8:08Type-driven vs term-driven
- 9:52Plausible sealing intro
- 10:55How plausible sealing works
- 12:15Lexical vs global sealing
- 13:18Advantages of lexical sealing
- 14:18Fully abstract embedding
- 14:40Embedding cryptographic lambda
- 15:24Multiple sealing behaviors
- 16:27Intermediate language Funky
- 17:11Evidence-based gradual types
- 18:37Type precision with spans
- 20:25Generalizing evidence spans
- 21:30Consistent transitivity
- 22:34Parametricity in Funky
- 23:17Future work
- 24:16Q&A
related talks
18mDeveloping a Dependently Typed Language with Runtime Proof Search
21mSeamless Scope-Safe Metaprogramming Through Polymorphic Subtype Inference (Short Paper)
01h 07mAn introduction to synthetic guarded domain theory with applications to probabilistic(…)
01h 05mAll the Languages Together
27mTaming Unsoundness with Gradual Abstract Interpretation
18mEpistemic Logic for Polyglots (Short Paper)
18mDeferring the Details and Deriving Programs
19mGradual Correctness: a Dynamically Bidirectional Full-Spectrum Dependent Type Theory