Borrowing describes the process in which a tracked resource can be temporarily shared and used in a special form before being returned to the original resource owner/handler. This is an old idea that was more recently popularized in the Rust programming language. In Rust, borrowing is used to guarantee memory safety by making mutability and aliasing mutually exclusive and bounding the lifetimes of borrowed references. This in turn depends crucially on Rust’s ownership system, which is a substructural type system with a coarse representation of value lifetimes that significantly restricts the space of valid programs. But the basic idea of borrowing also makes sense independently of such ownership and substructural systems, and in particular it makes sense in more classical garbage-collected and high-level programming languages. In this context, it can for example be used to prevent iterator invalidation and to make structured concurrency “fearless” by preventing data races.

In this talk, I propose a new take on borrowing based on a type and effect system and Boolean algebraic subtyping. Instead of restricting the aliasing of sensitive resources, we track their uses as side effects in the type system. Then, we encode borrowing by describing regions in which certain effects cannot occur – which is represented through the use of Boolean negation types. Moreover, using a slight generalization of MLstruct’s Boolean-algebraic subtype inference allows us to express programs that make use of borrowing without any type annotations in user programs. Finally, since our borrowing discipline is entirely type-based (and not syntactic, unlike Rust’s borrow-checker), we can freely modularize the code by, for instance, moving arbitrary parts of an implementation into helper functions, enabling fearless refactoring.

After Lionel’s talk, we’ll have a lunch together outside the campus with members from the HKUST TACO group. In the afternoon, we’ll have some free discussions in CB308. Please join us!