<p>In Chapter 1 of <em>Advanced Topics in Types and Programming Languages</em>, the following rule is presented for the introduction of a product in a linear/unrestricted type system:</p>
<p>(<span class="math-container">$\circ$</span> is context concatenation, <span class="math-container">$q$</span> represents some given modality (linear/unrestricted))</p>
<p><span class="math-container">$$
\frac{\Gamma_1 \vdash t_1 : T_1\quad\Gamma_2 \vdash t_2 : T_2 \quad q\,(T_1) \quad q\,(T_2)}
{\Gamma_1 \circ\Gamma_2 \vdash q\,\langle t_1, t_2\rangle : q\,(T_1 * T_2)}
$$</span></p>
<p>I don't quite understand how this product rule works. You can't allow the variables put into the product to persist after being put into the product or you'll break the linearity constraint, right? This presentation seems to me to allow them to persist as such.
For example, if I'm reading it correctly, this would allow the following:</p>
<pre><code>let a : lin int = lin 5 in
let b : lin char = lin 'c' in

// If i'm reading correctly, you can still use `a` and `b` after this line
let p = (a, b) in

let (x, y) = p in

// Now you have two instances of the same linear variable, no?
</code></pre>

<types><type-systems><substructural-types>
Why does ATTAPL's linear product introduction rule not delete the objects from the context?
<p>Technically, the linear lambda calculus presented in <em>ATTAPL</em> does not include a <code>let</code> construct, so your hypothetical “bad program” is not even syntactically legitimate. Of course, <code>let</code> can be considered an abbreviation for an application of a lambda in the usual way, but if we want to work through an example using the provided typing rules, it is clearer if we avoid such abbreviations. Let’s therefore start by rewriting your example to a simpler term that is directly accepted by the language’s grammar yet still illustrates your objection:</p>
<pre><code>lin λ a:lin Bool.
  split lin &lt;a, un true&gt; as x, _ in
  lin &lt;a, x&gt;
</code></pre>
<p>Here we have a linear variable <code>a</code> that is used twice, once to construct the pair <code>&lt;a, un true&gt;</code> and a second time in the body of the <code>split</code>. If this were allowed, we would have duplicated <code>a</code>, so it must somehow be illegal. To see how, consider the invariants described at the top of the “Typing” subsection of section 1.2:</p>
<blockquote>
<p>To ensure that linear objects are used exactly once, our type system maintains two important invariants.</p>
<ol>
<li><p>Linear variables are used exactly once along every control-flow path.</p>
</li>
<li><p>Unrestricted data structures may not contain linear data structures. More generally, data structures with less restrictive type may not contain data structures with more restrictive type.</p>
</li>
</ol>
</blockquote>
<p>Your question is clearly about the enforcement of invariant 1. A paragraph on the following page explains how it is maintained:</p>
<blockquote>
<p>We maintain the first invariant through careful context management. When type checking terms with two or more subterms, we pass all of the unrestricted variables in the context to each subterm. However, we split the linear variables between the different subterms to ensure each variable is used exactly once. Figure 1-4 defines a relation, <span class="math-container">$Γ = Γ_1 ◦ Γ_2$</span>, which describes how to split a single context in a rule conclusion (<span class="math-container">$Γ$</span>) into two contexts (<span class="math-container">$Γ_1$</span> and <span class="math-container">$Γ_2$</span>) that will be used to type different subterms in a rule premise.</p>
</blockquote>
<p>In other words, all of the magic is in context splitting. Since every subterm must use disjoint sets of linear variables, using a linear variable multiple times is impossible. We can see this in the typechecking rule for <code>split</code>:
<span class="math-container">$$
\begin{array}{l}
Γ_1 ⊢ t_1 : q\ (T_1 * T_2) \\
Γ_2, x{:}T_1, y{:}T_2 ⊢ t_2 : T \\
\hline
Γ_1 ◦ Γ_2 ⊢ \mathbf{split}\ t_1\ \mathbf{as}\ x, y\ \mathbf{in}\ t_2 : T
\end{array}
$$</span>
In our example program, the variable <code>a</code> appears in both <span class="math-container">$t_1$</span> and <span class="math-container">$t_2$</span>, so it must be present in both <span class="math-container">$Γ_1$</span> and <span class="math-container">$Γ_2$</span>. However, <code>a</code> is a linear variable, so this is not allowed by the definition of context splitting. Therefore, this program is (correctly) rejected.</p>
<p>Note that this “careful context management” means that the system is not syntax-directed, as one cannot know ahead of time which variables should appear in which context. For that reason, this formulation of the rules constitutes a <em>declarative</em> type system for the linear lambda calculus. The following section, titled “Algorithmic Linear Type Checking”, presents a different formulation of the rules using output contexts, which may look closer to what you were expecting.</p>

