Gradually Typing Strategies
summary
Adds a gradual type system to Stratego with a prototype type checker and cast inserter that type-checks code and emits runtime casts; applied to Jasmin (an existing Java bytecode assembler) with 3,200 LOC, 36 files, 146 strategies/rules, producing 117 new top-level type signatures of which 85 are fully static. The prototype finds real bugs (mismatched literal types, overly general patterns, list-vs-element confusions), preserves generic traversals via type-preserving strategies, and leaves runtime cast insertion and performance engineering for future work.
AI-written summary · about
chapters (16)
- 0:00Intro
- 1:02Stratego Usage Scenario
- 2:07III-Typed Trees Must Be Allowed
- 3:09Idiomatic Transformation Pipelines
- 3:26Types Already in Stratego
- 5:11Rewrite Rules: Execution
- 5:27Strategies
- 8:08Type System Requirements
- 8:57Gradual Types to the Rescue
- 9:26Top-Level Type Annotations and Patterns
- 10:15Type Inference for Variables
- 10:28Type Preserving Transformations
- 11:47Evaluation on Jasmin (Assembler)
- 12:39Evaluation on Jasmin (Interpreter)
- 14:01Future Work
- 14:41Conclusion
related talks
15mTaming Type Annotations in Gradual Typing
15mWell-Typed Programs Can Go Wrong: A Study of Typing-Related Bugs in JVM Compilers
27mTowards Type Debugging using Partial Evaluation
18mGradual Typing for Effect Handlers
56mOn Type-Based Techniques for Program Manipulation
19mGradual Correctness: a Dynamically Bidirectional Full-Spectrum Dependent Type Theory
58mPanel discussion: Types for All: From weak to strong, from static to dynamic
23mBehavioural up/down casting for statically typed languages