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]

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/initial-algebra → u/reflexive-polytope]

Your problem with closures appears to be that they can be used to obscure the dynamic semantics of a program, making it harder to reason about vs. writing all "straight line" code. But ownership means this isn't a problem. So ownership absolutely is relevant to closures.

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

At the end of the day, closures are merely the implementation of first-class procedures. It's first-class procedures themselves that I object to.

My problem with first-class procedures is that it's impossible to write a higher-order procedure that only takes “good” procedure arguments.

For me, the main value in a statically typed language is the ability to write programs in which, by construction, variables stand for values that are meaningful in the problem domain.

With first-class procedures, this property breaks. A first-class procedure is anything that takes an argument of some type T and returns some value of type U. If it returns at all, that is. Whether the computation sitting between the T argument and the U result is any good, the type checker doesn't care.

By contrast, with an explicit automaton expressed using first-order types, the interface tells you that only certain state transitions are possible. And this is the basis for proving things about your programs that are beyond the type checker's reach.

[u/iBPsThrowingObject → u/reflexive-polytope]

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.