Crosscut

Yesterday, I presented an example that combines linear types and multiple effects. Here it is again:

file
    "a" write
    "b" write

write is going to trigger some kind of effect that signals the host that it needs to write to a file (let's call that Write). In principle, the host could decide not to resume this code after handling the effect, and if that happens, our linear value here (file) would have nowhere to go. But it's linear, so it needs to go somewhere. We can't just drop it implicitly.

I think this can be solved by expressing in the type system, that the code must resume after the Write effect. The host could still not do it, but the host could mess up in any number of ways that language design can't prevent. Any Caterpillar code handling that effect could be forced to always resume, by the compiler. The drawback is the additional complexity this introduces.

Tomorrow, I'd like to look at the second effect that write could trigger, in the case of an error.