A Friendly Tour of Substructural, Uniqueness, Ownership, and Capabilities Types — and more!
A Friendly Tour of Substructural, Uniqueness, Ownership, and Capabilities Types — and more!
THIS POST IS NOT YET COMPLETED.
-->
This post is part of The Eter programming<br>Language series.
Edit: Take a look at the discussion in the Programming Languages subreddit.
This is the third post in the series dedicated to the Eter programming language, a side project that allows me to take my mind off the research I have to conduct.<br>The previous posts are Mutable Value Semantics (MVS) or Ownership & Borrowing: A Trade-off Analysis and The Mutable Value Semantics (MVS): A Non-superficial Study.<br>If you are interested in the project, you can find more information in the<br>Eter compiler monorepo.<br>The Eter language reference and the<br>Eter Doxygen documentation, although not yet complete,<br>are also good starting points.
The first post, in its prelude, introduces what we are currently researching for the Eter language.<br>Then, it discusses the mutable value semantics (MVS) and how the popular programming languages (e.g., Swift , Hylo ) implement it.<br>The second post covers the trade-offs between MVS and ownership & borrowing, examining friction points in Rust, Hylo, and Swift while searching for common ground between the two memory models.
Contrary to what I mentioned in the previous two posts, this post is once again not part of the Eter language itself. I needed to provide this post to clarify some concepts I consider fundamental to the language's design, semantics, and type system.
What follows is meant to be a friendly tour. We start from the logical roots of why ordinary type systems fall short, walk through linear, affine, and uniqueness types, and then visit the broader family—regions, effects, capabilities, typestate, and the very recent work on reachability and separation. I keep the theory light on purpose; the goal is intuition and a map of the landscape, with pointers to the literature for the details.
Resources are not Truths
Classical logic treats propositions as eternal truths. If you know that \(A\) holds, you may use that fact as many times as you like, pass it around freely, and ignore it when you don't need it. This is exactly the behavior we want from mathematical knowledge—and exactly the behavior we get from values in a conventional type system.
Programs, however, spend much of their time juggling resources: file handles, memory, locks, network connections. Resources do not behave like truths. A file handle used twice may corrupt state; a lock acquired but never released deadlocks; memory freed and then read invites undefined behavior. The type systems we inherit from the simply-typed \(\lambda\)-calculus have no vocabulary for "this value must be used exactly once" or "there must never be two copies of this reference".
This is the gap that an entire family of type systems sets out to close. Their common ancestor is a branch of logic—substructural logic—and their descendants include Rust's ownership system, Haskell's linear types, Scala's capabilities, and the object-capability security model. The rest of this post is a tour of that family.
Restricting Use: Substructural Types
The first family asks a deceptively simple question: how many times may a variable be used? By giving up some of the structural rules we are about to meet, these systems turn ordinary hypotheses into resources that have to be spent carefully—and that is already enough to make memory, file handles, and locks safe.
Substructural Type Systems
Let me give an informal introduction to substructural type systems, uniqueness types, and fractional uniqueness, for those who are not familiar with them.<br>Substructural type systems resemble the idea of substructural logic.<br>They are based on the following structural rules (where \(\Gamma\) is the context of assumptions):
Exchange , the order of assumptions in \(\Gamma\) does not matter. That is, the order of variable declarations does not influence the semantics of the program.<br>\[<br>\frac{\Gamma_1, x : A, y : B, \Gamma_2 \vdash t : C}<br>{\Gamma_1, y : B, x : A, \Gamma_2 \vdash t : C}<br>\]<br>Weakening , assumptions can be discarded (ignored). That is, variables can be declared but not used in the program.<br>\[<br>\frac{\Gamma \vdash t : A}<br>{\Gamma, x : B \vdash t : A}<br>\quad x \notin FV(t)<br>\]<br>Contraction , assumptions can be duplicated. That is, two "copies" of the same variable are equivalent.<br>\[<br>\frac{\Gamma, x : A, x : A \vdash t : B}<br>{\Gamma, x : A \vdash t : B}<br>\]
Substructural type systems arise by selectively restricting these rules. Removing different rules yields different disciplines for how often a variable may appear:
SystemExchangeWeakeningContractionVariable use
Ordered✗✗✗Exactly once, in order<br>Linear ✓✗✗Exactly once<br>Affine ✓✓✗At most once<br>Relevant✓✗✓At least once<br>Normal✓✓✓Arbitrarily
To cite a few, linear type systems (resembling linear logic ) disallow both weakening and contraction,...