Ownership and borrowing

RCE has no manual free, and a value cannot be used after it is released. Two ideas, also found in Rust, make this work: every value has one owner, and other code can borrow a value for a short time. A value is released when the block that owns it ends. RCE's borrows are more restricted than Rust's, which makes them simpler to check.

Moving

Small fixed-size values such as integers, bool and f64 are copied when you pass them. Values that own memory, such as text, List and Map, are moved: passing one to a function hands it over, and the old name can no longer be used.

fn take(s: text) -> u64 = s.len_chars() as u64

fn twice(s: text) -> u64
    let a = take(s)
    return a + take(s)

$ rce check use_after_move.rce
requires change use_after_move.rce: line 5: W-OWN-1 `s` is used after it was moved
exit status: 1

The first call to take moved s, so the second call requires change. If you really need two independent values, copy(s) makes a full copy.

Borrowing

fn length(s: &text) -> u64 = s.len_chars() as u64

fn push_all(dst: &mut List[i64], src: &[i64])
    for x in src
        dst.append(x)

fn demo() -> u64
    let name = "Ada"
    let n = length(&name)
    let again = length(&name)
    var a: List[i64] = [1, 2, 3]
    let b: List[i64] = [4, 5]
    push_all(&mut a, &b)
    let c = copy(a)
    return n + again + (c.len() as u64) + (a.len() as u64)

check demo() == 16

&name lends name for reading. The owner keeps it, so length can be called twice.
&mut a lends a for changing. push_all appends to the caller's list.
copy(a) makes a separate list.

The one rule about borrows

While something is borrowed for changing, nothing else may look at it in the same call:

fn both(_a: &mut List[i64], _b: &List[i64])
    pass

fn bad()
    var xs: List[i64] = [1]
    both(&mut xs, &xs)

$ rce check mut_alias.rce
requires change mut_alias.rce: line 6: W-OWN-2 `xs` is borrowed mutably and again in one call
exit status: 1

Different fields are different places, so two(&mut f.a, &mut f.b) lends two separate things and is fine; two(&mut f.a, &mut f) lends f.a twice and requires change. Two elements of one list, xs[0] and xs[1], count as the same place, because the checker does not compare indexes.

A let can hold a borrow too. let a = &mut n lasts until the last statement of its block that uses a, and until then nothing else may use n; a change made through a is a change to n.

Why RCE borrows need no lifetimes

In RCE a borrow lives only as long as the call or statement that made it, or, for a borrow held by let, until the last statement of its block that uses it. A borrow cannot be stored in a field, a list, an event or a state, and in general cannot be returned. (A function may return a borrow of one of its own parameters, such as a slice of a list it was given.) Because borrows never outlive the block that created them, the checker does not need lifetime annotations, and the check is a local pass through each function.

The specification calls these second-class borrows, a design also used by Swift's inout parameters and by the Hylo language.

What you learned

Copy types are copied; owning types are moved, and a moved name is dead.
&x lends for reading, &mut x for writing, copy(x) duplicates.
A mutable borrow excludes every other use for its duration.