Capturing Types (TOPLAS)
summary
A minimal calculus called CC<:◻ capture calculus extends System F<: with capture sets so types record which capability-like free variables values may retain, and a Scala extension implementation uses scoped capabilities as implicit parameters to unify effects and resources. The prototype migrates parts of the Scala collections with almost no API changes, flags unsafe lazy iterators requiring extra annotations, proves soundness and gives an algorithmic checker and concurrency extensions.
AI-written summary · about
chapters (10)
- 0:00Introduction
- 1:11Motivation for effects and resources
- 2:58Capability vs classical effects
- 5:47Handling resources in Scala
- 7:58Capability derivation and hierarchy
- 10:11Capture calculus CC⊆
- 12:21Capture sets in polymorphism
- 13:26Annotation burden on Scala collections
- 14:51Formal results and overview
- 15:33Questions and answers session
related talks
01h 03mInside the Scala Capture Checker
51mHands-on Typelevel Scala
30mEffects,capabilities,and boxes: from scope-based reasoning to type-based reasoning and back
19mFrom Capabilities to Regions: Enabling Efficient Compilation of Lexical Effect ...
13mOne-Pass CPS Translation of Dependent Types (Talk Proposal)
56mOn Type-Based Techniques for Program Manipulation
46mScala's Role in the Programming Languages Ecosystem
23mType-Level Programming with Match Types