Modular Borrowing Without Ownership or Linear Types

on YouTube ↗30m

" summary

Claims a practical way to get Rust-like temporary borrowing without ownership or linear types by tracking uses as effects and encoding forbidden regions with Boolean negation types, implemented atop a type-and-effect system with generalized MLstruct Boolean-algebraic subtyping and higher-rank polymorphism. Shows concrete encodings: iterator-invalidations prevented, exception handlers as capabilities, mutable buffers with safe iteration and parallel nesting, and a prototype implementation that typechecks and rejects leaked effects while letting code be refactored freely via the new tracked binding construct.

AI-written summary · about

" chapters (19)

1. 0:00Introduction
2. 1:02Borrowing semantics disclaimer
3. 2:06Scope safety and guarantees
4. 3:09Tracked instance construct
5. 4:31Type and effect system basics
6. 5:55Tracking mutation with effects
7. 8:23Referential transparency
8. 9:49Ambient effects and ergonomics
9. 10:31Exception safety with combinators
10. 13:00Mutable collections safely
11. 14:23Iterator lifetime restrictions
12. 16:10Modular refactoring without syntax
13. 17:12Non-lexical lifetimes
14. 18:37Safe concurrency with effects
15. 19:19Type system foundations
16. 20:23Implementation progress
17. 20:43Related work and philosophy
18. 21:04Conclusion
19. 22:13Q&A