Discussion: Taste of Linear Logic
Comment on Philip Wadler's paper "A Taste of Linear Logic", or raise a question.
How does this logic relate to memory management? Is there a relationship between linear logic and the way, say, Rust handles memory management? It seems like garbage collection at compile-time would be a great application of linear logic.
Is there a rule of thumb when to use intuitionistic logic and linear logic in real systems? Is it only when copying information is impossible/inefficient?
I went through most of the rules. I just curious about what's the difference between the assumption in different logic?
Why would somebody need Fixpoints? Is there a specific class of computable functions that can't be expressed in typed term calculus?
The argument that linear logic is strictly more expressive than intuitionistic logic is convincing. However, I don't fully understand what form that extra expressivity takes in the world of types; it seems to lie in the
case s of !x → uproductions of section 5's term grammar, but I'm having trouble grokking it.
"As we shall see, an assumption of the form ⟨!A⟩ is in a sense equivalent to an assumption of the form [A]. However, they differ in that a linear assumption – even one of the form ⟨!A⟩ – must be used exactly once in a proof, while an intuitionistic assumption may be used any number of times." I don't really understand this. How do you "use up" ⟨!A⟩