Functional Ownership through Fractional Uniqueness

TL;DR

This paper introduces a novel type system that integrates fractional permissions and grading to model ownership and borrowing, bridging the gap between Rust's ownership model and functional programming type systems.

Contribution

It presents the first account of ownership and borrowing that combines fractional permissions with grading, extending the Granule language to unify these concepts within a standard type system.

Findings

Shows Rust's ownership as a graded generalisation of uniqueness.

Develops a type system integrating fractional permissions with grading.

Extends Granule with new ownership and borrowing concepts.

Abstract

Ownership and borrowing systems, designed to enforce safe memory management without the need for garbage collection, have been brought to the fore by the Rust programming language. Rust also aims to bring some guarantees offered by functional programming into the realm of performant systems code, but the type system is largely separate from the ownership model, with type and borrow checking happening in separate compilation phases. Recent models such as RustBelt and Oxide aim to formalise Rust in depth, but there is less focus on integrating the basic ideas into more traditional type systems. An approach designed to expose an essential core for ownership and borrowing would open the door for functional languages to borrow concepts found in Rust and other ownership frameworks, so that more programmers can enjoy their benefits. One strategy for managing memory in a functional setting is through uniqueness types, but these offer a coarse-grained view: either a value has exactly one reference, and can be mutated safely, or it cannot, since other references may exist. Recent work demonstrates that linear and uniqueness types can be combined in a single system to offer restrictions on program behaviour and guarantees about memory usage. We develop this connection further, showing that just as graded type systems like those of Granule and Idris generalise linearity, Rust's ownership model arises as a graded generalisation of uniqueness. We combine fractional permissions with grading to give the first account of ownership and borrowing that smoothly integrates into a standard type system alongside linearity and graded types, and extend Granule accordingly with these ideas.