Kindly Bent to Free Us
summary
A new ML extension called Affe enforces linearity and affinity so a database use-after-free example compiles in OCaml but is rejected at compile time here. It combines kinds and constrained types with exclusive and shared borrowing plus regions to let closures capture linear resources safely, supports impure strict ML idioms, and delivers complete principal type inference via an HM(X)-style constraint solution. A prototype is available online; current limits are no flow sensitivity and no concurrency story yet.
AI-written summary · about
chapters (10)
- 0:00Intro
- 0:20"high severity security bugs" in Chromium
- 0:49Let's write some OCaml code
- 3:09Linearity through kinds
- 4:55Functions and captures
- 7:30Borrows - Example of uses
- 9:23Everything together
- 11:56Inference in action
- 13:10The Affe language - Summary
- 14:01The theory - Summary
related talks
16mTowards formally secure compilation of verified F* programs against unverified ML(…)
57mInvited Talk: Bridging Safety and Performance
14mA Lightweight Type-and-Effect System for Invalidation Safety: Tracking Permanent and(…)
33mExtensible Effects: A Leaner Cake for Purely Functional Code
33mResource polymorphism: proposal for integrating first-class resources into ML
52mConstraints Liberate, Liberties Constrain
47mExtensibly Free Arrows
40mRetrofitting Concurrency – Lessons from the Engine Room