Is Space-Efficient Polymorphic Gradual Typing Possible?
summary
Argument shows that preserving parametric polymorphism plus standard gradual-typing guarantees prevents a generic space-efficient implementation: a formal impossibility theorem proves there exists a counterexample family of programs whose cast/coercion structures accumulate and force unbounded space overhead, and a prototype interpreter demonstrates the effect concretely, producing quadratic-style blowup for sequences of length n rather than linear space; the paper extracts the exact semantic assumptions behind the negative result.
AI-written summary · about
chapters (7)
- 0:00Introduction to talk
- 3:32Core problem of gradual typing
- 7:14Existing solutions and limitations
- 10:05Proposed approach overview
- 13:51Key techniques explained
- 17:28Demonstration and results
- 20:04Q&A session
related talks
19mAbstracting Gradual Typing Moving Forward : Precise and Space-Efficient
21mGradual Typing is the best!
15mTaming Type Annotations in Gradual Typing
49mThe Trouble With Types
33mTyped Clojure: From Optional to Gradual Typing
22mSubtyping is Overrated
11mThe Secrets of Polymorphic Variants
14mTransitioning from Structural to Nominal Code with Efficient Gradual Typing