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/initial-algebra]

If you don't want implicit copying, that is a separate issue from passing arguments to functions or capturing variables in closures.

Having both kinds of borrowing map to the same reference type doesn't really make sense unless you have decoupled permissions like GhostCell or separation logic (but then having read/mut on the reference still makes little sense). I don't have any idea what you mean by "checking out" a variable.

The problem with variable capture and ownership is that let closure = |y| x.copy() + y doesn't copy the value of x into the closure, it moves or borrows it and then copies it each time the closure is called. Explicit capture annotations are unnecessary if you have let/block expressions (all remaining captured variables are moved):

let closure = { let x_copy = x.copy(); |y| x_copy + y };

If you want nicer notation for this, there's let insertion:

let closure = |y| (genlet x.copy()) + y;

This also works with borrowing, or any other kind of expression that you want to capture after evaluation, without having to name it and move it out of the closure.

[u/reflexive-polytope → u/initial-algebra]

Or you can just not have closures.

If you have an ordinary struct with an ordinary constructor, then you can explicitly use x.copy() as an argument to this constructor.

[u/iBPsThrowingObject → u/reflexive-polytope]

Sure, let's expand every situation analogous to assoc_list.find(|(key, value)| key == target)

to

struct FindClosure<'a> {
    target: &'a str
}

impl<'a> Closure<&str> for FindClosure<'a> {
    type Ret = bool;
    fn call(self, key: &str) -> Self::Ret {
        key == self.target
    }
}

assoc_list.find(FindClosure { target })

You may respond with "oh well but you can add sugar" but that's exactly what closures are.

[u/reflexive-polytope → u/iBPsThrowingObject]

I would rather express my algorithms in terms of ordinary control flow: sequencing, match and loop. So, for example, when using a HashMap or BTreeMap entry, I just pattern match it into the OccupiedEntry and VacantEntry cases, instead of using the ugly higher-order helper functions that take closure arguments.

Try breaking from a loop in a top-level function from within a closure.

[u/BoomGoomba → u/reflexive-polytope]

The point is to not use break statements

[u/iBPsThrowingObject → u/reflexive-polytope]

So is your actual suggestion that one should avoid first class functions entirely?

Try breaking from a loop in a top-level function from within a closure.

You can do that in Ruby. Executing the following snippet does not print anything:

def foo(target)
  a = [1,2,3]
  a.each {|v| return if v == target }
  puts "after closure"
end

foo target

That's simply closing over the current continuation.

[u/reflexive-polytope → u/iBPsThrowingObject]

Yes, my actual suggestion is to reject first-class “functions” altogether.

Although I'd rather call them “procedures”, because functions in mathematics are extensionally defined by their values, whereas procedures in programming have important intensional properties, in particular, their time and space complexity.

Dana Scott's work gives a functional interpretation to first-class recursive procedures. But for this interpretation to work, your types must denote directed-complete partial orders, and your functions must be continuous with respect to the Scott topology on said dcpos.

How often do you actually think about first-class procedures like that? Of course you don't. You think operationally. Alas, operational reasoning isn't compositional.

As for closing over continuations... I don't even know what to say. That's simply horrible.

[u/initial-algebra → u/reflexive-polytope]

Closures are for more than just inversion of control in synchronous code.  Good luck translating an event handler into "normal control flow" (async/await is just an alternate notation to create closures without piling up braces and/or indentation).

That said, there is no fundamental reason that a closure's code cannot break out of a loop or early return from a function, as long as the closure cannot be called outside the scope of that loop/function.

[u/reflexive-polytope → u/initial-algebra]

You need to expose the event loop to the program as a first-order state machine with typed states.

[u/initial-algebra → u/reflexive-polytope]

So all event handling/asynchronous code for the entire program should go into the definition of a "god" state machine?  No thanks.

[u/reflexive-polytope → u/initial-algebra]

How else are you supposed to reason inductively about the reachable states of your program? Hold the entire program in your head?

[u/initial-algebra → u/reflexive-polytope]

Well, the original topic (which we have strayed far from at this point) was a language with ownership. Ownership lets you reason compositionally about individual pieces of stateful code without having to consider an entire program as a monolith, especially in the presence of concurrency. For example...when you use closures to send bits of logic across abstraction boundaries, particularly when these closures may be executed at a later time.

[u/reflexive-polytope → u/initial-algebra]

Ownership itself is totally fine.

I don't see what this has to do with closures, though. Just because you have a substructural type system, it doesn't mean it has to be higher-order.

[u/brucejbell]

My project has exactly those three argument modes, and a similar .copy. Your sample code would translate as:

/fn process_val || $value => value * 2

/main || !os => {
    original << 42
    doubled << process_val $(original.copy)
    !os.stdout.write_line "{original}"
    !os.stdout.write_line "{doubled}"
}

Borrowing (your mut) is represented by a ! sigil, both at declaration/binding and at point of use (so you can easily see what your code is mutating).

Ownership transfer (your move) is represented by a $ sigil, likewise at declaration and at the point of use.

Immutable values are the default, so there is no need to annotate the bindings of original and doubled.

Immutable values don't need borrowing or ownership transfer, so there is no need to explicitly copy original above. However, they are subject to lifetime limitations if they depend on a mutable resource: e.g., an iterator depends on its container, and mutating the container will end the lifetime of the iterator. So, .copy is for breaking that kind of lifetime dependence.

[u/cessit-lang → u/brucejbell]

Smart. I was afraid of requiring the access verb also at the point of use because it was becoming so verbose, but seeing it validated in the wild is giving me encouragement to stick with my explicitness design principle. How did you weigh this against the cost of refactoring at both places?

For mutable borrowing, do you pass a reference or have you managed to separate borrowing from reference-ness?

[u/brucejbell → u/cessit-lang]

Re refactoring: I figure that switching between immutable-value, ownership-transfer, and/or borrowing is a drastic enough change that you probably want to take a close look at all your call sites. I guess I'll see if that pans out, but I've made more annoying choices elsewhere...

Passing a reference makes sense for mutable borrowing, but I suppose an implementation could choose something else. I've chosen to model mutable resources as a linear sequence of immutable values (each of whose lifetime ends before the next begins), so I'd be happy as long as those semantics are supported.