[JonChesterfield]

Linear types are more powerful than affine in terms of implementing code that cannot go wrong as enforced by the type system. State machines reified in application code.

Affine is fine if there's a catch all operation available for when the value drops out of scope which the compiler inserts. You can call deallocate or similar when an exception comes through the call stack.

If the final operation is some function that returns something significant, takes extra arguments, interacts with the rest of the program in some sort of must-happen sense, then calling a destructor implicitly doesn't cover it.

There's some interesting ideas around associating handlers with functions to deal with exceptions passing through but I think I've only seen that in one language. The simple/easy approach is to accept that exceptions and linear types are inconsistent.

[Rusky]

One way you can think of the exception unwinding stuff is that each call provides not just one continuation (the usual return address) but two (also one for the cleanup), and that these are combined using the & connective of linear logic.

This means both paths must use the same set of resources, and exactly one of them must be invoked. Interestingly, in linear logic this is equivalent (using De Morgan dualities) to a single continuation that expects a sum type: A^⊥ & B^⊥ = (A ⊕ B)^⊥.

[JonChesterfield]

That's exactly the challenge though. The puzzle isn't in the compiler internals, it's in the language syntax.

The happy case is you have an instance of a linear type, you call some unrelated function which doesn't use that instance, then lexically later in the caller you do something with it. All typechecks easily, all is well.

If that unrelated function wants to throw an exception, reinstate some other continuation, or in any other way not execute the use of the instance after said function call, you have a design puzzle.

Affine types solve it by saying the object didn't need to be used anyway, so whatever. No type problems. Whatever deals with garbage collection will handle it.

Linear type systems usually solve it by refusing to let the called function branch to somewhere other than the nominal return site, aka no call/cc or exceptions in the language. Possibly function colouring to say no call/cc or exceptions in anything branched to within the lifetime of a linear variable.

The obvious answer to a compiler dev is that call/return is sugar anyway - all the variables "live across a call site" are implicitly arguments to the branch, so they're available tn whatever continuation the callee invokes. The plumbing is all fine. Typechecking is abstract interpretation so that's all good too, one can totally build the thing.

The missing piece is how you get the programmer to describe what they intend to happen to the linear instance on any continuations which are not the one denoted by the code immediately lexically after the function call 'instruction'. Where the syntax in question is an exception, it means "branch to somewhere implicitly recorded in a side table", so for the linear type use to work out you need to somehow annotate what is supposed to happen to the thing in that case. I don't know of a good notation for that.

(functions taking sum types are prone to being implemented as a branch on which field as active so you're definitely right that success+failure continuations can be transformed into one taking a sum - it's a reversible transform - but I don't think it helps the notation challenge).

[Rusky]

I was talking about language syntax, and in particular the way proof terms for linear logic (which linear type systems come from) already provide a syntax for this.

But in fact we also have multiple options on the more programmer-familiar side of this- `try/finally` blocks, `defer`, etc. The problem isn't limited to linear types so it's already been pretty thoroughly explored.

[fdupress]

Linear types and handlers are even more inconsistent, given the continuations could be run more than once if not careful.

[alexisread]

This is why, in Koka, there exists initially and finally blocks, to control resource cleanup https://koka-lang.github.io/koka/doc/book.html#sec-resource

I think linear types and exceptions can play well together if you use controlled effects like this.