Practical Type Inference with Levels
summary
Formalizes the implementation trick called levels for Hindley‑Milner style systems, covering generalization, local data types, and higher‑rank polymorphism, proves mechanized soundness and completeness for the level‑based declarative system, and delivers an Koka implementation of level‑based type inference. Benchmarks use nested programs (up to 200 nested functions, 10 runs averaged) and show the level approach avoids whole‑context traversals and noticeably speeds generalization versus the original Koka checker.
AI-written summary · about
chapters (8)
- 0:00Introduction
- 2:28Level-based type system
- 8:15Local data types
- 10:25Higher rank polymorphism
- 13:36Mechanized proofs
- 15:20Case studies in Koka
- 16:43Performance results
- 17:24Conclusion & Q&A
related talks
14mScalability and Precision by Combining Expressive Type Systems and Deductive Verification
14mA Lightweight Type-and-Effect System for Invalidation Safety: Tracking Permanent and(…)
15mAutomatic and Efficient Variability-Aware Lifting of Functional Programs
01h 02mAdvanced Levelization Techniques (part 2 of 3)
13mA Type System for Extracting Functional Specifications from Memory-Safe Imperative Programs
15mGradual Verification of Recursive Heap Data Structures
22mFrom FP to OOP and Back, Consistently
01h 00mAdvanced Levelization Techniques (part 1 of 3)