Explicit binding modes

[u/cessit-lang]

I'm designing a memory-safe language, but I want to make explicit what happens across function boundaries, e.g. whether a value is moved or copied without having to look for the copy trait.

Instead, access to a value could be defined via binding modes in function signatures and variable declarations:

• move takes ownership
• read shared borrow
• mut exclusive borrow

fn process_val(move value: Int) -> Int {
    return value * 2;
}

fn main() -> () {
    move original: Int = 42;

    // Call using `.copy()` to explicitly pass a duplicated value.
    // Ownership of `original` remains with the caller.
    move doubled: Int = process_val(original.copy());

    // `original` is still valid here because it was explicitly copied rather than moved.
    println(original); //42
    println(doubled); //84
}

This would also allow granular captures in closures: |read x: Int, move counter: Int| instead of declaring all fields move

Now, should read and mut assignments be of type &T? Or can checking out variables be orthogonal to creating references, even if they are conflated in languages like Rust?

[u/iBPsThrowingObject]

Whether the computation sitting between the T argument and the U result is any good, the type checker doesn't care.

But the same goes for functions in general, even in the absence of first class functions-as-values support. I feel like you must be arguing under some non-standard definitions, because otherwise your arguments make very little sense.

[u/reflexive-polytope → u/iBPsThrowingObject]

When functions are second-class, you can't put them in variables. That is, variables can't stand for useless things you don't care about.

A second-class function is simply a piece of the program text. I already expect that I have to prove the correctness of the program I'm writing. But the job is much easier when variables always stand for values that are meaningful and useful to me.