Repository logo

Infoscience

  • English
  • French
Log In
Logo EPFL, École polytechnique fédérale de Lausanne

Infoscience

  • English
  • French
Log In
  1. Home
  2. Academic and Research Output
  3. Journal articles
  4. What’s in the Box: Ergonomic and Expressive Capture Tracking over Generic Data Structures
 
research article

What’s in the Box: Ergonomic and Expressive Capture Tracking over Generic Data Structures

Xu, Yichen  
•
Bračevac, Oliver  
•
Pham, Cao Nguyen  
Show more
October 9, 2025
Proceedings of the ACM on Programming Languages

Capturing types in Scala unify static effect and resource tracking with object capabilities, enabling lightweight effect polymorphism with minimal notational overhead. However, their expressiveness has been insufficient for tracking capabilities embedded in generic data structures, preventing them from scaling to the standard collections library – an essential prerequisite for broader adoption. This limitation stems from the inability to name capabilities within the system’s notion of box types. This paper develops System Capless, a new foundation for capturing types that provides the theoretical basis for reach capabilities (rcaps), a novel mechanism for naming “what’s in the box”. The calculus refines the universal capability notion into a new scheme with existential and universal capture set quantification. Intuitively, rcaps witness existentially quantified capture sets inside the boxes of generic types in a way that does not require exposing existential capture types in the surface language. We have fully mechanized the formal metatheory of System Capless in Lean, including proofs of type soundness and scope safety. System Capless supports the same lightweight notation of capturing types plus rcaps, as certified by a type-preserving translation, and also enables fully optional explicit capture-set quantification to increase expressiveness. Finally, we present a full reimplementation of capture checking in Scala 3 based on System Capless and migrate the entire Scala collections library and an asynchronous programming library to evaluate its practicality and ergonomics. Our results demonstrate that reach capabilities enable the adoption of capture checking in production code with minimal changes and minimal-to-zero notational overhead in a vast majority of cases.

  • Details
  • Metrics
Type
research article
DOI
10.1145/3763112
Author(s)
Xu, Yichen  

École Polytechnique Fédérale de Lausanne

Bračevac, Oliver  

École Polytechnique Fédérale de Lausanne

Pham, Cao Nguyen  

École Polytechnique Fédérale de Lausanne

Odersky, Martin  

École Polytechnique Fédérale de Lausanne

Date Issued

2025-10-09

Publisher

Association for Computing Machinery (ACM)

Published in
Proceedings of the ACM on Programming Languages
Volume

9

Issue

OOPSLA2

Start page

1726

End page

1753

Editorial or Peer reviewed

REVIEWED

Written at

EPFL

EPFL units
LAMP1  
FunderFunding(s)Grant NumberGrant URL

FNSNF

TMAG-2_209506/1

Available on Infoscience
October 14, 2025
Use this identifier to reference this record
https://infoscience.epfl.ch/handle/20.500.14299/254902
Logo EPFL, École polytechnique fédérale de Lausanne
  • Contact
  • infoscience@epfl.ch

  • Follow us on Facebook
  • Follow us on Instagram
  • Follow us on LinkedIn
  • Follow us on X
  • Follow us on Youtube
AccessibilityLegal noticePrivacy policyCookie settingsEnd User AgreementGet helpFeedback

Infoscience is a service managed and provided by the Library and IT Services of EPFL. © EPFL, tous droits réservés