This paper [1710.07047] Safe Pointers in SPARK 2014 states the SPARK's pointers have been created based on Rust's borrow checker and affine types. What are affine types in Rust? Apparently, in an affine type system, a variable can be used at most once, according to this Wikipedia article: Substructural type system - Wikipedia. However, this doesn't seem to be the case in Rust: I can use variables more than once. So, what are affine types in Rust?
That's a fancy name for the combination of Rust's move semantics which ensure that if a type isn't marked as copyable, it can only be moved, not copied.enum
and
Why a "combination" of enum and move semantics? I understand that if a type is not copyable, then it can only be moved or cloned. But what is the relation between this and enums?
I believe that what @kornel was mentioning about enum
s is that there will only ever be one of the possibilities of the enum in a value.
Example:
enum Foo {
A,
B,
C,
}
let a_foo: Foo = get_a_foo();
//We can be assured that `a_foo` is:
// Either A
// OR B
// OR C
// But not more than one at a time
and if you're familiar with it, then it's kind of the opposite to a C/C++ union
Sorry, I think I was mistaken, and the enum
magic isn't required for the affine types.
BTW, here's an article about linear types (must use exactly once) which are a next level up from affine types (use at most once): https://gankro.github.io/blah/linear-rust/
Affine types is another word for move semantics. All Rust types that aren't Copy
(like raw integers and references) are affine.
A side note though, Copy
is implicit while Clone
is not, right?
Clone is explicit in the sense that you need to call "clone" to clone objects that implement the Clone
trait, whereas Copy
is performed automatically (or "implicitly", which I think is a misleading adverb) by the compiler: no need to call functions to copy (copyable) objects.
Anyway, what does this have to do directly with my post?
Well, in a sense, it's this:
Your "Affine Types" is a pretty name for rust's ownership/move semantics as @kornel and @notriddle mentioned, and is about how every variable can only be used once per function, as per rust's rules that specify that variables are de-allocated at the end of every function, therefore they cannot be "used" in the caller more than once in another function. Rust gets around this by using it's infamous borrow checker where it creates a "temporary" reference variable to the original variable so that the underlying T
is not dropped while the &T
is. It all works out
- Linear type - every value must be used exactly once
- affine type - every value must be used once or not at all