Uniqueness for Behavioural Types

Jane Street has been developing modal types for OCaml – an extension to the type system where modes track properties of values, such as their scope, thread sharing, and aliasing. These modes restrict which operations are permitted on values, enabling safer and more efficient systems programming. In this post, I focus on the uniqueness mode, which tracks aliasing, and show how it can eliminate certain runtime checks. My intention in this post is not to explain how the different modes work. There are a number