Linearity, Uniqueness, Ownership: An Entente Cordiale

on YouTube ↗32m

" summary

Claims that linearity and uniqueness serve different temporal guarantees—linearity restricts the future, uniqueness guarantees the past—and that both plus Rust-style ownership can coexist in a single graded system. Demonstrates an extended type system implemented in Granule, proved correspondence to fractional permissions and graded modalities, and shows concrete rules (share, clone) that enable destructive updates on unique mutable arrays and safe borrowing via fractional permissions. Presents ESOP/OOPSLA papers and an implemented prototype.

AI-written summary · about

" chapters (15)

1. 0:00Introduction
2. 1:04Granule and research background
3. 3:10Linear types with cake analogy
4. 5:15Graded modal types beyond binary
5. 8:46Uniqueness types and coffee analogy
6. 11:13Linearity versus uniqueness
7. 13:40Linearity and uniqueness in Granule
8. 16:28Mutable arrays example
9. 16:49Ownership in Rust-like systems
10. 19:35Graded modalities for uniqueness
11. 21:19Recap and related research
12. 23:03Summary of linearity types
13. 24:18Q&A: Fractional permissions
14. 28:09Q&A: Unique ownership
15. 30:00Q&A: Linear basis