lift operator - sketch

[Chriscbr]

This write-up is inspired by an offline discussion with the compiler team about how to handle the issue of MutArray<T> functionally behaving like Array<T> once it is lifted into inflight, where @ShaiBer had the idea of "what if lift was a keyword?". The idea here is just to explore the concept and see whether that would give us any new expressive capabilities to the language.

To start, suppose there is an operator in the language called "lift". It's an operator you use before an expression, similar to "await" in JavaScript or "go" in Golang. An example expression that uses it is lift x. The rules of the operator is that given x has type T, then lift x has type Lifted<T>. Ok, so what does it do?

Well, lift takes a value that was defined in preflight, and transforms it into a form you can use inflight. The "Lifted" modifier changes what operations are allowed on the type. For example, Bucket has the methods addObject and onCreate, performing lift on a bucket gives you a Lifted<Bucket> which has the methods put and get. Basically, Lifted<T> would give us a way to model in our type system how it is that inflight code is magically changing what operations we can call on objects.

lift would be an irreversible operation (you can't un-lift something), and lifting a value that has already been lifted is a no-op (similar to await in JS). (Lifting an already-lifted value may or may not be allowed, I'm not sure this detail is consequential.)

How does this work with Wing code today? Well, in most code today you haven't had to explicitly use lift because the Wing compiler will automatically adds it for you most of the time. For example, in this snippet:

bring cloud;

let bucket = new cloud.Bucket();
let queue = new cloud.Queue();
let counter = new cloud.Counter();

queue.setConsumer(inflight (message: str) => {
  let id = counter.inc();
  bucket.put("file-${id}", "Hello, ${message}");
});

The compiler would really be providing you with syntax sugar for this:

bring cloud;

let bucket = new cloud.Bucket();
let queue = new cloud.Queue();
let counter = new cloud.Counter();

queue.setConsumer(inflight (message: str) => {
  let id = (lift counter).inc();
  (lift bucket).put("file-${id}", "Hello, ${message}");
});

Notice how "counter" and "bucket" both had to be lifted in the inflight code.

This isn't too unlike how the Rust compiler automatically adds "*" in front of values to save you some keystrokes when you are accessing fields or methods of a value behind a pointer.

What's useful about Lifted<T> is it lets us articulate what operations are possible on certain types. For example, we can decide that Lifted<MutArray<T>> has the same semantics as Array<T>, since you can only perform readonly operations on the array once it has been lifted. This would resolve the question of "how is the type of my MutArray value changing between preflight and inflight?". When you mouse over a lifted MutArray<num>, you would see the type annotated as Lifted<MutArray<num>> or perhaps lifted MutArray<num>.

If T is a preflight function type (like the type of bucket.onCreate), then Lifted<T> could simply be the bottom type ("never") - a clean way to model the fact that preflight functions cannot be used inflight.

It also might give us a convenient solution to some problems we have with structs and serialization. Today, there's a limitation where a Wing struct cannot contain fields of certain types like preflight function types because if you did, it wouldn't be possible to lift the struct into inflight. However, with the Lifted<T> syntax, it's easy to define a semantics that once a struct has been lifted, you can only access the fields as Lifted<T> versions of them.

Another interesting thing about lift is that because it's an operator, in theory you could use it anywhere. To keep things simple, we might start by only allowing you to use lift when you're inflight. But, suppose you did call lift on something in a preflight scope. What kinds of use cases would that enable?

For one, it would give you the control to create multiple lifted copies (or "snapshots") of values. For example:

let var size = 1;

let initial_size = lift x;
size += 5;
let final_size = lift x;

test "print values" {
  log(initial_size); // 1
  log(final_size); // 6
}

The "lift" operator also closes the loop of explaining why you can't reassign to a variable that has been lifted inflight. lift x is not the same as x, hence:

let var x = 1;
inflight () => {
  x = x + 1;
};

desugars into:

let var x = 1;
inflight () => {
  lift x = lift x + 1;
};

and lift x isn't valid on the left-hand side of an equal sign. This is similar to how you can't write

await myPromise = undefined;

in TypeScript.

[ShaiBer]

Great read! And thanks for the credit, but my suggestion was a bit different and less good, to have to explicitly assign lifted expressions into immutable variables in inflight. I think @eladb then suggested the much better lift keyword.
In any case, I'm coming to love this concept more and more and your doc articulates it perfectly.

[eladb]

Love it.

Follow up:

What's the syntax/pattern/idiom for declaring classes and their lifted (aka inflight) api?

[ekeren]

I wasn't in the team discussion so I am probably missing some context, which is actually not a good thing because non of Wing users will have that context.

I am not sure I understand the user value for the lift keyword, when will I the user actually care about it or explicitly use it.

But the idea itself is intriguing, have you consider this lift mechanism as method on an preflight class (maybe even using the existing inflight init)

If we consider fields and variables the same way (@eladb has been talking about adapting the kotlin constructor) it feels that a well defined default implementation of lift/inflight init object method can achieve the same result. (going over all the fields, and lifting them)

I also think that this gives a nice connection to other language, for example in typescript

class CounterClient {
}
class Counter {
lift() { // or inflight init
   return new CounterClient(...)
} 
}

[ShaiBer]

I am not sure I understand the user value for the lift keyword, when will I the user actually care about it or explicitly use it.

The lifting mechanism brings with it some non-standard behaviors, for instance that the lifted data is immutable in inflight.
The idea behind the keyword is to be explicit about it so when the user encounters compiler errors or other behaviors then it will be clearer to them why they get those.
Also, by being explicit about it, they will not write invalid code in the first place.
For example, take @chris's example:
if you write this:

let var x = 1;
inflight () => {
  x =  x + 1;
};

you expect it to work, but if you have to write something like this:

let var x = 1;
inflight () => {
  lift x = lift x + 1;
};
It is more clear why it is not valid

[yoav-steinberg]

I think this is closely related to to #4564. That issue exposes the unexpected behavior of the inflight ctor being executed per client (or per lift). So any changes you perform on inflight (client) data isn't valid across different lifts. Also any global state (a bucket for example) modifier in the inflight ctor is also modifier again when there's another lift.
This confusion can be mitigated by making it more explicit that we're performing a lift (creating a new client). It'll feel more expected that inflight state or inflight ctor are modifier/called.

Dumping some syntax thoughts:

let b = new Bucket();
inflight () => {
  b.put(); // What b was lifted, when? where? what permission did we provide to the host?
}

inflight () => {
  let b = lift(b); // This is explicit, but uses a built in and doesn't feel ctor'ish
}

inflight () => {
  let b = lift b(args...); // Feels a bit more ctor'ish but
}

with lifted b { // A scope style syntax
 b.put()
}

inflight () => {
  let b = lift b(args..., premissions = {...}); // Way to add custom permissions
}

let b_client = lift Bucket(inflight args...) from b; // Most verbose syntax with room for sugar, feels ctor'ish, custom clients..
lift b(inflight args..); // Sugar don't specify client type
b.put(); // If there are no inflight fields we can implicitly lift without an explicit inflight ctor call