Chapter 1: ライフタイムの形式的理解
学習目標
- ライフタイムの数学的定義を理解する
- 領域ベース型システムの理論を学ぶ
- サブタイピング関係を深く理解する
- variance（変性）の概念を習得する
- ライフタイム推論アルゴリズムを学ぶ
---
1.1 ライフタイムの数学的定義
1.1.1 ライフタイムとは何か
形式的定義：
ライフタイム α は、プログラムの実行における
時間区間の集合である。
α = {[start₁, end₁), [start₂, end₂), ...}
where startᵢ, endᵢ ∈ プログラムポイント
例：
fn example() {
let x = 5; // ← P1
let r = &x; // ← P2
println!("{}", r); // ← P3
} // ← P4
// 'x のライフタイム: [P1, P4)
// 'r のライフタイム: [P2, P4)
1.1.2 ライフタイムの包含関係
定義：
'a outlives 'b ⟺ 'a ⊇ 'b
記法: 'a: 'b
つまり、'aが有効な期間は'bが有効な期間を完全に包含する
例：
fn foo<'a, 'b>(x: &'a i32, y: &'b i32) -> &'a i32
where
'a: 'b, // 'a outlives 'b
{
x
}
視覚化：
時間軸 ──────────────────────────►
'a: ┌──────────────────────────┐
│ │
'b: │ ┌──────────┐ │
│ │ │ │
└────┴──────────┴──────────┘
'a: 'b が成立（'a は 'b を包含）
---
1.2 領域ベース型システム
1.2.1 Tofte-Talpin 領域推論
歴史的背景：
- 1994年にMads TofteとJean-Pierre Talpinが提案
- 関数型言語のメモリ管理のため
- Rustのライフタイムシステムの理論的基礎
基本概念：
型 τ ::= int | bool | τ₁ → τ₂ | ref^ρ τ
領域注釈 ──┘
ρ: 領域（region）= Rustのライフタイム
1.2.2 型付け規則
参照の生成：
Γ ⊢ e : τ ρ fresh
─────────────────────
Γ ⊢ ref e : ref^ρ τ
参照の読み取り：
Γ ⊢ e : ref^ρ τ
────────────────
Γ ⊢ !e : τ
---
1.3 サブタイピングと変性
1.3.1 ライフタイムのサブタイピング
定義：
'a: 'b
─────────────────────
&'a T <: &'b T
（より長いライフタイムの参照は、
より短いライフタイムの参照として使える）
例：
fn take_short<'a>(r: &'a i32) {
// ...
}
fn example() {
let x = 5; // 'x
{
let y = 10; // 'y (shorter)
let r: &i32 = &x; // 型: &'x i32
// &'x i32 <: &'y i32 なので OK
take_short::<'y>(r);
}
}
1.3.2 Variance（変性）
定義：
┌─────────────────────────────────────────────────────────┐
│ Variance の3種類 │
├─────────────────────────────────────────────────────────┤
│ │
│ Covariant（共変）: │
│ 'a: 'b ⟹ F<'a> <: F<'b> │
│ 例: &'a T, *const T │
│ │
│ Contravariant（反変）: │
│ 'a: 'b ⟹ F<'b> <: F<'a> │
│ 例: fn(&'a T) │
│ │
│ Invariant（不変）: │
│ サブタイピング関係なし │
│ 例: &'a mut T, Cell<'a T> │
│ │
└─────────────────────────────────────────────────────────┘
具体例：
// Covariant: &'a T
fn covariant_example<'a, 'b>(x: &'a i32) -> &'b i32
where
'a: 'b,
{
x // OK: &'a i32 <: &'b i32
}
// Contravariant: for<'a> fn(&'a T)
fn contravariant_example<'a, 'b>()
where
'a: 'b,
{
let f: fn(&'a i32) = |_| {};
let g: fn(&'b i32) = f; // OK: 'a: 'b なら fn(&'b) <: fn(&'a)
}
// Invariant: &'a mut T
fn invariant_example<'a, 'b>(x: &'a mut i32) -> &'b mut i32
where
'a: 'b,
{
// x // エラー！&'a mut i32 は &'b mut i32 のサブタイプではない
unimplemented!()
}
1.3.3 なぜ &mut T は Invariant か
// もし &'a mut T が covariant だったら...
fn evil<'a, 'b>(short: &'a mut &'b i32, long: &'a mut &'a i32) {
// &'a mut &'a i32 <: &'a mut &'b i32 と仮定
*short = *long; // 型は合うように見える
// しかし 'b < 'a なので、shortが長いライフタイムを持つことに！
}
// 実際にはコンパイルエラー
---
1.4 ライフタイム推論
1.4.1 制約ベース推論
アルゴリズムの概要：
1. 各参照にライフタイム変数を割り当て
let x = &y ⟹ x: &'a T
2. 制約を生成
- 代入: x = y ⟹ 'x ⊇ 'y
- 関数呼び出し: f(x) ⟹ 制約を関数シグネチャから導出
- スコープ: { let x = ...; } ⟹ 'x ⊆ スコープ
3. 制約を解く（最小不動点）
- 最も制限的な解を求める
4. 矛盾があればエラー
例：
fn example() {
let x = 5; // 'x
let r = &x; // 'r
let s = r; // 's
println!("{}", s);
}
// 制約:
// 'r ⊆ 'x (r は x を借用)
// 's = 'r (s は r のコピー)
// 's ⊆ println呼び出しまで
// 解:
// 'x = [L1, L4)
// 'r = [L2, L4)
// 's = [L3, L4)
1.4.2 Higher-Rank Trait Bounds (HRTB)
for<'a> 構文：
// 全てのライフタイムについて成立
fn example<F>(f: F)
where
F: for<'a> Fn(&'a i32) -> &'a i32,
{
let x = 5;
let y = f(&x);
println!("{}", y);
}
形式的意味：
∀ 'a. F: Fn(&'a i32) -> &'a i32
（任意のライフタイム'aについて、
Fは&'a i32を受け取り&'a i32を返す関数）
---
1.5 早期束縛 vs 遅延束縛
1.5.1 Early-bound Lifetimes
fn foo<'a>(x: &'a i32) -> &'a i32 {
// ^^
// 早期束縛：関数呼び出し時に決定
x
}
// 呼び出し側
foo::<'static>(&5); // 明示的に指定可能
1.5.2 Late-bound Lifetimes
// HRTBで使用
fn bar(f: for<'a> fn(&'a i32)) {
// ^^^^^^^
// 遅延束縛：使用時に決定
}
違い：
Early-bound:
- 関数のジェネリクスパラメータとして
- 明示的に指定可能
- 単相化される
Late-bound:
- for<'a> で導入
- 呼び出し元で自動推論
- 柔軟性が高い
---
1.6 ライフタイムと型の関係
1.6.1 ライフタイムパラメータの位置
struct Foo<'a, T> {
// ^^ ^
// | 型パラメータ
// ライフタイムパラメータ
x: &'a T,
}
// ライフタイムは型の一部
type Alias<'a> = &'a i32;
1.6.2 Associated Type とライフタイム
trait Iterator {
type Item; // 関連型
fn next(&mut self) -> Option<Self::Item>;
}
// ライフタイム付き関連型
trait LendingIterator {
type Item<'a> where Self: 'a;
fn next<'a>(&'a mut self) -> Option<Self::Item<'a>>;
}
---
1.7 'static の特殊性
1.7.1 'static の2つの意味
1. 静的ライフタイム：
let s: &'static str = "hello";
// プログラム全体で有効
2. 'static トレイト境界：
fn foo<T: 'static>(x: T) {
// T は 'static ライフタイムの参照を含まない
// または、T自体が所有型
}
1.7.2 'static の形式的定義
'static = [program_start, program_end)
任意のライフタイム 'a について:
'static: 'a （'static は全てのライフタイムをoutlive）
---
1.8 まとめ
1.8.1 理論的基盤
ライフタイムシステムは以下に基づく：
- 領域ベース型システム（Tofte-Talpin）
- サブタイピング（順序関係）
- Variance（型構築子の振る舞い）
- 制約ベース推論（最小不動点）
- ライフタイムは時間区間
- 包含関係がサブタイピングを決定
- Varianceは安全性を保証
- コンパイラが制約を解く
1.8.2 実用的な理解
---
練習問題
問題1
以下の制約を満たすライフタイムの最小解を求めなさい。'a ⊇ 'b
'b ⊇ 'c
'c ⊇ [L5, L10)
問題2
なぜ&'a mut T が invariant である必要があるか、反例を用いて説明しなさい。問題3
以下のコードでライフタイム推論がどのように働くか説明しなさい。fn foo<'a>(x: &'a i32, y: &'a i32) -> &'a i32 {
if x > y { x } else { y }
}
---