¶Stack values can be quotations
2023-09-23
At first I assumed that stack values in Swanson cannot just be modeled as a quotation that pushes the contained values onto the runtime stack.
Stack values cannot be quotations
But maybe they can? My concern was that closing over a value would not be compatible with quotations having multiple branches. Implicit in that description is that the closed-over value would only live in one of the branches. And so if you invoked one of the branches that doesn't include the value, the value would silently disappear, violating linearity.
Or described more accurately, the value would not live in all of the quotation's branches. That suggests another way to solve the problem — ensure that the closed-over value does (i.e., is guaranteed to) live in all branches of the closure quotation.
To do that, we'd introduce two kinds of quotations: branchless and branched. A branched quotation is exactly the one we've already been describing: they consist of multiple named branches, and when you invoke one you specify which branch should be executed. A branchless quotation would just consist of a single branch of code, and would have no name. Invoking one would be a separate instruction, where you don't provide a branch name. (The type of those two instructions would be different too: branched invoke would require a branched quotation, and branchless invoke would require a branchless quotation.)
The quote (or close over) instruction would create a branchless quotation. There's only one possible branch, and so we start with the guarantee that the linear value will still be consumed precisely once. (The new branchless quotation is itself a linear value, which must be consumed — via invocation — exactly once, and doing so brings the value back onto the runtime stack with the obligation to eventually consume it.)
The last bit of spackle we need is that compose can compose two quotations of the same kind (branchless with branchless, branched with branched), as you might expect. But it can also combine different kinds of quotation (branchless with branched, branched with branchless).
The semantics of composing two branchless quotations is the most simple: there's still a single (unnamed) branch in the result, and that branch performs LHS's single branch and then RHS's single branch.
Composing two branched quotations is similarly simple. There's a choice of how to handle branched quotations with different sets of branch names. You can either not handle that, by requiring the branch name sets to be identical, or you can have the composed result have the union of the branch names that appear in either side. (This would be like an outer join in SQL; you'd use an empty branch for any branch name that doesn't appear on one side.)
Composing a branched and a branchless quotation would act as if we first translated the branchless quotation into a branched one. We would give it a branch for each of the named branches in the branched quotation. Each of those branches would be a copy of the branchless quotation's single unnamed branch. That would ensure that any values closed over in the branchless quotation end up in every branch in the result, which correctly propagates its responsibility to consume those closed-over values.
This definition of composing branched+branchless makes the union approach to branched+branched not work, because it's not true that “the empty branch” is the correct “null value” to fill in for the “outer join” — you would need the default missing branches to do something with any closed-over values that “every branch” inherited responsibility for. (What would you do with those values? Leave them on the stack? Drop them? If so, how?)
So, it's an alternative, but I'm not sure if it's the right one. I like the idea of a branchless quotation. (I was mimicking those before using a branched quotation with a single branch whose name was the empty string.) But I also like the idea of stack values being a first class and separate thing, with explicit instructions for constructing and deconstructing them.
(Of course, the choice doesn't have to be mutually exclusive...)