Coursera Flash Sale
40% Off Coursera Plus for 3 Months!
Grab it
Explore a conference presentation that introduces System Capless, a new theoretical foundation for capturing types in Scala that enables ergonomic and expressive capture tracking over generic data structures. Learn how researchers from EPFL developed reach capabilities (rcaps), a novel mechanism for naming capabilities within box types that addresses previous limitations in tracking capabilities embedded in generic data structures. Discover how this advancement makes it possible to scale capture checking to Scala's standard collections library, which is essential for broader adoption of capturing types. Examine the theoretical foundations including existential and universal capture set quantification, and understand how rcaps witness existentially quantified capture sets inside generic type boxes without exposing existential capture types in the surface language. Review the fully mechanized formal metatheory implemented in Lean, including proofs of type soundness and scope safety. Analyze the practical implementation through a complete reimplementation of capture checking in Scala 3 based on System Capless, and evaluate the migration results of the entire Scala collections library and an asynchronous programming library that demonstrate minimal changes and minimal-to-zero notational overhead in production code.
