Caterpillar

We could annotate functions with the effects they can trigger. I think this is of limited use, for two reasons: It would be redundant, and it would be noisy. Let's start with the redundancy.

I want to represent the effects that a function can have in its parameters and return values. So a function that could write to a file, should take a value that represents that file as an argument, and return a value that represents the modified file. (Which requires linear types).

Annotating a function with a "write file" effect isn't necessary, if it already takes and returns a File. Although, I guess, the effect would provide further clarification, if multiple things can be done to that file. Or maybe having the effect makes taking the linear File value redundant? I'm not sure. There'll be lots of design space to explore, once we get to that.