Advanced TAPL Linear Lambda Calculus

Question

I'm reading the chapter on Substructural Type Systems from Advanced TAPL (Chapter 1), and am confused about the notion that "linearly qualified data structures will be used exactly once".

Specifically, consider the following (well-typed) expression:

(lin (lambda x : lin bool. x)) (lin true)

The linear variable x appears exactly once, but does not appear in its if-elimination form (i.e., it is never used). Thus, is the type system only meant to guarantee that linearly tagged resources can be used at most once, or is my understanding of the use of a resource at fault here?

The typing rules for the linear lambda calculus I'm referring to is given in Figure 1-5. Thanks!

Answer 1

I don't have access to the book (if possible you should recall the type system) but this is what I understand.

lambda x : lin bool. x is a function that

• takes a linear boolean x,
• returns it: this is linear in x because x appears exactly once in the body of the function.

So the lin declaration when abstracting on some variable means "the body of this abstraction will use the variable exactly once", and this is what the types check.

• chakravyuh: Thanks, but then the type system isn't meant to guarantee that linear resources will be eliminated exactly once. Thus, when evaluating a closed, well-typed, terminating expression with an initially empty store, you aren't guaranteed to have a linear-resource free final store right?
• chi: @chakravyuh My guess is that returned values count as "eliminated by the function caller". Roughly, the expression x should be equivalent to if x then true else false in its static and dynamic semantics (except for one extra reduction step). I don't own the book so I can't fully confirm this.