Space-Efficient Polymorphic Gradual Typing, Mostly Parametric
summary
Claim: space-efficient gradual typing becomes possible when polymorphism is restricted to mostly parametric, meaning parametricity is enforced only for instantiations with non- types. The paper defines a coercion calculus λCmp with type names and four new coercions, then implements a space-efficient form λSmp*, proves translation from λCmp to λSmp is type- and semantics-preserving, and proves λSmp guarantees statically bounded runtime coercion size, so the implementation works.
AI-written summary · about
chapters (6)
- 0:00Polymorphic gradual typing intro
- 2:10Parametric polymorphism
- 5:05Space efficiency challenges
- 7:12Why mostly parametric works
- 15:44Lambda C and S calculi
- 16:32Q&A on practical implications
related talks
21mSeamless Scope-Safe Metaprogramming Through Polymorphic Subtype Inference (Short Paper)
21mPolymorphic Type Inference for Dynamic Languages
28mSemi-explicit polymorphic parameters
13mOne-Pass CPS Translation of Dependent Types (Talk Proposal)
43mAdding kind-polymorphism to the Scala programming language
19mGradual Correctness: a Dynamically Bidirectional Full-Spectrum Dependent Type Theory
36mDependently Typed Multi-Stage Programming, Revisited
18mGradual Typing for Effect Handlers