This post is meant as an explainer about how substructural type theory can be applied in programming language design. Terms like “substructural type theory” tend to scare and confuse programmers who don’t write Haskell on the weekends, so one thing programming language designers should do when thinking about how they will present their language is invent metaphors, even slightly misleading ones, to help more ordinary programmers understand how their language works. One such term is “ownership.”

Not infrequently, objects in a program come to represent something outside of themselves; they are not “pure data” but some kind of resource with identity. A classic example of this might be a sort of handle granting exclusive access to a resource. For this to really work well you want to know that to get that object you had to execute certain code (a “constructor”), that when the object is no longer used some other code will be executed (a “destructor”), and that while the object is in scope, no concurrently executing code also has an object representing the same exclusive resource (that it is not “aliased”). This is what ownership (as presented in Rust, at least) is all about.

I want to demystify ownership and substructural types in the hopes that this will become more common knowledge. Nothing in this post is really groundbreaking - if you’re already “in the know,” it will contain no new information - but it does contain some notes on aspects of Rust’s implementation that I think are incorrect (one of which would even be easy to change).

…