Understanding Subscripts

[AbhinavK00]

Hi, I'm having a hard time understanding subscripts and their use. Currently what I understand I that val functions can't/don't return references and only return values, subscripts are there to fill the use case of functions that return references. I assume that subscripts do it in a way that is safe and does not require us to use lifetime annotations like rust. But that's just me and I would be grateful if someone can point if I understand and provide more insight into subscripts.

[kyouko-taiga]

Hi @AbhinavK00!

Your understanding is relatively accurate.

In general, I think it's best to just forget about references when reasoning about Val. The reason is that, although projections (i.e., the result of a subscript) fill a similar role, they do not represent a distinct kind of values, with a distinct type. For example, in C++, a reference to int has type int& or int const&. In Rust, a reference to i64 has type &i64 or &mut i64. In Val, a projection of Int has type Int.

So if it's technically correct to say that "Val functions can't return references", it's important to note that it simply derives from the fact that references don't exist in Val.

Unlike functions, subscripts don't return values, they project them until they are no longer used by the caller. That's an important difference. Projecting doesn't make values escape (we'll come back to that); all operations can happen in-place and nothing has to "move". For example, when we write x[2], the subscript doesn't return anything, it simply projects access to the third element of the array:

fun f(_ i: Int) { print(i) }

public fun main() {
  let x = Array([0, 1, 2, 3])
  let y = x[2]
  f(x[2])
  f(0)
}

Notice that f(_:) accepts a value of type Int, meaning that both f(x[2]) and f(0) are legal. Yet, f(_:) is not a generic function.

Subscripts are not the only way to project a value. Passing arguments to let/inout/set parameters, or simply binding local variables may create projections as well. For example, in f(_:) above, i is a projection too.

References à la C++/Rust require lifetime annotations because the type &i64 says nothing about the lifetime of the referred integer. So one write &'a i64 to (roughly) mean "a reference to i64 with lifetime a", thereby encoding the lifetime of the referred object in the type system. In turn, it allows Rust's type system to guarantee that the reference is never used beyond that lifetime. In Val, Int is just Int, projected or not, so the type system needs to rely on a different concept to guarantee safety.

That's where escape comes back. Val's type system keeps track of the values that are allowed to escape and those that aren't, based on their ability to move and their outstanding uses at a given program point.

For example, consider the following program:

fun forty_two() -> Int {
  let x = 42;
  let y = x
  print(y)
  return x
}

If the caller of forty_two uses the return value, that use will be outside the lifetime of x, the initial binding of the returned value. So we say that x escapes when it is returned.

Escaping a value requires it to be not bound by any other binding still in use and that its type be Sinkable. In forty_two above, both of these conditions are met because Int is Sinkable and neither x nor y is in use after the return statement. In contrast, the one of the conditions is not met in the following program:

fun consume(_ x: sink Int) {}

public fun main() {
  let x = Array([0, 1, 2, 3])
  let y = x[2]
  consume(y) // error: `y` cannot escape while `x` is let-bound
  print(x)
}

The call to consume(_:) is attempting to make y escape. Int is Sinkable but the value of y is bound (transitively) by x which is still in use at this point. So the call is illegal.

[AbhinavK00]

Thanks for the reply!!

[neuring]

What is the general desugaring of a subscript invocation (maybe in terms of Rust or C++)? I feel like this could help quite a lot in understanding the semantics. At least for me terms like projection, while kinda conveying the general idea, can be quite vague and don't describe what my hardware is doing behind the abstraction layer of the language.
Are you aware of any other languages that use these kinds of subscripts or is it a novel invention in Val?

Finally, in your explanation you mention the Sinkable trait.
What does it imply exactly? My thinking is that it is a marker trait for types that can be destructively moved. If that is the case what types in Val are not Sinkable?

[kyouko-taiga]

What is the general desugaring of a subscript invocation (maybe in terms of Rust or C++)?

One way to think about subscripts is to imagine the portion of the code using the projected value being wrapped inside a closure and executed by the yield statement of the subscript. For example:

type Angle {
  public var radians: Double
  public memberwise init
  public property degrees: Double {
    inout {
      var d = radians * 180.0 / Double.pi
      yield &d
      radians = d * Double.pi / 180.0
    }
  }
}

public fun main() {
  var x = Angle(radians: Double.pi)
  inout y = &x.degrees
  &y += 1
  print(x)
}

In this example, another way to think about this program is to imagine that degrees is a function that accepts a closure representing the use of the projected value:

public fun main() {
  var x = Angle(radians: Double.pi)
  x.with_degrees(fun (y) { &y += 1 })
  print(x)
}

You can write such closure in C++ or Rust.

Are you aware of any other languages that use these kinds of subscripts or is it a novel invention in Val?

Val's projections is a generalization of Swift's subscript. One important improvement brought by Val is that projections can be assigned to local bindings. In Swift, subscripts can only be used as sub-expressions.

My thinking is that it is a marker trait for types that can be destructively moved. If that is the case what types in Val are not Sinkable?

You are right. Sinkable is the trait of (destructively) movable types.

If that is the case what types in Val are not Sinkable?

Like all traits, conformance to Sinkable must be declared explicitly. So a kind of circular answer would be: the types that are not declared Sinkable.

In general, anything containing a remote projection is not Sinkable (e.g., Optional<remote let Int>).

[neuring]

Thank you for the reply, the explanation of subscripts using closures makes a lot of sense.

Regarding non-Sinkable types, Rust has quite a lot of issues with immovable types. For example, their futures can be self referential which break if the such a value is moved bit-wise. This requires type system "hacks" like Pin which can be quite cumbersome to use and can usually only be interacted with in a unsafe manner. Every now and then a discussion about a hypothetical Moveable trait pops up in the Rust community but Rusts backwards compatibility guarantees make it quite difficult to retroactively add such a trait. It sounds like Val might be able to circumvent such issues since it starts out with Sinkable trait from the beginning.
Presumably, once the unsafe part of Val is figured out it might be possible to build types that are self referential internally but still can expose a safe and mostly convenient API to the user without unnecessary allocations.

[dabrahams]

Presumably, once the unsafe part of Val is figured out it might be possible to build types that are self referential internally but still can expose a safe and mostly convenient API to the user without unnecessary allocations.

Yes we believe that Val's design makes that straightforward (with the usual caveats about using unsafe things).