¶Branches are the key
¶2022-07-23
The key idea in Swanson is that invokables have branches. That is, in linear logic, an invokable is not modeled as a linear function, but as a linear sum of linear functions. Each branch has the same closure set but can receive differing sets of inputs. To invoke the invokable, you must choose one of the branches. (That means that we're using additive conjunction (&) to join the branches, since it is the invoker who gets to choose which branch to invoke.) Doing so consumes the entire invokable, preventing the other branches from ever being executed. As long as the branch correctly consumes its (shared) closure set and all of its inputs, linearity is satisfied.
¶2022-07-27
Baker1994 talks about this a bit on page 6, when talking about if in Linear Lisp. He mentions that you must “relax...the linearity condition to allow a reference in both arms, so long as they are not executed concurrently or speculatively”. There's also an interesting footnote that I need to investigate further: “Typestates [Strom83] can check linearity in complex control structures”.