Capture Checking - A New Approach to Effect Safety in Scala
summary
Capture Checking adds capability tracking into Scala’s type system and turns runtime resource-leak crashes (for example returning a file handle from a scoped block) into compile errors; the compiler already emits errors for those leaks and the standard library has been annotated in nightlies with capture sets. It uses boxing to suspend captures in generic code, supports effect polymorphism and classifiers for finer filtering, includes separation checks, and has a mechanized soundness proof in Lean.
AI-written summary · about
chapters (11)
- 0:00Capture checking in Scala
- 2:28Fixing resource leaks
- 7:23Classes with capture annotations
- 12:40Subcapturing and lineage
- 13:01Effect polymorphism
- 19:22Path-dependent types
- 21:27Implicit vs explicit polymorphism
- 22:51Boxing for generic code
- 26:23Full Scala standard library
- 32:22Advanced classifier capabilities
- 34:54Maturity and availability
related talks
01h 03mInside the Scala Capture Checker
01h 23mCapture Tracking in Scala
31mReal-Life Scala Capture Checking
01h 03mWhere Are We With Scala's Capabilities?
41mWhere Are We With Scala's Capabilities?
20mSystem Capybara: Capture Tracking for Ownership and Borrowing
54mHow to avoid safety hazards when using closures in Scala
24mLet the Scala compiler work for you