Type Inference Techniques: Implementation and Formalization, Better Together
summary
Argues that informal compiler hacks need formal proofs and demonstrates this with two concrete cases: scope checks for high‑rank polymorphism implemented via level numbers and the untouchable variables discipline for GADTs. Shows a real GHC corner‑case where levels let a program be accepted despite the formal outside‑in specification (a bug present for over 10 years and since fixed). Presents a Koka implementation with microbenchmarks and ongoing work toward a mechanized, level‑based formalization.
AI-written summary · about
chapters (9)
- 0:00Welcome
- 1:05Type system components
- 4:14Implementation techniques
- 8:05High rank polymorphism
- 13:30Implementation levels
- 16:00Generalized algebraic data types issues
- 21:39GHC bug gap
- 23:46Current work
- 24:28Q&A
related talks
24mLet the Scala compiler work for you
42mSuggesting Valid Substitutions For Typed Holes
01h 00mA Type-Safe Structure Editor Calculus + Strictly Capturing Non-Strict Closures
50mSharing Is Caring - How to Let the Compiler Know What You're Thinking
01h 06mOn-The-Fly Verification via Incremental, Interactive Abstract Interpretation wi...
20mGetting into the Flow: Towards Better Type Error Messages for Constraint-Based ...
22mScale By The Bay 2018 Unconference: Omer Van Kloeten
16mIncremental Proof Development in Dafny with Module-Based Induction