Kindly Bent to Free Us

TL;DR

The paper introduces Affe, an ML extension that manages resource safety through linear and affine types, borrowing, and inference, aiming to reduce bugs and vulnerabilities in systems programming.

Contribution

Affe extends ML with linearity and affinity types, borrowing features from Rust, without requiring annotations, enhancing resource safety in functional programming.

Findings

Supports resource management with affine and linear types

Enables borrowing of resources similar to Rust

Maintains ML's type inference and abstraction features

Abstract

Systems programming often requires the manipulation of resources like file handles, network connections, or dynamically allocated memory. Programmers need to follow certain protocols to handle these resources correctly. Violating these protocols causes bugs ranging from type mismatches over data races to use-after-free errors and memory leaks. These bugs often lead to security vulnerabilities. While statically typed programming languages guarantee type soundness and memory safety by design, most of them do not address issues arising from improper handling of resources. An important step towards handling resources is the adoption of linear and affine types that enforce single-threaded resource usage. However, the few languages supporting such types require heavy type annotations. We present Affe, an extension of ML that manages linearity and affinity properties using kinds and constrained types. In addition Affe supports the exclusive and shared borrowing of affine resources, inspired by features of Rust. Moreover, Affe retains the defining features of the ML family: it is an impure, strict, functional expression language with complete principal type inference and type abstraction. Affe does not require any linearity annotations in expressions and supports common functional programming idioms.