I'm not super well versed on this stuff, but aren't affine types strictly superior? Though I suppose linear types might be better for tracking system resources?
All of this is performed by destructors/GC cleanup/Drop in most languages.
> That's why even in safe Rust code, it's possible to leak memory
It's possible to leak memory through circular references and lazy evaluation in all languages AFAIK.
> e.g. shut down without calling the "switch off the radiation emitter" destructor on a medical device.
Unsafe unwinding is possible in any language, including one with linear types. If the runtime crashes, there's nothing to guarantee their one-time use.
Most GC languages don't guarantee that finalisers will run on shutdown, and no languages I'm aware of guarantee that destructors will run. For really safety critical applications it's not enough that it works fine most of the time; it needs to provide an iron-clad guarantee (as e.g. Ada with Spark can provide for many things). When writing a library it's not possible to guarantee the user will use it correctly when the compiler isn't able to enforce this.
>It's possible to leak memory through circular references and lazy evaluation in all languages AFAIK.
In a garbage-collected language, circular references alone aren't enough to cause memory leaks, as if the circle is not referenced transitively from the root object then it will still be collected.
>Unsafe unwinding is possible in any language, including one with linear types. If the runtime crashes, there's nothing to guarantee their one-time use.
That's true and unfortunate. But linear types at least guarantee that with orderly shutdown, every destructor will be called correctly.
In languages like Java, C#, F#, it is quite easy to have a lint check that gives a compiler error when an IAutoCloseable or IDisposable isn't used with a try/using block, just like RAII, with a bit of static analysis help.
A new without delete, not only causes a memory leak, it also leaks whatever else could be released by the destructor.
Same applies to Rust when heap memory gets forgotten.
Could you explain a bit more about what you mean here? To me, RAII is about how the constructor is written, and stack allocation/global memory segments are about where the object is created. I don't see any connection between the two.
For example, if I have a class with a custom allocator that allocates from its own arena, I can still do RAII on the members of objects of that class... can't I?
As an example (ignore possible compile errors),
// in mylib.h
namespace mylib {
template<class allocator = default_arena>
class ArenaString final {
public:
ArenaString();
~ArenaString();
// several String related methods
private:
ArenaAllocator<allocator> stringData;
};
// several utility functions
ArenaString* StringFactory() {
return new ArenaString();
}
}
// now on main.cpp
#include "mylib.h"
void myLeakyFunction()
{
auto strPtr = mylib::StringFactory();
// do something with strPtr
//oops, strPtr is now gone and ArenaString::~ArenaString() won't get called
}
But then the question about class instances surviving the region as empty shells with a corrupt state in their stringData member data arises.
While this example is made on purpose to illustrate my point, on big code bases (specially with libraries that one doesn't have any kind of control) it can lead to bad code that prevents RAII patterns to work as expected.
Code that most developers on the team won't even realize it is there and probably will spend hours trying to find out what is wrong with the memory management.
The only thing I'm left confused about is "global memory segments". How does that fit in? If it's a global it's never destroyed, so you don't have to worry about it? Or did you mean something else?
Affine types are less foreign to most developers. The safe fragment of Rust’s ownership model is an example of an affine type system...and that’s already a bit of a lift for folks new to the borrow checker. Affine types are harder to reason about than linear types, but still much easier to reason about than the Normal [1] (in the proper noun sense) types used in most PLs.