On "let" and stack instructions

[RossTate]

A number of discussions on stack instructions (like dup) have referenced let as a forthcoming alternative. But I think that, even
having let, there are scenarios where stack instructions have unique advantages, as I discuss below.

Weaknesses of let

I'll start with going over weaknesses.

Size

let is not a particularly small instruction. It specifies a list of variable types, a list of input types, a list of output types, and requires a matching end. That's a lot of infrastructure for simulating something like dup or swap.

Initialization

The stated motivation for let has to do with defining locals for non-defaultable types (particularly non-null types). But let's consider a language like Kotlin that is well-suited to utilize non-null types. Kotlin allows programs like the following:

val s: String
if (...) {
    ... // do stuff
    ... // initialize s
    ... // do more stuff using s
} else {
    ... // do stuff
    ... // initialize s
    ... // do more stuff using s
}
... // do even more stuff using s

In these programs, s is initialized in separate branches, and in Kotlin the String type guarantees (here) that s is not null. With flow-sensitive reasoning, it is easy to see that s is initialized after the if/else, and indeed Kotlin recognizes this fact. But let is not flow-sensitive. As such, this program would require three sets of let just to do stuff using s because there are insufficient stack instructions (e.g. no way to use a value on the stack and keep that value around for after the if/else). And this program illustrates that initialization is not always so simple. WebAssembly's stack is already able to reason about this program correctly, so adding instructions for better accessing/manipulating the stack seems like a better (i.e. smaller binary and easier to generate) alternative.

Type Refinement

Sticking with Kotlin a bit further, Kotlin employs flow-sensitive/occurrence typing, which means that the type of an (immutable) variable can be refined by control flow:

fun demo(x: Any) {
    if (x is String) {
        print(x + x.length) // x has type String here
    }
}

In the above program, because x.length occurs inside an if (x is String), Kotlin refines its type to String rather than its original declared type Any. You can also write this program in the following manner and it'll type check:

fun demo(x: Any) {
    if (x !is String) return
    print(x + x.length) // x has type String here
}

The stack can already reason about the correctness of this program. But without stack instructions, we need to use a let after the branch just because we use x twice. Same would be true if we needed x once but the instructions happened to be in the wrong order.

