What's in the Box: Ergonomic and Expressive Capture Tracking over Generic Data(…)
summary
Claims a new calculus System Capless with existential and universal capture-set quantification and a named mechanism rcaps that lets generic boxed capabilities be referenced without exposing existentials in surface code. Metatheory is fully mechanized in Lean with proofs of type soundness and scope safety. Implements a Scala 3 capture checker, migrates the entire collections library and an async library with minimal signature changes, runs in nightly builds and targets shipment in Scala 3.8.
AI-written summary · about
chapters (14)
- 0:00Capture tracking motivation
- 1:03What is capture tracking
- 2:28Capabilities and effects
- 3:11Capture types syntax
- 4:16Lightweight polymorphism in Scala
- 5:41Boxes and tunneling explained
- 6:43C subbox limitations
- 8:33Explicit polymorphism solution
- 9:14Capless system design
- 10:37Balancing notations
- 11:59Redesigning notations
- 12:41Capture checking Scala collections
- 13:04Future extensions
- 13:48Q&A
related talks
15mTypestate via Revocable Capabilities
55mSet Theoretic Algebraic Constructive Calculus
50mSimple code for a type safe world
30mConstraint Typing with Boolean Algebra
28mType-Driven Prompt Programming: From Typed Interfaces to a Calculus of Constraints
55mThe Shape of Shapeless (Part 2)
44mType level Computations in Scala
23mType-Level Programming with Match Types