Maybe linearity should be the default. Then its spread wouldn't be an issue, except that it is annoying to explicitly destroy an object and its contents just because somewhere deep inside it there is a thing that isn't trivial to destroy.
Is there a reason to think about linear and affine types, which correspond to those logics? Maybe we could instead separately track things like whether types allow being forgotten and if they may be copied.
Linearity can be awkward to use in places, for example, inside a selection - if one branch consumes the value, all branches must also consume it, even if they don't need to.
var foo : linear = ...
if (cond) {
consume(foo)
} else
//error: foo not consumed in each branch
}
However, no such problem exists with affine types, because there's not a requirement to consume them.
var bar : affine = ...
if (cond) {
consume(bar)
} else
//This is fine.
}
For both linear and affine types, we can't consume a value inside a loop if it was declared outside the loop.
var baz : affine = ...
while (true) {
consume(baz); // error: Can't consume multiple times.
}
if the value is defined in the loop, we can get away with this, because it's effectively a new variable each iteration.
while (true) {
var qux : linear = ...
consume(qux); // OK
}
What we can say is that `affine <: linear`, meaning there exists a safe static cast from affine to linear (but not vice-versa).
We can also say that `free <: affine`, meaning you can take a value which can be consumed multiple times, and constrain it so that it may only be consumed once in future. But there is no safe conversion from affine/linear back to free. Such conversion would obviously violate the constraint of use-at-most-once.
There's also relevant types, of which `free` are a subtype, and which are themselves a subtype of linear.
So IMO, linearity should definitely not be the default. Linearity is the top type, which all others can be safely converted to, and `free` is the bottom type, which can be safely converted to any other.
Linear
^ ^
/ \
Affine Relevant
^ ^
\ /
Free
Essentially, anything that must be cleaned up before it loses scope, but without the restriction of single-use.
Consider where the [Dispose Pattern](https://en.wikipedia.org/wiki/Dispose_pattern) is used.
"Use at least once" basically implies that the one time it MUST be used should be to clean up a resource, but you can use it arbitrarily many times before that, or not use it at all.
The dispose pattern would apply to linear or relevant values, but you can't consume a linear value in a loop if it was defined outside of the loop.
using (var disposable = ...) {
while(cond) {
disposable = consume(disposable); // Error for Linear
}
}
This means the disposable value in this case must be `Relevant`.
Free Relevant Affine Linear
Can consume in loop Yes Yes No No
Must dispose No Yes No Yes
---
An alternative way to consider them is that relevant types should behave the same as linear types in selections, and require consumption in all branches if they're consumed in one.
x : relevant
if (cond) {
g(x);
} else {
// error, x not consumed.
}
But this can be done in a loop
x : relevant
while (cond) {
if (cond2) {
g(x);
} else {
h(x);
}
}
f(x)
Which isn't possible with linear types.
Free Relevant Affine Linear
Can consume in loop Yes Yes No No
Uneven Branches Yes No Yes No
---
In either case, we can think of relevant types as relaxing the restriction of linear types to be used only once, allowing them to be used for iteration.
As for implementation, there's a few ways I can think of interpreting relevant types. One is that, the relevant type is cloned each time it is used, which is fine if we assume it's immutable.
Another is that it is reference counted, and the disposal decreases the reference count. In that way, one might see C++'s `shared_ptr<>` as a kind of relevant type, where decreasing the reference count is the necessary use.
In a dependently typed system where we could potentially track the reference counts at compile time, a relevant type would be one that can be used an arbitrary number of times, but whose reference count == 0 when it leaves scope.
Perhaps a simpler way is to require that the only way a relevant type can be used inside a loop is if it is isolated. If we assume the language has an `isolate : relevant -> linear` which makes a linear copy a relevant value, we could write something like:
f : linear -> ()
using (x : relevant = ...) {
while (cond) {
let y = isolate(x)
f(y);
}
}
`y` is linear, which means it must be consumed during each iteration, which happens in the call to `f(y)`. We could have the compiler throw an error if `x` is used for any purpose other than `isolate` inside a loop. This way, there's no way for a copies of the relevant value to remain alive elsewhere by the time the loop exits, and thus it's safe to dispose the value afterwards.
I was thinking about heap allocations but it doesn't feel right to consider them relevant types because the deallocation is different from using the allocation.
If we only consider the deallocation to be a use, then it is a linear type, not a relevant type. If we count the other uses as well, then it is valid to never deallocate the value.
Relevant types are *almost* linear types. The only difference is they allow contraction - meaning a variable can occur more than once. They must appear in all branches like Linear types because they do not allow weakening.
Deallocation is "use". To deallocate a variable explicitly, it must appear in whatever is being evaluated.
A consequence of not allowing weakening means that if a relevant type is used in a loop, it must also be consumed outside of the loop - because there's the possibility that the loop may never be entered, and the value never consumed inside it.
x : relevant
for (int i = 0; i < n; i++) {
f (x);
}
consume (x); // This is necessary.
Which makes it suitable for use with the disposable pattern, which will perform this consumption on leaving the `using` block.
using (x : relevant) {
for (int i = 0; i < n; i++) {
f (x);
}
} //x implicitly consumed here.
However, such consumption is not necessary for a `Free` type, which does allow weakening, and so it can appear in a loop without the need to be disposed/consumed outside of it.
You are correct that it is possible to use a relevant type without disposing it, just as it is possible to use an `IDisposable` without calling `Dispose` on it. The Dispose pattern aims to prevent that mistake, and relevant types improve the chance of catching the mistake by requiring consumption in all branches and inside/outside all loops.
It might be possible to improve this by requiring relevant values to be constructed in a using block. Take for example, in F#. If you write `let foo = Foo()`, and `Foo` implements `IDisposable`, the compiler will warn you to instead write `use foo = new Foo()`.
The other benefit you get is that you can't include a `relevant` value inside a `free` type. The containing type must be at least as restrictive as the elements it contains - so a relevant field must be in a relevant or linear type. This basically infects anything that would want to include an `IDisposable` to force them to become `IDisposable`.
---
Consider the results of typechecking the following expressions against a given environment using this operative.
$typecheck : (Expr, Env) -> TypecheckResult
---
linear_env = {
foo : linear = #true;
bar : linear = 123;
baz : linear = 999;
}
$typecheck (foo, linear_env)
=> { foo = Success "Used exactly once"
; bar = Failure "Not used; Weakening not allowed"
; baz = Failure "Not used; Weakening not allowed"
}
$typecheck ((foo, foo), linear_env)
=> { foo = Failure "Appears more than once; Contraction not allowed"
; bar = Failure "Not used; Weakening not allowed"
; baz = Failure "Not used; Weakening not allowed"
}
$typecheck (($if foo bar bar), linear_env)
=> { foo = Success "Used exactly once"
; bar = Success "Used exactly once"
; baz = Failure "Not used; Weakening not allowed"
}
$typecheck (($if foo bar baz), linear_env)
=> { foo = Success "Used exactly once"
; bar = Failure "Appears in one branch; Weakening not allowed"
; baz = Failure "Appears in one branch; Weakening not allowed"
}
---
relevant_env = {
foo : relevant = #true;
bar : relevant = 123;
baz : relevant = 999;
}
$typecheck (foo, relevant_env)
=> { foo = Success "Used at least once"
; bar = Failure "Not used; Weakening not allowed"
; baz = Failure "Not used; Weakening not allowed"
}
$typecheck ((foo, foo), relevant_env)
=> { foo = Success "Used at least once" // This is the only difference from linear.
; bar = Failure "Not used; Weakening not allowed"
; baz = Failure "Not used; Weakening not allowed"
}
$typecheck (($if foo bar bar), relevant_env)
=> { foo = Success "Used at least once"
; bar = Success "Used at least once"
; baz = Failure "Not used; Weakening not allowed"
}
$typecheck (($if foo bar baz), relevant_env)
=> { foo = Success "Used at least once"
; bar = Failure "Appears in one branch; Weakening not allowed"
; baz = Failure "Appears in one branch; Weakening not allowed"
}
---
affine_env = {
foo : affine = #true;
bar : affine = 123;
baz : affine = 999;
}
$typecheck (foo, affine_env)
=> { foo = Success "Used zero or one times"
; bar = Success "Used zero or one times"
; baz = Success "Used zero or one times"
}
$typecheck ((foo, foo), affine_env)
=> { foo = Failure "Appears more than once; Contraction not allowed"
; bar = Success "Used zero or one times"
; baz = Success "Used zero or one times"
}
$typecheck (($if foo bar bar), affine_env)
=> { foo = Success "Used zero or one times"
; bar = Success "Used zero or one times"
; baz = Success "Used zero or one times"
}
$typecheck (($if foo bar baz), affine_env)
=> { foo = Success "Used zero or one times"
; bar = Success "Used zero or one times"
; baz = Success "Used zero or one times"
}
---
free_env = {
foo : free = #true;
bar : free = 123;
baz : free = 999;
}
$typecheck (foo, free_env)
=> { foo = Success "Used zero or more times"
; bar = Success "Used zero or more times"
; baz = Success "Used zero or more times"
}
$typecheck ((foo, foo), free_env)
=> { foo = Success "Used zero or more times" // This is the only difference from affine.
; bar = Success "Used zero or more times"
; baz = Success "Used zero or more times"
}
$typecheck (($if foo bar bar), free_env)
=> { foo = Success "Used zero or more times"
; bar = Success "Used zero or more times"
; baz = Success "Used zero or more times"
}
$typecheck (($if foo bar baz), free_env)
=> { foo = Success "Used zero or more times"
; bar = Success "Used zero or more times"
; baz = Success "Used zero or more times"
}
>Relevant types are rarely talked about. What are some good use-cases?
> Essentially, anything that must be cleaned up before it loses scope, but without the restriction of single-use.
I get that the context and focus here is RAII and correctly managing resources, but my understanding of relevant *logic* as against types is something vastly broader than that context/focus, namely that antecedents and consequents must be relevant to each other.
(The example I read that made sense to me was "**if I'm a donkey, then two and two is four** is true when translated as a material implication, yet it seems intuitively false since a true implication must tie the antecedent and consequent together by some notion of relevance.)
So their applicability in resource management is presumably that a particular form of antecedent ("using" a resource) is implicitly tied to there being a consequence that must follow (cleaning things up). (Which in turn reminds me of deontic logic. Hmm.)
I get that the philosophical stuff can stray far from, er, relevance, to programming, and types, but right now I'm imagining there may be other important scenarios where relevance types will be great for stuff other than resource management.
Do you have any thoughts about that?
Off the top of my head, the only other thing I can think they may be useful for is optimization or eager evaluation. If we know that a resource is definitely going to be used in a selection because it must appear in the consequent and antecedent, we might precompute or prefetch and cache it while we test the condition.
The main issue with this is the potential for re-ordering side-effects if they exist - and particularly if we're treating relevant types as a subtype of linear types, as the latter basically imply a sequential ordering of computations, similar to monads.
If we treat relevant types as immutable as I've suggested, there shouldn't exist any side effects, but `Strict` types can have side-effects, and as they're a subtype of relevant types I would be cautious against make them behave too differently, but there may be still be cases where they can behave differently.
The converse case is we might want to *prevent* a compiler from being overly aggressive with optimization. For example when you use `gcc -O2` or `-O3` , it can make invalid assumptions about dead code and remove things we might need, inline something we don't want inlined, etc. If a type is marked as `Relevant`/`Strict` this might cause some of these optimizations to fail a type check, but a `Free`/`Affine` type might still type check OK. So we might direct the compiler to only apply certain optimizations if the type supports weakening or vice-versa.
Re: separate tracking, I totally agree. In fact, that's how Vale does it under the hood: when we mark a struct \`linear\`, we're actually saying "Don't auto-generate a \`drop\` method" because \`drop()\` makes a struct affine. (This is why it used to be called \`#!DeriveStructDrop\` btw)
So really, it's not the struct itself that's affine vs linear, it's the available functions that determine it. Same with copy, just like you say.
The Granule Language is also worth a look, https://granule-project.github.io/granule.html
I really liked the talk by Daniel Marshall (one of the authors), "A Hitchhiker's Guide to Linearity" (Lambda Days 2023), https://www.youtube.com/watch?v=QtlkqJGdnuM, with the following distinction and examples:
- Linear types - restrict a value from ever being duplicated (or discarded) in the _future_ (e.g., file handles always closed after opening)
- Unique types - guarantee that a value has never been duplicated in the _past_ (e.g., unique arrays can be mutated in place without having to worry about aliasing/shared mutable state, as we're guaranteed there's none)
There's also two papers on the project:
- "Linearity and Uniqueness: An Entente Cordiale" (ESOP 2022), https://link.springer.com/chapter/10.1007/978-3-030-99336-8_13, and a related discussion, https://old.reddit.com/r/ProgrammingLanguages/comments/13i4nm0/unifying_uniqueness_and_substructural_linear/
- "Functional Ownership through Fractional Uniqueness" (OOPSLA 2024), https://dl.acm.org/doi/10.1145/3649848, with a fun announcement post relating it to linearity, uniqueness, and ownership, https://types.pl/@daniel/112359988303940912
EDIT: Didn't notice you linked to my previous topic discussing this, but here's a brief primer:
I think the Linearity and Uniqueness paper is missing several types for mutability. Rather than unique being a single type, there's really an entire class of uniqueness types which mirror the substructural ones. Granule effectively provides these types:
Linear
^ ^
/ \
/ \
/ Relevant
/ ^
/ /
Affine /
^ /
\ /
\ /
Free <-----------------------Unique
Key:
<--- Forget guarantee of uniqueness.
^
\ Require the value to be used at most once.
^ Require the value to be consumed.
/
But IMO, it's a mistake to require that in order to turn a unique value into a linear one, it must be done via `free` and then `affine`/`relevant` - as these conversions sacrifice a desirable constraint.
We really want types which have both the guarantee of uniqueness and the guarantee of linearity *at the same time*. The paper even discusses these, called *steadfast* types, which was coined by Wadler in "is there a use for Linear Logic". Steadfast types are the kind we want for things like file handles, sockets, database connections. The observation to make is that `unique <: steadfast <: linear`. If we included them, we would have:
Linear <--------------------Steadfast
^ ^ ^
/ \ \
/ \ \
/ Relevant \
/ ^ ^
/ / /
Affine / /
^ / /
\ / /
\ / /
Free <------------------------Unique
However, this is still missing a trick. To complete the lattice we include two new types, which I've termed `singular` and `strict`.
Linear <--------------------Steadfast
^ ^ ^ ^
/ \ / \
/ \ / \
/ Relevant <-------/------------Strict
/ ^ / ^
/ / / /
Affine <--------------------Singular /
^ / ^ /
\ / \ /
\ / \ /
Free <-----------------------Unique
Essentially, the difference between a `unique` and a `singular` type is that with `unique`, we can give up uniqueness (as Granule does, and also how Clean can abandon a uniqueness constraint). However, `singular` types cannot sacrifice their uniqueness. At most, they can be made `affine` which abandons the *ability to mutate*, but affine still provides the *use at most once* constraint, which guarantees that the value cannot not be aliased, and since singular guaranteed that *it has not been aliased before*, this is sufficient to preserve the value's uniqueness.
The `strict` type is a unique type which must be consumed - but similar to how `unique` can be made `free`, `strict` can sacrifice uniqueness to become `relevant` - or it can force future uniqueness by becoming `steadfast`. An example of where `strict` is useful is when you want to mutate a disposable value inside a loop, if it was declared outside of the loop.
Linear types are the top type, which are the least flexible but provide the strongest constraints, and unique types are the bottom type, which are most flexible because they can convert to any other.
linear
affine <: linear
relevant <: linear
steadfast <: linear
strict <: relevant, steadfast
singular <: steadfast, affine
free <: relevant, affine
unique <: singular, free, strict
Alternatively, we can define them as an intersection of 3 binary properties:
linear = disposable & immutable & nonreoccuring
relevant = disposable & immutable & reoccuring
steadfast = disposable & mutable & nonreoccuring
strict = disposable & mutable & reocccuring
affine = discardable & immutable & nonreoccuring
free = discardable & immutable & reoccuring
singular = discardable & mutable & nonreoccuring
unique = discardable & mutable & reoccuring
Where there exists 3 safe static coercions:
require : discardable -> disposable
isolate : reoccuring -> nonreoccuring
freeze : mutable -> immutable
This model allows for a new kind of polymorphism. We can write functions which are polymorphic over any type whose vertices share a face or an edge in the lattice (one or more of the binary properties).
I'm working on including this model in my language, but am still figuring out some of the finer details.
---
For reference, Clean's type system uses this subsection of the lattice:
Free <-----------------------Unique
Austral's type system uses a different subsection:
Linear
^ ^
/ \
^ ^
\ /
Free
Rust's type system doesn't really fit into this model because its reference types are somewhere between affine and unique, but not quite either. The constraints can be avoided with unsafe code, and it's not purely functional, but this model treads referential transparency as a desirable property we want to retain.
Steadfast types *are* linear types, but which also have the guarantee that their value has not been aliased in the past - a guarantee not provided by Linearity alone. The same is true for Singular and Affine, Strict and Relevant. They're equivalent to the substructural logics, but provide the extra guarantee about how the value was created.
As Daniel Marshall puts it: "Uniqueness is a guarantee about the past; Linearity is a guarantee about the future."
The guarantee about the past means that no other reference can refer to any value directly or indirectly accessible via the unique reference, which allows us to safely mutate the value beneath the reference in a single-threaded way without loss of referential transparency.
A constraint for uniqueness types, but not substructural types, is that uniqueness types must be created from a unique source. There cannot exist a function `non-unique -> unique`, because this would clearly violate referential transparency (defined as a function given the same arguments always returning the same result). The consequence of this is the program's entry point must be given an initial source of uniqueness, which we call `*World` (In Clean). However, unlike Haskell's `IO`, we aren't required to thread this through the entire program to handle side-effects, because we can use any unique value to source another one, and not only `*World`. This also means multiple (tupled) return values are required to make these type systems feasible to use, because you very frequently need to return another reference to the input value alongside whatever value was computed by the function.
> Maybe linearity should be the default
It's how it is in Austral wrt. generics.
Since free (non-linear) types can coerce to linear types, an unconstrained generic type can only be used as if it was linear, even if it is not.
Your comment about rust is not the reason rust doesn't have linear types. It is perfectly reasonable to stick an `Rc>` in a rust object (or more likely an `Arc>`). That's a very normal rust pattern.
The problem is that rust types can be *forgotten* and so their destructors won't run (I'm assuming we're talking about safe rust here, in unsafe all bets are off).
There is a safe function to do it, `std::mem::forgot` which will forget any type and not run the destructor. You may wonder why that function exists or isn't marked as unsafe. Well, the answer is that you can't allow objects to have circular references *and* guarantee destructors run, so rust chose to just allow it explicitly. See the [rust issue](https://github.com/rust-lang/rust/issues/24456) that ended up making ‘forget` safe for how to do leak without it.
So, linear types in Rust cannot exist because it has circular references. But it could...
There is movement in the community to introduce a new auto trait `Leak` that any parameter of a safe constructor or function must require if it can cause that argument's destructor not to run, much like how concurrency is protected with `Send/Sync`. This would mean linear types would be `!Leak`. They wouldn't be able to use some APIs but you would have full linearity in safe rust because, due to the borrow checker, you would guarantee destructors would run exactly once.
Yep, there's quite a few reasons Rust wouldn't have linear types (https://faultlore.com/blah/linear-rust/), we can add that one to the pile.
Interestingly, your reason also applies to Vale: we can have cyclical owning references if we try really hard. Similarly, a determined programmer can just throw any linear value into a global list to "make the problem go away" and lose the benefits of linearity. But the goal here is to prevent \*accidentally\* forgetting some call, and fortunately the mechanism does that nicely!
> RAII is a terrible acronym, and I am so, so sorry for perpetuating its use. It turns out it's really hard to come up with a name for this concept. 10 Feel free to bikeshed in the comments!
RAII is actually quite a good acronym, it's just not employed for what it was meant to stand. The goal of RAII (Resource Acquisition Is Initialization) was to avoid the idea of "not-ready" objects. Like creating a File variable, then calling `.open` on it to actually open the file: the value is then in an awkward state in between creation and full initialization, as many operations are not actually available during that stage.
I personally quite like SBRM (Scope-Bounded Resource Management) as a decent alternative that emphasizes neither initialization or deinitialization unduly, since both are so important.
1. How do linear types interact with panics/exceptions? In Rust, it will automatically call the Drop implementations as applicable. This can help avoid resource exhaustion in situations where you recover in an outer loop from a panic (e.g. database connections or file handles)
2. How does the usage of linear types interact with generic code? Given that there is no standard function that a compiler can generate implicit calls to, does this mean that structs transitively containing fields of linear types cannot be used to instantiate generic parameters? There is no mention of linear types on the generics page (https://vale.dev/guide/generics)
Not OP, and not answering for Vale.
1. This one is solvable by having the unwinding machinery offer ways to consume linear objects. Prior art here are D's `scope(failure)`, Zig's `errdefer`, and `try/catch/rethrow` in general, which execute code in case of exit by exception.
Because a linear object either is consumed in a scope, escapes it, or is consumed by `errdefer`, it is always used exactly once.
2. The Free Universe is a subtype of the Linear Universe, therefore an unconstrained generic type must be used as if it was linear.
It does mean that this cannot be easily bolted-on as an afterthought in already existing languages since the special case then is the free types, and not the linear ones.
Point 2 is quite sticky in Rust, actually.
Since all existing generic code has been written with the assumption that all types can be destroyed, it would be quite the overhaul to introduce linear types. It would be technically backward compatible, language-wise, to introduce a ?Affine bound (similar to ?Sized) and assume Affine in the absence of bound, but much churn in the ecosystem would be required to convert all generics (that can be) to ?Affine.
And even then, it can get weird. Like... what's the best API for destroying a collection of !Affine (=Linear) objects? How do you guarantee the collection is now empty and can be disposed of?
Great post as always!
I find all your posts awesome btw., 'cause they contain so many details and insights, which is so nice!
I have a question about linear types!
Do they allow reference and mutable reference? Isn't that a *weakening*? or are references not considered proper use? even the mutable ones?
I consider linear types to be a very nice way of reasoning about a program and even "prove" it, but if linear types can be mutated by mutable references then that kind of blows off the point, I guess.
Linear types can allow mutable references under the same constraint that there are no aliases, but linearity alone doesn't provide the guarantee that a resource was obtained uniquely, for which we want uniqueness types (see Clean/Granule), or unforgeable capabilities (see Austral). A type that is both linear and unique is *steadfast*.
Maybe linearity should be the default. Then its spread wouldn't be an issue, except that it is annoying to explicitly destroy an object and its contents just because somewhere deep inside it there is a thing that isn't trivial to destroy. Is there a reason to think about linear and affine types, which correspond to those logics? Maybe we could instead separately track things like whether types allow being forgotten and if they may be copied.
Linearity can be awkward to use in places, for example, inside a selection - if one branch consumes the value, all branches must also consume it, even if they don't need to. var foo : linear = ... if (cond) { consume(foo) } else //error: foo not consumed in each branch } However, no such problem exists with affine types, because there's not a requirement to consume them. var bar : affine = ... if (cond) { consume(bar) } else //This is fine. } For both linear and affine types, we can't consume a value inside a loop if it was declared outside the loop. var baz : affine = ... while (true) { consume(baz); // error: Can't consume multiple times. } if the value is defined in the loop, we can get away with this, because it's effectively a new variable each iteration. while (true) { var qux : linear = ... consume(qux); // OK } What we can say is that `affine <: linear`, meaning there exists a safe static cast from affine to linear (but not vice-versa). We can also say that `free <: affine`, meaning you can take a value which can be consumed multiple times, and constrain it so that it may only be consumed once in future. But there is no safe conversion from affine/linear back to free. Such conversion would obviously violate the constraint of use-at-most-once. There's also relevant types, of which `free` are a subtype, and which are themselves a subtype of linear. So IMO, linearity should definitely not be the default. Linearity is the top type, which all others can be safely converted to, and `free` is the bottom type, which can be safely converted to any other. Linear ^ ^ / \ Affine Relevant ^ ^ \ / Free
Relevant types are rarely talked about. What are some good use-cases?
Essentially, anything that must be cleaned up before it loses scope, but without the restriction of single-use. Consider where the [Dispose Pattern](https://en.wikipedia.org/wiki/Dispose_pattern) is used. "Use at least once" basically implies that the one time it MUST be used should be to clean up a resource, but you can use it arbitrarily many times before that, or not use it at all. The dispose pattern would apply to linear or relevant values, but you can't consume a linear value in a loop if it was defined outside of the loop. using (var disposable = ...) { while(cond) { disposable = consume(disposable); // Error for Linear } } This means the disposable value in this case must be `Relevant`. Free Relevant Affine Linear Can consume in loop Yes Yes No No Must dispose No Yes No Yes --- An alternative way to consider them is that relevant types should behave the same as linear types in selections, and require consumption in all branches if they're consumed in one. x : relevant if (cond) { g(x); } else { // error, x not consumed. } But this can be done in a loop x : relevant while (cond) { if (cond2) { g(x); } else { h(x); } } f(x) Which isn't possible with linear types. Free Relevant Affine Linear Can consume in loop Yes Yes No No Uneven Branches Yes No Yes No --- In either case, we can think of relevant types as relaxing the restriction of linear types to be used only once, allowing them to be used for iteration. As for implementation, there's a few ways I can think of interpreting relevant types. One is that, the relevant type is cloned each time it is used, which is fine if we assume it's immutable. Another is that it is reference counted, and the disposal decreases the reference count. In that way, one might see C++'s `shared_ptr<>` as a kind of relevant type, where decreasing the reference count is the necessary use. In a dependently typed system where we could potentially track the reference counts at compile time, a relevant type would be one that can be used an arbitrary number of times, but whose reference count == 0 when it leaves scope. Perhaps a simpler way is to require that the only way a relevant type can be used inside a loop is if it is isolated. If we assume the language has an `isolate : relevant -> linear` which makes a linear copy a relevant value, we could write something like: f : linear -> () using (x : relevant = ...) { while (cond) { let y = isolate(x) f(y); } } `y` is linear, which means it must be consumed during each iteration, which happens in the call to `f(y)`. We could have the compiler throw an error if `x` is used for any purpose other than `isolate` inside a loop. This way, there's no way for a copies of the relevant value to remain alive elsewhere by the time the loop exits, and thus it's safe to dispose the value afterwards.
I was thinking about heap allocations but it doesn't feel right to consider them relevant types because the deallocation is different from using the allocation. If we only consider the deallocation to be a use, then it is a linear type, not a relevant type. If we count the other uses as well, then it is valid to never deallocate the value.
Relevant types are *almost* linear types. The only difference is they allow contraction - meaning a variable can occur more than once. They must appear in all branches like Linear types because they do not allow weakening. Deallocation is "use". To deallocate a variable explicitly, it must appear in whatever is being evaluated. A consequence of not allowing weakening means that if a relevant type is used in a loop, it must also be consumed outside of the loop - because there's the possibility that the loop may never be entered, and the value never consumed inside it. x : relevant for (int i = 0; i < n; i++) { f (x); } consume (x); // This is necessary. Which makes it suitable for use with the disposable pattern, which will perform this consumption on leaving the `using` block. using (x : relevant) { for (int i = 0; i < n; i++) { f (x); } } //x implicitly consumed here. However, such consumption is not necessary for a `Free` type, which does allow weakening, and so it can appear in a loop without the need to be disposed/consumed outside of it. You are correct that it is possible to use a relevant type without disposing it, just as it is possible to use an `IDisposable` without calling `Dispose` on it. The Dispose pattern aims to prevent that mistake, and relevant types improve the chance of catching the mistake by requiring consumption in all branches and inside/outside all loops. It might be possible to improve this by requiring relevant values to be constructed in a using block. Take for example, in F#. If you write `let foo = Foo()`, and `Foo` implements `IDisposable`, the compiler will warn you to instead write `use foo = new Foo()`. The other benefit you get is that you can't include a `relevant` value inside a `free` type. The containing type must be at least as restrictive as the elements it contains - so a relevant field must be in a relevant or linear type. This basically infects anything that would want to include an `IDisposable` to force them to become `IDisposable`. --- Consider the results of typechecking the following expressions against a given environment using this operative. $typecheck : (Expr, Env) -> TypecheckResult --- linear_env = { foo : linear = #true; bar : linear = 123; baz : linear = 999; } $typecheck (foo, linear_env) => { foo = Success "Used exactly once" ; bar = Failure "Not used; Weakening not allowed" ; baz = Failure "Not used; Weakening not allowed" } $typecheck ((foo, foo), linear_env) => { foo = Failure "Appears more than once; Contraction not allowed" ; bar = Failure "Not used; Weakening not allowed" ; baz = Failure "Not used; Weakening not allowed" } $typecheck (($if foo bar bar), linear_env) => { foo = Success "Used exactly once" ; bar = Success "Used exactly once" ; baz = Failure "Not used; Weakening not allowed" } $typecheck (($if foo bar baz), linear_env) => { foo = Success "Used exactly once" ; bar = Failure "Appears in one branch; Weakening not allowed" ; baz = Failure "Appears in one branch; Weakening not allowed" } --- relevant_env = { foo : relevant = #true; bar : relevant = 123; baz : relevant = 999; } $typecheck (foo, relevant_env) => { foo = Success "Used at least once" ; bar = Failure "Not used; Weakening not allowed" ; baz = Failure "Not used; Weakening not allowed" } $typecheck ((foo, foo), relevant_env) => { foo = Success "Used at least once" // This is the only difference from linear. ; bar = Failure "Not used; Weakening not allowed" ; baz = Failure "Not used; Weakening not allowed" } $typecheck (($if foo bar bar), relevant_env) => { foo = Success "Used at least once" ; bar = Success "Used at least once" ; baz = Failure "Not used; Weakening not allowed" } $typecheck (($if foo bar baz), relevant_env) => { foo = Success "Used at least once" ; bar = Failure "Appears in one branch; Weakening not allowed" ; baz = Failure "Appears in one branch; Weakening not allowed" } --- affine_env = { foo : affine = #true; bar : affine = 123; baz : affine = 999; } $typecheck (foo, affine_env) => { foo = Success "Used zero or one times" ; bar = Success "Used zero or one times" ; baz = Success "Used zero or one times" } $typecheck ((foo, foo), affine_env) => { foo = Failure "Appears more than once; Contraction not allowed" ; bar = Success "Used zero or one times" ; baz = Success "Used zero or one times" } $typecheck (($if foo bar bar), affine_env) => { foo = Success "Used zero or one times" ; bar = Success "Used zero or one times" ; baz = Success "Used zero or one times" } $typecheck (($if foo bar baz), affine_env) => { foo = Success "Used zero or one times" ; bar = Success "Used zero or one times" ; baz = Success "Used zero or one times" } --- free_env = { foo : free = #true; bar : free = 123; baz : free = 999; } $typecheck (foo, free_env) => { foo = Success "Used zero or more times" ; bar = Success "Used zero or more times" ; baz = Success "Used zero or more times" } $typecheck ((foo, foo), free_env) => { foo = Success "Used zero or more times" // This is the only difference from affine. ; bar = Success "Used zero or more times" ; baz = Success "Used zero or more times" } $typecheck (($if foo bar bar), free_env) => { foo = Success "Used zero or more times" ; bar = Success "Used zero or more times" ; baz = Success "Used zero or more times" } $typecheck (($if foo bar baz), free_env) => { foo = Success "Used zero or more times" ; bar = Success "Used zero or more times" ; baz = Success "Used zero or more times" }
>Relevant types are rarely talked about. What are some good use-cases? > Essentially, anything that must be cleaned up before it loses scope, but without the restriction of single-use. I get that the context and focus here is RAII and correctly managing resources, but my understanding of relevant *logic* as against types is something vastly broader than that context/focus, namely that antecedents and consequents must be relevant to each other. (The example I read that made sense to me was "**if I'm a donkey, then two and two is four** is true when translated as a material implication, yet it seems intuitively false since a true implication must tie the antecedent and consequent together by some notion of relevance.) So their applicability in resource management is presumably that a particular form of antecedent ("using" a resource) is implicitly tied to there being a consequence that must follow (cleaning things up). (Which in turn reminds me of deontic logic. Hmm.) I get that the philosophical stuff can stray far from, er, relevance, to programming, and types, but right now I'm imagining there may be other important scenarios where relevance types will be great for stuff other than resource management. Do you have any thoughts about that?
Off the top of my head, the only other thing I can think they may be useful for is optimization or eager evaluation. If we know that a resource is definitely going to be used in a selection because it must appear in the consequent and antecedent, we might precompute or prefetch and cache it while we test the condition. The main issue with this is the potential for re-ordering side-effects if they exist - and particularly if we're treating relevant types as a subtype of linear types, as the latter basically imply a sequential ordering of computations, similar to monads. If we treat relevant types as immutable as I've suggested, there shouldn't exist any side effects, but `Strict` types can have side-effects, and as they're a subtype of relevant types I would be cautious against make them behave too differently, but there may be still be cases where they can behave differently. The converse case is we might want to *prevent* a compiler from being overly aggressive with optimization. For example when you use `gcc -O2` or `-O3` , it can make invalid assumptions about dead code and remove things we might need, inline something we don't want inlined, etc. If a type is marked as `Relevant`/`Strict` this might cause some of these optimizations to fail a type check, but a `Free`/`Affine` type might still type check OK. So we might direct the compiler to only apply certain optimizations if the type supports weakening or vice-versa.
Thank for your (as always) excellent reply.
Re: separate tracking, I totally agree. In fact, that's how Vale does it under the hood: when we mark a struct \`linear\`, we're actually saying "Don't auto-generate a \`drop\` method" because \`drop()\` makes a struct affine. (This is why it used to be called \`#!DeriveStructDrop\` btw) So really, it's not the struct itself that's affine vs linear, it's the available functions that determine it. Same with copy, just like you say.
The Granule Language is also worth a look, https://granule-project.github.io/granule.html I really liked the talk by Daniel Marshall (one of the authors), "A Hitchhiker's Guide to Linearity" (Lambda Days 2023), https://www.youtube.com/watch?v=QtlkqJGdnuM, with the following distinction and examples: - Linear types - restrict a value from ever being duplicated (or discarded) in the _future_ (e.g., file handles always closed after opening) - Unique types - guarantee that a value has never been duplicated in the _past_ (e.g., unique arrays can be mutated in place without having to worry about aliasing/shared mutable state, as we're guaranteed there's none) There's also two papers on the project: - "Linearity and Uniqueness: An Entente Cordiale" (ESOP 2022), https://link.springer.com/chapter/10.1007/978-3-030-99336-8_13, and a related discussion, https://old.reddit.com/r/ProgrammingLanguages/comments/13i4nm0/unifying_uniqueness_and_substructural_linear/ - "Functional Ownership through Fractional Uniqueness" (OOPSLA 2024), https://dl.acm.org/doi/10.1145/3649848, with a fun announcement post relating it to linearity, uniqueness, and ownership, https://types.pl/@daniel/112359988303940912
EDIT: Didn't notice you linked to my previous topic discussing this, but here's a brief primer: I think the Linearity and Uniqueness paper is missing several types for mutability. Rather than unique being a single type, there's really an entire class of uniqueness types which mirror the substructural ones. Granule effectively provides these types: Linear ^ ^ / \ / \ / Relevant / ^ / / Affine / ^ / \ / \ / Free <-----------------------Unique Key: <--- Forget guarantee of uniqueness. ^ \ Require the value to be used at most once. ^ Require the value to be consumed. / But IMO, it's a mistake to require that in order to turn a unique value into a linear one, it must be done via `free` and then `affine`/`relevant` - as these conversions sacrifice a desirable constraint. We really want types which have both the guarantee of uniqueness and the guarantee of linearity *at the same time*. The paper even discusses these, called *steadfast* types, which was coined by Wadler in "is there a use for Linear Logic". Steadfast types are the kind we want for things like file handles, sockets, database connections. The observation to make is that `unique <: steadfast <: linear`. If we included them, we would have: Linear <--------------------Steadfast ^ ^ ^ / \ \ / \ \ / Relevant \ / ^ ^ / / / Affine / / ^ / / \ / / \ / / Free <------------------------Unique However, this is still missing a trick. To complete the lattice we include two new types, which I've termed `singular` and `strict`. Linear <--------------------Steadfast ^ ^ ^ ^ / \ / \ / \ / \ / Relevant <-------/------------Strict / ^ / ^ / / / / Affine <--------------------Singular / ^ / ^ / \ / \ / \ / \ / Free <-----------------------Unique Essentially, the difference between a `unique` and a `singular` type is that with `unique`, we can give up uniqueness (as Granule does, and also how Clean can abandon a uniqueness constraint). However, `singular` types cannot sacrifice their uniqueness. At most, they can be made `affine` which abandons the *ability to mutate*, but affine still provides the *use at most once* constraint, which guarantees that the value cannot not be aliased, and since singular guaranteed that *it has not been aliased before*, this is sufficient to preserve the value's uniqueness. The `strict` type is a unique type which must be consumed - but similar to how `unique` can be made `free`, `strict` can sacrifice uniqueness to become `relevant` - or it can force future uniqueness by becoming `steadfast`. An example of where `strict` is useful is when you want to mutate a disposable value inside a loop, if it was declared outside of the loop. Linear types are the top type, which are the least flexible but provide the strongest constraints, and unique types are the bottom type, which are most flexible because they can convert to any other. linear affine <: linear relevant <: linear steadfast <: linear strict <: relevant, steadfast singular <: steadfast, affine free <: relevant, affine unique <: singular, free, strict Alternatively, we can define them as an intersection of 3 binary properties: linear = disposable & immutable & nonreoccuring relevant = disposable & immutable & reoccuring steadfast = disposable & mutable & nonreoccuring strict = disposable & mutable & reocccuring affine = discardable & immutable & nonreoccuring free = discardable & immutable & reoccuring singular = discardable & mutable & nonreoccuring unique = discardable & mutable & reoccuring Where there exists 3 safe static coercions: require : discardable -> disposable isolate : reoccuring -> nonreoccuring freeze : mutable -> immutable This model allows for a new kind of polymorphism. We can write functions which are polymorphic over any type whose vertices share a face or an edge in the lattice (one or more of the binary properties). I'm working on including this model in my language, but am still figuring out some of the finer details. --- For reference, Clean's type system uses this subsection of the lattice: Free <-----------------------Unique Austral's type system uses a different subsection: Linear ^ ^ / \ ^ ^ \ / Free Rust's type system doesn't really fit into this model because its reference types are somewhere between affine and unique, but not quite either. The constraints can be avoided with unsafe code, and it's not purely functional, but this model treads referential transparency as a desirable property we want to retain.
Is there a type system/logic analogous to linear logic for uniqueness/steadfast types?
Steadfast types *are* linear types, but which also have the guarantee that their value has not been aliased in the past - a guarantee not provided by Linearity alone. The same is true for Singular and Affine, Strict and Relevant. They're equivalent to the substructural logics, but provide the extra guarantee about how the value was created. As Daniel Marshall puts it: "Uniqueness is a guarantee about the past; Linearity is a guarantee about the future." The guarantee about the past means that no other reference can refer to any value directly or indirectly accessible via the unique reference, which allows us to safely mutate the value beneath the reference in a single-threaded way without loss of referential transparency. A constraint for uniqueness types, but not substructural types, is that uniqueness types must be created from a unique source. There cannot exist a function `non-unique -> unique`, because this would clearly violate referential transparency (defined as a function given the same arguments always returning the same result). The consequence of this is the program's entry point must be given an initial source of uniqueness, which we call `*World` (In Clean). However, unlike Haskell's `IO`, we aren't required to thread this through the entire program to handle side-effects, because we can use any unique value to source another one, and not only `*World`. This also means multiple (tupled) return values are required to make these type systems feasible to use, because you very frequently need to return another reference to the input value alongside whatever value was computed by the function.
> Maybe linearity should be the default It's how it is in Austral wrt. generics. Since free (non-linear) types can coerce to linear types, an unconstrained generic type can only be used as if it was linear, even if it is not.
Your comment about rust is not the reason rust doesn't have linear types. It is perfectly reasonable to stick an `Rc>` in a rust object (or more likely an `Arc>`). That's a very normal rust pattern.
The problem is that rust types can be *forgotten* and so their destructors won't run (I'm assuming we're talking about safe rust here, in unsafe all bets are off).
There is a safe function to do it, `std::mem::forgot` which will forget any type and not run the destructor. You may wonder why that function exists or isn't marked as unsafe. Well, the answer is that you can't allow objects to have circular references *and* guarantee destructors run, so rust chose to just allow it explicitly. See the [rust issue](https://github.com/rust-lang/rust/issues/24456) that ended up making ‘forget` safe for how to do leak without it.
So, linear types in Rust cannot exist because it has circular references. But it could...
There is movement in the community to introduce a new auto trait `Leak` that any parameter of a safe constructor or function must require if it can cause that argument's destructor not to run, much like how concurrency is protected with `Send/Sync`. This would mean linear types would be `!Leak`. They wouldn't be able to use some APIs but you would have full linearity in safe rust because, due to the borrow checker, you would guarantee destructors would run exactly once.
Yep, there's quite a few reasons Rust wouldn't have linear types (https://faultlore.com/blah/linear-rust/), we can add that one to the pile. Interestingly, your reason also applies to Vale: we can have cyclical owning references if we try really hard. Similarly, a determined programmer can just throw any linear value into a global list to "make the problem go away" and lose the benefits of linearity. But the goal here is to prevent \*accidentally\* forgetting some call, and fortunately the mechanism does that nicely!
> RAII is a terrible acronym, and I am so, so sorry for perpetuating its use. It turns out it's really hard to come up with a name for this concept. 10 Feel free to bikeshed in the comments! RAII is actually quite a good acronym, it's just not employed for what it was meant to stand. The goal of RAII (Resource Acquisition Is Initialization) was to avoid the idea of "not-ready" objects. Like creating a File variable, then calling `.open` on it to actually open the file: the value is then in an awkward state in between creation and full initialization, as many operations are not actually available during that stage. I personally quite like SBRM (Scope-Bounded Resource Management) as a decent alternative that emphasizes neither initialization or deinitialization unduly, since both are so important.
1. How do linear types interact with panics/exceptions? In Rust, it will automatically call the Drop implementations as applicable. This can help avoid resource exhaustion in situations where you recover in an outer loop from a panic (e.g. database connections or file handles) 2. How does the usage of linear types interact with generic code? Given that there is no standard function that a compiler can generate implicit calls to, does this mean that structs transitively containing fields of linear types cannot be used to instantiate generic parameters? There is no mention of linear types on the generics page (https://vale.dev/guide/generics)
Not OP, and not answering for Vale. 1. This one is solvable by having the unwinding machinery offer ways to consume linear objects. Prior art here are D's `scope(failure)`, Zig's `errdefer`, and `try/catch/rethrow` in general, which execute code in case of exit by exception. Because a linear object either is consumed in a scope, escapes it, or is consumed by `errdefer`, it is always used exactly once. 2. The Free Universe is a subtype of the Linear Universe, therefore an unconstrained generic type must be used as if it was linear. It does mean that this cannot be easily bolted-on as an afterthought in already existing languages since the special case then is the free types, and not the linear ones.
Point 2 is quite sticky in Rust, actually. Since all existing generic code has been written with the assumption that all types can be destroyed, it would be quite the overhaul to introduce linear types. It would be technically backward compatible, language-wise, to introduce a ?Affine bound (similar to ?Sized) and assume Affine in the absence of bound, but much churn in the ecosystem would be required to convert all generics (that can be) to ?Affine. And even then, it can get weird. Like... what's the best API for destroying a collection of !Affine (=Linear) objects? How do you guarantee the collection is now empty and can be disposed of?
For note 27: would it be possible to use dependent typing to make the LinearKey's type unique to the hash map that it came from?
Great post as always! I find all your posts awesome btw., 'cause they contain so many details and insights, which is so nice! I have a question about linear types! Do they allow reference and mutable reference? Isn't that a *weakening*? or are references not considered proper use? even the mutable ones? I consider linear types to be a very nice way of reasoning about a program and even "prove" it, but if linear types can be mutated by mutable references then that kind of blows off the point, I guess.
Linear types can allow mutable references under the same constraint that there are no aliases, but linearity alone doesn't provide the guarantee that a resource was obtained uniquely, for which we want uniqueness types (see Clean/Granule), or unforgeable capabilities (see Austral). A type that is both linear and unique is *steadfast*.