[rust-dev] A better type system

Matthieu Monrocq matthieu.monrocq at gmail.com
Sun Jun 1 04:36:05 PDT 2014


FYI: I did a RFC for separating mut and "only" some times ago:
https://github.com/rust-lang/rfcs/pull/78#

I invite the interested readers to check it out and read the comments
(notably those by thestinger, aka Daniel Micay on this list).

For now, my understanding was that proposals on the topic were suspended
until the dev team manages to clear its plate of several big projects (such
as DST), especially as thestinger had a proposal to change the way lambda
captures are modeled so it no longer requires a "&uniq" (only accessible to
the compiler).

-- Matthieu



On Sun, Jun 1, 2014 at 2:32 AM, Patrick Walton <pwalton at mozilla.com> wrote:

> Yes, you could eliminate (c) by prohibiting taking references to the
> inside of sum types (really, any existential type). This is what Cyclone
> did. For (e) I'm thinking of sum types in which the two variants have
> different sizes (although maybe that doesn't work).
>
> We'd basically have to bring back the old &mut as a separate type of
> pointer to make it work. Note that Niko was considering a system like this
> in older blog posts pre-INHTWAMA. (Search for "restrict pointers" on his
> blog.)
>
> Patrick
>
> On May 31, 2014 5:26:39 PM PDT, Cameron Zwarich <zwarich at mozilla.com>
> wrote:
>>
>> FWIW, I think you could eliminate (c) by prohibiting mutation of sum
>> types. What case are you thinking of for (e)?
>>
>> For (d), this would probably have to be distinguished from the current
>> &mut somehow, to allow for truly unique access paths to sum types or shared
>> data, so you could preserve any aliasing optimizations for the current
>> &mut. Of course, more functions might take the less restrictive version,
>> eliminating the optimization that way.
>>
>> Not that I think that this is a great idea; I’m just wondering whether
>> there are any caveats that have escaped my mental model of the borrow
>> checker.
>>
>> Cameron
>>
>> On May 31, 2014, at 5:01 PM, Patrick Walton <pwalton at mozilla.com> wrote:
>>
>> I assume what you're trying to say is that we should allow multiple
>> mutable references to pointer-free data. (Note that, as Huon pointed out,
>> this is not the same thing as the Copy bound.)
>>
>> That is potentially plausible, but (a) it adds more complexity to the
>> borrow checker; (b) it's a fairly narrow use case, since it'd only be safe
>> for pointer-free data; (c) it admits casts like 3u8 -> bool, casts to
>> out-of-range enum values, denormal floats, and the like, all of which would
>> have various annoying consequences; (d) it complicates or defeats
>> optimizations based on pointer aliasing of &mut; (e) it allows
>> uninitialized data to be read, introducing undefined behavior into the
>> language. I don't think it's worth it.
>>
>> Patrick
>>
>> On May 31, 2014 4:42:10 PM PDT, Tommi <rusty.gates at icloud.com> wrote:
>>>
>>> On 2014-06-01, at 1:02, Patrick Walton <pcwalton at mozilla.com> wrote:
>>>
>>>    fn my_transmute<T:Clone,U>(value: T, other: U) -> U {
>>>        let mut x = Left(other);
>>>        let y = match x {
>>>            Left(ref mut y) => y,
>>>            Right(_) => fail!()
>>>        };
>>>        *x = Right(value);
>>>        (*y).clone()
>>>    }
>>>
>>>
>>> If `U` implements `Copy`, then I don't see a (memory-safety) issue here.
>>> And if `U` doesn't implement `Copy`, then it's same situation as it was in
>>> the earlier example given by Matthieu, where there was an assignment to an
>>> `Option<Box<str>>` variable while a different reference pointing to that
>>> variable existed. The compiler shouldn't allow that assignment just as in
>>> your example the compiler shouldn't allow the assignment `x =
>>> Right(value);` (after a separate reference pointing to the contents of `x`
>>> has been created) if `U` is not a `Copy` type.
>>>
>>> But, like I said in an earlier post, even though I don't see this
>>> (transmuting a `Copy` type in safe code) as a memory-safety issue, it is a
>>> code correctness issue. So it's a compromise between preventing logic bugs
>>> (in safe code) and the convenience of more liberal mutation.
>>>
>>>
>> --
>> Sent from my Android phone with K-9 Mail. Please excuse my brevity.
>> _______________________________________________
>> Rust-dev mailing list
>> Rust-dev at mozilla.org
>> https://mail.mozilla.org/listinfo/rust-dev
>>
>>
>>
> --
> Sent from my Android phone with K-9 Mail. Please excuse my brevity.
>
> _______________________________________________
> Rust-dev mailing list
> Rust-dev at mozilla.org
> https://mail.mozilla.org/listinfo/rust-dev
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.mozilla.org/pipermail/rust-dev/attachments/20140601/b0a4f226/attachment.html>


More information about the Rust-dev mailing list