My favorite Rust function

Reminds me of Coq's definition of `False`:

`Inductive False := .`

i.e., `False` has no constructors and hence is an empty type.

Anyway, this means that for any type `A`, you can construct a function of type `False -> A` because you just do this:

`fun (x : False) => match x with end.`

Since `False` has no constructors, a match statement on a value of type `False` has no cases to match on, and you're done. (Coq's type system requires a case for each constructor of the type of the thing being matched on.) This is why, if you assume something that is false, you can prove anything. :)

What do you mean by "will not work"? Will it not compile? And how do we write that with add1 taking ownership vs. not?

Do variables go out of scope after last use or when the function exits? I could see the former evolving into the language if it’s not already the default behavior.

In which case there’s only one situation where I could see this useful, and that’s when you are building a large object to replace an old one.

The semantics of

    foo = buildGiantBoject();

In most languages is that foo exists until reassigned. When the object represents a nontrivial amount of memory, and you don’t have fallback behavior that keeps the old data, then you might see something like

    drop(foo);
    foo = buildGiantBoject();

Most of the rest of the time it’s not worth the hassle.

Interestingly, the type of `x` actually does matter here in Rust! For most types, yes, passing something by value into a function will cause the memory to be "moved", which means that reusing `x` will be a compiler error. That being said, you can also either pass a shared reference (i.e. `&x`), which will allow you to access the data in Rust (provided you don't move anything out from it or mutate it, which would cause a compiler error) or a mutable reference (i.e. `&mut x`), which will allow you to access or mutate the data in `x` but not take ownership of it (unless it's replaced with something else of the same type).

However, a few types, including integers, but also things like booleans and chars, implement a trait (which for the purposes of this discussion is like an interface, if you're not familiar with traits) called Copy that means that they should be implicitly copied rather than moved. This means that in the specific example you gave above, there would not be any error, since `x` would be copied implicitly. You can also implement Copy on your own types, but this is generally only supposed to be done on things that are relatively small due to the performance overheard of large copies. Instead, for larger types, you can implement Clone, which gives a `.clone` method that lets you explicitly copy the type while still having moves rather than copies be the default. Notably, the Copy trait can only be implemented on types that already implement Clone, so anything that is implicitly copied be can also be explicitly copied as well

You'll get a compile-time error explaining the situation, yes, including documentation links and possible fixes. The differences between the versions are minimal.

    fn add1(x: Thing) -> Thing {
      x + 1
    }

    fn add2(x: &Thing) -> Thing {
      x + 2
    }

This works on the assumption that whatever "+ 1" really means doesn't itself need ownership of x, e.g. because it mutates it. If it does, then you'll get an error. Or you could do this:

    fn add3(x: &mut Thing) {
      x.add(3)
    }

Which, presumably, modifies x instead of returning a copy. It's your job to make sure it makes sense to do that, but Rust has another trick in its pockets:

    let y = add1(x);  // Works; takes ownership.
    let z = add2(&y);  // Works, and doesn't take ownership.
    let zz = add2(&y);  // So you can do it twice. (Y tho?)
    let h = add3(&y);  // Compile-time error!
    let hh = add3(&mut y);  // Works. You need to specify that you're fine with y being mutated.