What can Rust's type/lifetime system do that Val can't?

[andrewjw1995]

I've always been surprised by the common practice in Rust of giving lifetimes a single-letter name. Basically every example of Rust that contains lifetimes calls them 'a, 'b, 'c etc. The fact that we can't provide meaningful names for them seems like a code smell, so if Val can solve the same problems without needing lifetime annotations, then I am definitely in favour of eliminating them!

I've been reading through the wiki and the discussions here, and I still don't fully understand the language. My understanding so far is that references are second-class citizens in Val. You can't directly create one, but you can use parameter intents and remotes, which result in a reference behind the scenes. What I don't understand is how Val can distinguish between something being passed as 'inout' because you want to modify it, and something being passed as 'inout' because you want to alias it.

For example, suppose you have a 'deserialize' method which creates a 'Message' from an array of bytes. For performance reasons, the message content points to the original array instead of copying it into a new one. This method also utilizes caching, so it needs the cache to be passed in as a mutable parameter. In Rust, I could have something like the following:

fn deserialize<'a, 'b>(frame: &'a mut [i8], cache: &'b mut Cache) -> Message<'a> {
    // ...
}

Please excuse any syntax errors, I'm a C# developer but I hope the example demonstrates the point

The lifetime annotations make it very clear that I am returning something which aliases the content, not the cache. Rust understands that after this function has been called, the contents are aliased by the returned message but it's safe to use the cache in another call. Is it possible to achieve the same thing in Val?

[kyouko-taiga]

I've always been surprised by the common practice in Rust of giving lifetimes a single-letter name

To be fair, you can use any name you want. The single-letter practice is just a convention, like using T for most generic type parameters.

What I don't understand is how Val can distinguish between something being passed as 'inout' because you want to modify it, and something being passed as 'inout' because you want to alias it.

You never use inout to alias anything. In fact, you never use any passing convention to talk about aliasing. Val is all about independent values and lets you write programs as though references didn't exist.

For example, suppose you have a 'deserialize' method which creates a 'Message' from an array of bytes. [...]

You can't return a reference to a part of an object. However, you can project it. This mechanism plays a big role in the elimination of lifetime annotations because a projected value can never escape. The signature of deserialize would probably look something like this in Val:

subscript deserialize(frame: Array<UInt8>, cache: inout Cache): Message { ... }

Note: I don't think frame had to be mutable in your original example, so I made it immutable here.

The lifetime annotations make it very clear that I am returning something which aliases the content, not the cache. [...]

Because we're only projecting a Message, we're allowed to store remote parts coming from frame and cache. However, there's no way in Val to say that you definitely won't use parts from cache in the projection or that you won't touch it after the projection ends. Therefore, unlike in Rust, you won't be able to use it while the projection is live. That's the kind of hit to expressiveness we're willing to take in exchange for a simpler type system.

It is possible to work around the type checker, but not in the safe subset of the language.

[andrewjw1995]

You never use inout to alias anything. In fact, you never use any passing convention to talk about aliasing.

Oh, it looks like I've misunderstood how subscripts work! How does Val distinguish between parameters that are just used for the duration of the method, and parameters which are used in the projected value? E.g. if I'm making a dictionary-like type, with a method to get an item:

subscript try_get_item(key: TKey): TItem? { ... }

Does this mean that the key is considered 'aliased' by the returned item?

[kyouko-taiga]

Does this mean that the key is considered 'aliased' by the returned item?

Yes, although I would prefer the term borrowed.

To understand why, we have to remember the semantics of a subscript. Roughly speaking, these two definitions are equivalent:

subscript row_s(_ m: Int[3][3], _ r: Int): Int[3] {
  print("will project row ${r}")
  yield m[r]
  print("did project row ${r}")
}

fun row_f<T>(_ m: Int[3][3], _ r: Int, _ action: (Int[3]) -> T) -> T {
  print("will project row ${r}")
  let result = action(m[r])
  print("did project row ${r}")
  return result
}

As you can see, nothing prevents r from being used after yield (or after the call to action). So it still has to be considered borrowed until the projection ends and the subscript (or its roughly equivalent function) returns.

You could copy the key before calling row_s (or your try_get_item) so that the subscript would get an independent value.

public fun foo(_ m: Int[3][3]) {
  var k = 0
  let r0 = row_s[m, k.copy()]
  &k += 1 // OK
  let r1 = row_s[m, k]
  ...
}

Maybe in the future we could imagine some sort of annotation that tells Val that a particular argument can't be used in the slide of the subscript (i.e., the part after yield). But that isn't on the menu yet.

[T4r4sB]

I dont know, should I open a new topic, because my question relates to this topic.
As I understood, structures can not contain references (except lambdas), and lambdas can not be returned from functions?
Also subscript works like a C++-template, e.g. instantiates in each place where used?

What if I has an outer module with subscript:

subscript one_of(_ x: inout Int, _ y: inout Int): Int {
  &x
}

And has a main module with code:

fun add(_ x: inout Int, _ a: Int) {
  x += a;
}

public fun main() {
  var x  = 1;
  var y = 2;
  add(&one_of[&x, &y], y);
}

Should it compile? Can compiler recognize that result one_of in not linked with y?
What if I change a body of one_of in other module and return y instead of x? Will compiler re-analyze a code of main module?

[kyouko-taiga]

A couple of corrections:

• Lambdas can be returned from functions if they don't capture let or inout bindings.
• Subscripts are nothing like C++ templates. They are constructs that are used to project values rather than returning them. A projection remains notionally part of its whole throughout its lifetime.

No instantiation occurs when you use a subscript. If it's in another module, it's been compiled and verified, once and for all (putting possible monomorphization aside).

Your code won't compile because the compiler will conclude that y is being simultaneously accessed mutably and immutably. It does not matter what the contents of your subscript is.

[T4r4sB]

So when I write a subsrcipt with header

subscript one_of(_ x: inout Int, _ y: inout Int): Int {
// body 
}

compiler thinks, that result borrows both of input arguments, isnt'it?

So, if I understoop the point, this example can not be written in Val?

https://play.rust-lang.org/?version=stable&mode=debug&edition=2021&gist=75dad2f92088825524cb596ca1c3e61a

[T4r4sB]

More realistic example: https://play.rust-lang.org/?version=stable&mode=debug&edition=2021&gist=cfb1895da4664b73558efd75c6d5b42d

[kyouko-taiga]

Indeed, they can't. Your examples are morally equivalent to @andrewjw1995's.