Linear Lambda Calculus

John Mitchell May 22, 1995

This handout summarizes a “linear” version of typed lambda calculus with function types and products. There are two exercises.

1 Typing rules

The untyped terms we consider are lambda terms extended with pairs and a pattern-matching form of pair destructor (instead of projection functions). The context-free grammar of untyped terms is

e : : = c | x | λx. e | ee | ⟨e, e⟩ | let ⟨x, y⟩ be e_{1} in e_{2}

The type expressions are given by the grammar

A : : = P | A−∘B | A ⊗ B

where P may be any type constant, A−∘B is the type of linear functions from A to B (i.e., functions that use the value of their argument exactly once) and A ⊗ B is a type of pairs ⟨a, b⟩, with a from A and b from B, with the property that each component may be used exactly once.

The typing rules use assertions of the form Γ ▷ e : A, where Γ is a set of assumptions A_{1}: τ_{1}, …, A_{k}: τ_{k} associating types to term variables, with no term variable appearing twice.

There is one typing axiom and five typing rules. In these rules, a comma between sets, as in Σ, Δ in A, means union of disjoint sets. Consequently, we can only type e_{1}e_{2} if no variable appears free in both e_{1} and e_{2} , maintaining the intended linearity of the calculus. (In writing Σ, x:A, we similarly assume that x:A is not in Σ.)

I  x:A ▷ x:A

Subst  \frac{Σ ▷ e_{1}:A x:A, Γ ▷ e_{2}:B}{Σ, Γ ▷ [e_{1}/x]e_{2}:B}

A  \frac{Δ ▷ e_{1}:(A−∘B)  Σ ▷ e_{2}:A}{Σ, Δ ▷ (e_{1} e_{2}):B}

−∘R  \frac{Σ, x:A ▷ e:B}{Σ ▷ λx. e:(A−∘B)}

⊗L \frac{Δ ▷ e_{1}:(A ⊗ B) Σ, x:A, y:B ▷ e_{2}:C}{Σ, Δ ▷ let ⟨x, y⟩ be e_{1} in e_{2}: C}

⊗R  \frac{Σ ▷ e_{1}:A  Γ ▷ e_{2}:B}{Σ, Γ ▷ ⟨e_{1}, e_{2}⟩:(A ⊗ B)}

Exercise: Show that the substitution typing rule can be dropped without changing the set of derivable typing assertions. In other words, show that if Γ ▷ e : A is derivable using the rules above, we may also prove Γ ▷ e : A without using Subst.

2 Adjunctions and Currying

There is a close correspondence between traditional typed lambda calculus with a terminal type 1, pairing and function types and cartesian closed categories.

The adjunction between products and exponentials (function types) in cartesian closed categories is essentially the isomorphism associated with Currying, i.e.,

A → B → C ≅ A × B → C

This is also sometimes written

\begin{matrix}A → B → C \\ A × B → C \end{matrix}

where the double horizontal line indicates a “natural isomorphism”. This property is proved in the typed lambda calculus by showing that the two maps

\begin{matrix}x: σ ▷ M : τ → ρ & ↦ & x: σ, y: τ ▷ My : ρ \\ x: σ, y: τ ▷ N : ρ & ↦ & x: σ ▷ λy: τ. N : τ → ρ \end{matrix}

are inverses. This proof uses the equational theory of typed lambda calculus.

The adjunction involving products and the terminal object involves the isomorphism

(A → B) × (A → C) ≅ A → B × C

However, there is a slight pun here regarding the first ×, which is really product in the category of categories, while the second is product in the category at hand. We can be clearer about this using the second notation above, writing

A → B, A → C
A → B × C

meaning that there is a natural isomorphism between pairs of arrows of the types given above the lines and arrows of the type given below the lines. This property is proved in the typed lambda calculus by showing that the two maps

x: σ ▷ M : τ x: σ ▷ N : ρ ↦  x: σ ▷ ⟨M, N⟩ : τ × ρ
x: σ ▷ M : τ × ρ  ↦ x: σ ▷ Proj_{1}M : τ x: σ ▷ Proj_{2}M : ρ

are inverses. This proof again uses the equational theory of typed lambda calculus.

Exercise: Consider the analogous properties for linear lambda calculus, with −∘ replacing → and ⊗ replacing ×. Show that the first of these isomorphism holds for the linear lambda calculus and explain why the second would cause linearity of functions to fail. In order to complete this part of the problem, you will have to make some assumptions about the equational theory of linear lambda calculus. To help you think about this, part of a structured operational semantics is given on the next page.

3 Operational semantics

−∘L \frac{e_{1} → → λx.v  e_{2} → → c  [c/x]v → → d}{(e_{1}e_{2}) → → d}
−∘ R  λx.e → → λx.e

⊗L  \frac{e_{1} → → ⟨c, d⟩  [c/x, d/y]e_{2} → → e}{let ⟨x, y⟩ be e_{1} in e_{2} → → e}

⊗R  \frac{e_{1} → → v_{1}  e_{2} → → v_{2}}{⟨e_{1}, e_{2}⟩ → → ⟨v_{1}, v_{2}⟩}