CC BY-SA 4.0
2023-11-15T13:24:16.010Z
2023-11-15T13:37:38.927Z
2023-11-15T13:37:38.927Z
Alexis King
# Why does ATTAPL's linear product introduction rule not delete the objects from the context?
Posted by: username_0 on 2023-11-15
In Chapter 1 of Advanced Topics in Types and Programming Languages, the following rule is presented for the introduction of a product in a linear/unrestricted type system:
($\circ$ is context concatenation, $q$ represents some given modality (linear/unrestricted))
$$
\frac{\Gamma_1 \vdash t_1 : T_1\quad\Gamma_2 \vdash t_2 : T_2 \quad q\,(T_1) \quad q\,(T_2)}
{\Gamma_1 \circ\Gamma_2 \vdash q\,\langle t_1, t_2\rangle : q\,(T_1 * T_2)}
$$
I don't quite understand how this product rule works. You can't allow the variables put into the product to persist after being put into the product or you'll break the linearity constraint, right? This presentation seems to me to allow them to persist as such.
For example, if I'm reading it correctly, this would allow the following:
let a : lin int = lin 5 in
let b : lin char = lin 'c' in

// If i'm reading correctly, you can still use `a` and `b` after this line
let p = (a, b) in

let (x, y) = p in

// Now you have two instances of the same linear variable, no?
**Tags:** types type-systems substructural-types
---
## 1 answers
### Answer by username_1 on 2023-11-15. Score: 10 | Accepted answer
Technically, the linear lambda calculus presented in ATTAPL does not include a let construct, so your hypothetical “bad program” is not even syntactically legitimate. Of course, let can be considered an abbreviation for an application of a lambda in the usual way, but if we want to work through an example using the provided typing rules, it is clearer if we avoid such abbreviations. Let’s therefore start by rewriting your example to a simpler term that is directly accepted by the language’s grammar yet still illustrates your objection:
lin λ a:lin Bool.
  split lin  as x, _ in
  lin 

Here we have a linear variable a that is used twice, once to construct the pair  and a second time in the body of the split. If this were allowed, we would have duplicated a, so it must somehow be illegal. To see how, consider the invariants described at the top of the “Typing” subsection of section 1.2:

To ensure that linear objects are used exactly once, our type system maintains two important invariants.

Linear variables are used exactly once along every control-flow path.

Unrestricted data structures may not contain linear data structures. More generally, data structures with less restrictive type may not contain data structures with more restrictive type.



Your question is clearly about the enforcement of invariant 1. A paragraph on the following page explains how it is maintained:

We maintain the first invariant through careful context management. When type checking terms with two or more subterms, we pass all of the unrestricted variables in the context to each subterm. However, we split the linear variables between the different subterms to ensure each variable is used exactly once. Figure 1-4 defines a relation, $Γ = Γ_1 ◦ Γ_2$, which describes how to split a single context in a rule conclusion ($Γ$) into two contexts ($Γ_1$ and $Γ_2$) that will be used to type different subterms in a rule premise.

In other words, all of the magic is in context splitting. Since every subterm must use disjoint sets of linear variables, using a linear variable multiple times is impossible. We can see this in the typechecking rule for split:
$$
\begin{array}{l}
Γ_1 ⊢ t_1 : q\ (T_1 * T_2) \\
Γ_2, x{:}T_1, y{:}T_2 ⊢ t_2 : T \\
\hline
Γ_1 ◦ Γ_2 ⊢ \mathbf{split}\ t_1\ \mathbf{as}\ x, y\ \mathbf{in}\ t_2 : T
\end{array}
$$
In our example program, the variable a appears in both $t_1$ and $t_2$, so it must be present in both $Γ_1$ and $Γ_2$. However, a is a linear variable, so this is not allowed by the definition of context splitting. Therefore, this program is (correctly) rejected.
Note that this “careful context management” means that the system is not syntax-directed, as one cannot know ahead of time which variables should appear in which context. For that reason, this formulation of the rules constitutes a declarative type system for the linear lambda calculus. The following section, titled “Algorithmic Linear Type Checking”, presents a different formulation of the rules using output contexts, which may look closer to what you were expecting.
---
