Abstracting Gradual Typing Moving Forward : Precise and Space-Efficient
summary
AGT gets two concrete fixes: a new evidence abstraction called bounded rows and records makes consistent evidence composition forward-complete, which prevents spurious subtyping witnesses that previously let hidden fields slip through; and forward-completeness forces consistent transitivity to be associative and to have a size bound, so runtime checks can be composed eagerly without growing the call stack. The result is a mechanically derived gradual semantics that enforces modular type invariants and preserves constant-space tail recursion.
AI-written summary · about
chapters (18)
- 0:00Intro
- 0:13What is gradual typing?
- 1:13Abstracting gradual typing (2016)
- 2:03AGT applications ...
- 2:17AGT framework...
- 2:35Problem 1: Does not enforce modular invariants An Example
- 5:11AGT by example - Record Subtyping
- 5:49Make all static type constraints explicit
- 6:31Abstracting Gradual Typing Define Gradual Types
- 11:59Problem 1: Precision Let's revisit the original problem
- 14:38Forward-complete gradual operations
- 15:10Forward completeness in Record Subtyping
- 15:27Outline for this talk
- 15:59Fixing the gradual design (draft)
- 16:21Rows still introduce noise!
- 16:50Fixing the gradual design (final)
- 18:06Two Requirements for Space Efficiency
- 19:04Abstracting Gradual Typing Moving Forward
related talks
22mIs Space-Efficient Polymorphic Gradual Typing Possible?
21mGradual Typing is the best!
15mTaming Type Annotations in Gradual Typing
33mStatically Typed Interpreters
45mDepending on Types
35mGADTs and You; Writing Safer Code Using GADTs
33mTyped Clojure: From Optional to Gradual Typing
23mGradual Typing in Python