add some of my talks

[web.git] / personal / _posts / 2018-01-31-sharing-for-a-lifetime.md

diff --git a/personal/_posts/2018-01-31-sharing-for-a-lifetime.md b/personal/_posts/2018-01-31-sharing-for-a-lifetime.md
index 8dd10daab96c7b8969e30050bf7bdf54a99c6742..e3bcce54c632194b84fef35b087a89904c09d723 100644 (file)
--- a/personal/_posts/2018-01-31-sharing-for-a-lifetime.md
+++ b/personal/_posts/2018-01-31-sharing-for-a-lifetime.md
@@ -4,11 +4,11 @@ categories: research rust
 forum: https://internals.rust-lang.org/t/sharing-for-a-lifetime/6675
 ---
 
 forum: https://internals.rust-lang.org/t/sharing-for-a-lifetime/6675
 ---
 

-This post is about an aspect of the [RustBelt paper]({{ site.baseurl }}{% post_url 2017-07-08-rustbelt %}).
+This post is about an aspect of the [RustBelt paper]({% post_url 2017-07-08-rustbelt %}).

 Concretely, I'd like to share some of our thoughts on the nature of types and shared references.
 Let's see how well this goes. :)
 
 Concretely, I'd like to share some of our thoughts on the nature of types and shared references.
 Let's see how well this goes. :)
 

-Shared references are an extremely powerful mechanism in the Rust type system, and we've had quite some trouble finding a good way of handling them in our [formal model]({{ site.baseurl }}{% post_url 2015-10-12-formalizing-rust %}).
+Shared references are an extremely powerful mechanism in the Rust type system, and we've had quite some trouble finding a good way of handling them in our [formal model]({% post_url 2015-10-12-formalizing-rust %}).

 In this post, I will present the model that we came up with.
 <!-- MORE -->
 Let's get started by discussing what a "model" of a type looks like, and what's so hard about handling shared references.
 In this post, I will present the model that we came up with.
 <!-- MORE -->
 Let's get started by discussing what a "model" of a type looks like, and what's so hard about handling shared references.


@@ -21,7 +21,7 @@ To see how, I will briefly assume that Rust does *not* permit interior mutabilit
 
 ### What's in a Type?
 
 
 ### What's in a Type?
 

-I've already [written]({{ site.baseurl }}{% post_url 2015-10-12-formalizing-rust %}) [about]({{ site.baseurl }}{% post_url 2016-01-09-the-scope-of-unsafe %}) the idea of "semantic types", which essentially boils down to the concept that types can impose *additional invariants* on their fields, like `self.cap >= self.len` (for `Vec`) or `!is_zero(self.0)` (for `NonZero`).
+I've already [written]({% post_url 2015-10-12-formalizing-rust %}) [about]({% post_url 2016-01-09-the-scope-of-unsafe %}) the idea of "semantic types", which essentially boils down to the concept that types can impose *additional invariants* on their fields, like `self.cap >= self.len` (for `Vec`) or `!is_zero(self.0)` (for `NonZero`).

 So, whenever I say "(semantic) type", I really mean "a type's (syntactic) definition (aka the data layout) **and** the additional invariants that the module imposes on this type".
 Two types may be syntactically equal but have different invariants, and then clearly casting from one to the other would be horribly unsafe -- so, these would be completely different types despite their syntactic similarity.
 What really matters for a type is the answer to the question: *Given some sequence of bytes, is this sequence a valid inhabitant of the type?*[^1]
 So, whenever I say "(semantic) type", I really mean "a type's (syntactic) definition (aka the data layout) **and** the additional invariants that the module imposes on this type".
 Two types may be syntactically equal but have different invariants, and then clearly casting from one to the other would be horribly unsafe -- so, these would be completely different types despite their syntactic similarity.
 What really matters for a type is the answer to the question: *Given some sequence of bytes, is this sequence a valid inhabitant of the type?*[^1]


@@ -51,7 +51,7 @@ Overall, we conclude that we did not violate any of the invariants imposed on `x
 ## Interior Mutability
 
 Interior mutability however breaks this model of `&'a T`:  We just cannot declare that the pointed-to memory is read-only in general.
 ## Interior Mutability
 
 Interior mutability however breaks this model of `&'a T`:  We just cannot declare that the pointed-to memory is read-only in general.

-If we did, [`Cell::set`](https://doc.rust-lang.org/beta/std/cell/struct.Cell.html#method.set) and many more operations would be blatantly unsafe.
+If we did, [`Cell::set`](https://doc.rust-lang.org/stable/std/cell/struct.Cell.html#method.set) and many more operations would be blatantly unsafe.

 Indeed this is the reason shared references are not called "immutable references" even though they are generally considered the dual of mutable references.
 (My personal thinking is that mutable references should really be called "unique references" to instill the point that the distinction between the two is about uniqueness, not about mutability.  Oh well.)
 
 Indeed this is the reason shared references are not called "immutable references" even though they are generally considered the dual of mutable references.
 (My personal thinking is that mutable references should really be called "unique references" to instill the point that the distinction between the two is about uniqueness, not about mutability.  Oh well.)
 


@@ -135,7 +135,7 @@ This is not so say that the last word on interior mutability has been spoken; th
 
 Either way, this model has certainly helped me not only in the formal work on RustBelt, but also in thinking about the Rust type system itself.
 For example, I briefly wondered why `Cell` is not covariant.
 
 Either way, this model has certainly helped me not only in the formal work on RustBelt, but also in thinking about the Rust type system itself.
 For example, I briefly wondered why `Cell` is not covariant.

-Indeed, if `U <: T`, then it is perfectly safe to turn a `Cell<T>` into a `Cell<U>` -- that is to say, whenever some sequence of bytes is valid at `Cell<T>`, it is also valid at `Cell<U>`.
+Indeed, if `T <: U`, then it is perfectly safe to turn a `Cell<T>` into a `Cell<U>` -- that is to say, whenever some sequence of bytes is valid at `Cell<T>`, it is also valid at `Cell<U>`.

 (In fact, the owned invariant for `Cell<T>` is *exactly the same* as the one for `T`!)
 That's precisely what we need for covariance, right?
 Well, not exactly -- because our types have two invariants, we also have to require that whenever a pointer is a shared `Cell<T>`, it is a shared `Cell<U>`, and that is decisively *not* true!
 (In fact, the owned invariant for `Cell<T>` is *exactly the same* as the one for `T`!)
 That's precisely what we need for covariance, right?
 Well, not exactly -- because our types have two invariants, we also have to require that whenever a pointer is a shared `Cell<T>`, it is a shared `Cell<U>`, and that is decisively *not* true!


@@ -156,3 +156,5 @@ I honestly don't know, but I had to think of this a while back when I read [this
 
 If you have any comments or thoughts on this, please join the [discussion in the Rust forums](https://internals.rust-lang.org/t/sharing-for-a-lifetime/6675)!
 I'd also be interested in feedback on how understandable this post is; this is my first attempt at translating research results into a blog post.
 
 If you have any comments or thoughts on this, please join the [discussion in the Rust forums](https://internals.rust-lang.org/t/sharing-for-a-lifetime/6675)!
 I'd also be interested in feedback on how understandable this post is; this is my first attempt at translating research results into a blog post.

+
+#### Footnotes