How to Evaluate Blame for Gradual Types, Part 2
summary
Empirical study instruments a rational-programmer procedure, mutates GTB benchmark programs, and runs three TyRet/Racket semantics (eraser, transient, natural) to see which runtime error info helps locate mistaken type interfaces. Result: natural with blame lets the automated procedure translate runtime failures into static type errors and locates bugs with a 20–40% improvement over other modes; transient blame is mixed; dynamic checks without blame often perform worse than eraser, which still detects most bugs (≈5% lower).
AI-written summary · about
chapters (12)
- 0:00Introduction
- 1:04TypeScript gradual typing
- 3:54Type interface mistakes
- 5:18Alternative semantics
- 7:03Semantics in action
- 10:15Research question
- 12:01Hypothesis on errors
- 15:30Bug location procedure
- 18:18Experiment design
- 20:23Results analysis
- 22:50Key takeaways
- 24:35Summary
related talks
27mTowards Type Debugging using Partial Evaluation
15mWell-Typed Programs Can Go Wrong: A Study of Typing-Related Bugs in JVM Compilers
26mType Narrowing the Hard Way
17mFrom Traces to Program Incorrectness: A Type-Theoretic Approach
56mOn Type-Based Techniques for Program Manipulation
16mGradually Typing Strategies
15mTaming Type Annotations in Gradual Typing
19mGradual Correctness: a Dynamically Bidirectional Full-Spectrum Dependent Type Theory