Solver-based Gradual Type Migration

on YouTube ↗12m

" summary

TypeWhich automates gradual type migration by emitting GTLC constraints solved with an off‑the‑shelf MaxSMT-based constraints backend instead of custom solvers, and encodes objectives like minimize syntactic coercions to prefer fewer coercions. It supports a compatibility mode that yields fully compatible migrations and a precise mode that improves far more types at the cost of some incompatibilities. Evaluation: 22 GTLC benchmarks (12 prior, 10 new) plus 11 Grift programs; TypeWhich recovers human annotations on 9/11 Grift benchmarks and reconstructs all but one program overall.

AI-written summary · about

" chapters (14)

1. 0:00Intro
2. 0:29Type Migration: Adding or Improving Type Information
3. 0:59Some Prior Approaches to Gradual Type Migration
4. 1:54Precision Matters
5. 4:29What Matters for Automatic Type Migration?
6. 4:51TypeWhich: Our Approach to Gradual Type Migration
7. 5:12Syntax-Directed Constraint Generation
8. 6:52Phase 1: Precise Migration
9. 7:47Phase 2: Compatible Migration
10. 8:38Variations on Compatibility
11. 9:14Evaluation
12. 9:46GTLC Benchmarks
13. 10:36Grift Benchmarks
14. 11:06Conclusion