> So linear types are incompatible with traditional exception handling.
Nice to see this spelled out. If the instance can be summarily dropped without error you can throw past it, and ideally call it affine instead of linear.
If the instance needs that close() call, you either can't throw past it, or you need to move the live instances into the exception instance as it passes by and deal with them at the catch site. I found a paper discussing that somewhere but didn't keep a reference to it.
A possibly interesting compromise is to allow linear types, but their live range cannot contain an unknown function call, or a function call coloured with throws. That models holding on to some handle and not doing anything too hazardous until you can put it away safely.
Nice to see this spelled out. If the instance can be summarily dropped without error you can throw past it, and ideally call it affine instead of linear.
If the instance needs that close() call, you either can't throw past it, or you need to move the live instances into the exception instance as it passes by and deal with them at the catch site. I found a paper discussing that somewhere but didn't keep a reference to it.
A possibly interesting compromise is to allow linear types, but their live range cannot contain an unknown function call, or a function call coloured with throws. That models holding on to some handle and not doing anything too hazardous until you can put it away safely.