In Kotlin this type refinement is apparent in the surface language, but it happens even more often in low-level systems, especially for dynamic languages. For languages and implementations relying more on flow-sensitive reasoning, it seems to me that they would be better served by having better stack instructions, since the stack is already flow-sensitive, rather than by let. (This gets even more problematic when one considers existential types, wherein flow-sensitive reasoning is extremely important and widespread, even for type-checking straight-line code, but I won't delve into that technical topic here.)

Affinity

An affine type is one whose values cannot be duplicated. Stack instructions like swap respect affinity, and so you can use swap and the like to shuffle around affine values on the stack. However, you cannot in general do the same with let. With let, you can put the value into a local, but if you cannot duplicate the value then how can you get it? After get, the value is on the stack and in the local—get fundamentally duplicates values, making let useless for affine types.

We ran into this in the proposal for first-class stacks. For reasons I won't repeat here, we recommend using an affine type for stack references. But this meant we could not use let and could not write a bunch of basic programs. So we took advantage of a back door: the null value is not affine. This meant that, instead of get, we could have an instruction get_clear that both gets the value in the local and sets the local to null, thereby eliminating the duplication.

That workaround was useful for other reasons as well (e.g. globals), but there is an irony in the fact that let was introduced for non-nullable types and the only way we could make use of let was to make our type nullable. If ever we want to have a non-nullable variant of stackref, then we will need a proper set of stack instructions because we will not be able to use let.

Strengths of let

This post should not be taken as advocating for removing let. It is just meant to point out that let is not a cure-all for stack instructions. I believe let has a number of uses, one of which is critical. But I do not get the impression that these uses line up with how let has been motivated, so I wanted to add them here.

Organization

This first strength is the one that I believe people already recognize. let is useful for organizing simple code. Many systems do not need the features I mentioned above, and for those systems let provides a nice simple model in which surface-level local variables correspond to WebAssembly local variables.

Even for systems that do need features above, let can be useful for values that are frequently referred to and remain fixed once initialized. One example of this comes from a pattern that will occur in the GC MVP. For technical reasons, the types of inputs to many functions will have to be less precise than they should be, and so inputs will have to first be cast to their expected types before the real body of the function can proceed. let will enable these inputs to be bound to locals with their more refined types after these casts have occurred. That said, unless we want to have a let/end block for each input one by one, we will need stack instructions to perform the relevant casts on each of them before binding them all simultaneously in one let/end block. So stack instructions would be helpful for setting up let blocks.

Branching

let has an annotation/validation cost, but it can also provide annotation/validation savings. Within a let, block types do not need to specify the types of the let-bound variables, and similarly branches to those labels do not need to check compatibility with those let-bound variables. So whereas "organization" is really more of a human-readability benefit, this is a real material benefit of let.

Stack Inspection

Lastly, let has a real expressiveness benefit, though only when we get to stack inspection. With stack inspection, an answer provides a way to access and mutate the contents of an existing frame on the stack. For that to be sound, we need to know that the stack frame has values of particular types, and that the answer does not change the types of those values. let ensures precisely that, both by providing a way to access a definitely initialized value (i.e. local.get) and by providing a way to update the stack frame without changing its type (i.e. local.set).

Summary

let and stack instructions are complementary, not competing, features. While they do overlap, neither subsumes nor conflicts with the other, and where they overlap they each have patterns they are better suited for. My recommendation is to continue advancing let, to also address the shortcomings of our current set of stack instructions, and to advance (the short-term portion of) #1379 as it seems to address the primary technical obstacle to adding stack instructions.

[titzer]

I think pick and dup would be very useful for many producers.

As for type refinement, the br_on_cast instruction from the GC proposal does flow-sensitive type refinement, as does br_on_null, so it is not necessary to use stack instructions in those situations.

[RossTate]

Yeah, I spent some time investigating if there were a good way to make the types of locals flow-sensitively refinable, but I came to the conclusion that the stack really is the best place for such reasoning, and hence that there should be better instructions for manipulating/rearranging values on the stack. The one exception was initialization, which I found could be done just as well on the stack as with locals (with labels indicating which potentially uninitialized locals have been initialized), but that did not seem worth the complexity tradeoff given that it still left other flow-sensitive refinement unaddressed.

[lukewagner]

Agreed that pick (aka rotate) would be quite useful. Not only would pick have a much small encoding (than the equivalent pattern in let) and cheaper validation, but also pick provides a baseline compiler better use-def info which allows the baseline to do better regalloc.

[conrad-watt]

Agreed that pick (aka rotate) would be quite useful.

When pick was previously discussed, it was with the semantics

v' (v^n) (pick n) --> v' (v^n) v'

which would generalise dup. Is this the behaviour you have in your head? A difference for @RossTate would be that rotate (or a different swap/move instruction) works with affine types but (the above) pick doesn't. I agree that either could be useful.

[RossTate]

Based on the use cases above, I see there being uses for 4 instructions (forgive the names):

• get n: copies the nth value on the stack onto the top of the stack
• set n: replaces the (n+1)th value on the stack with the top value on the stack (and updating its type accordingly)
• pluck n: moves the (n+1)th value on the stack to the top of the stack (moving the values in between one slot)
• insert n: moves the top value on the stack to the (n+1)th location on the stack (moving the values in between one slot)

dup is get 0. swap is both pluck 0 and insert 0 (the difference between these only manifests at larger indices).

[conrad-watt]

a further generalisation (my own apologies for the names) could be something like

copy src dst
and
move src dst

where

• get n is copy n 0
• set n is copy 0 n
• pluck n is move n 0
• insert n is move 0 n

modulo off-by-one errors.

I could also imagine a whole matrix of desirable behaviours "copy the src" vs "move the src" and "overwrite the dst" vs "displace the dst", which could be accomplished with a single instruction with enough parameters.

I suppose a problem with these generalisations is that the more immediates are added, the slighter any code size benefit gets. I imagine producers are much more likely to want get and pluck and less likely to want set and insert.

EDIT: thinking it through I far prefer @RossTate's 4 instructions (or just get and pluck) to any further attempt at generalisation, since the combinations of move, overwrite etc. I described above could be accomplished by different combinations of his instructions.

[lukewagner]

Agreed that pick (aka rotate) would be quite useful.

When pick was previously discussed, it was with the semantics

v' (v^n) (pick n) --> v' (v^n) v'

which would generalise dup. Is this the behaviour you have in your head? A difference for @RossTate would be that rotate (or a different swap/move instruction) works with affine types but (the above) pick doesn't. I agree that either could be useful.

Oh hah, our 24-year-old JSOP_PICK opcode has move, not copy semantics. Probably an indication that "pick" isn't a clear mnemonic ;)

I think both copying and moving stack instructions could be valuable. Agreed that move is extra-valuable for affine types; coincidentally that's something we've been discussing recently for interface types.