Greedy Implicit Bounded Quantification

on YouTube ↗18m

" summary

Presents F≤b, a variant of kernel F≤ with greedy implicit instantiation that handles bounded quantification, interdependent bounds, higher-rank polymorphism, and hard cases where local inference fails. Gives a declarative bidirectional system and a worklist algorithm that is proven sound, complete, and decidable, and shows completeness with respect to kernel F≤ including impredicative instantiations. All proofs are mechanically formalized in Abella (~25,000 lines) and a small Haskell implementation and reusable artifacts are provided.

AI-written summary · about

" chapters (12)

1. 0:00Introduction
2. 0:22Greedy implicit bounded quantification
3. 1:27Type inference challenges
4. 3:18Local type inference limits in Scala 2
5. 5:05No interdependent bounds in Scala 2
6. 6:10Hard to synthesize type arguments
7. 7:38Higher rank type inference problems
8. 9:28Calculus F subb
9. 11:19Monotype with bounded quantification
10. 12:44F subb variants and properties
11. 13:53Contributions
12. 14:59Q&A