Ordered Types for Typestate
summary
Derives a calculus that encodes typestate as sets of allowed future traces and uses ordered context semicolons as temporal consumption order, so borrows are implemented by a single split operation that returns an ordered pair (borrow view + leftover). Uses bunched contexts and regular-language product derivative to compute a unique best leftover type for borrows; shows when let-like rewrites break size preservation (so three different let forms or an effect/value discipline are needed). Demonstrates the approach models read/write/close protocols and avoids explicit object identities.
AI-written summary · about