「型システム入門」第4章の実装をRustでやってみた
「型システム入門 −プログラミング言語と型の理論−」（以下TaPL）は、型システムを理解するうえで必要な基礎知識を学ぶことができる、文字通り型システムの入門書である。最近、型とは実際に何なのかを知るために、この本を読んで勉強している。
第4章の型なし計算体系の実装がRustでもできそうだと思ったので、Rustで実装した。
環境
Rust 1.61.0 安定板
前置き
この本はがっつり数学（主に離散数学）の知識を必要とする。特に集合・関係や数学的帰納法がわからないと厳しいだろう。お恥ずかしながら自分は数学が苦手と言っても良く、第4章まで必死に数学が苦手ながらもなんとか読み進めた。
第4章は「型なし計算体系」のML実装である。この章では第3章で学習した型なし計算体系を、ML系言語であるOCamlで実装する章である。実際のところ第4章はML系言語でなくとも、ガベージコレクション（以下GC）及びパターンマッチングがある言語ならばどの言語でも容易に実装が可能である。たとえばパターンマッチ拡張付きScheme、Haskell、比較的最近の言語だとScalaやF#、Elmなどがある。
Rustはパターンマッチングはサポートされているが、GCはサポートされていない。これはRustがシステムプログラミング言語であるためである。動的メモリ確保などは自動でやってくれるのではなく、自分でやらなければならない。
もちろんRustはメモリ安全な言語であり、所有権やライフタイム（リージョン）などによってunsafeでない場合に限りRustが保証できる範囲でメモリ安全性を保証してくれる*1し、動的メモリも確保こそ手動でする必要があるがRAII*2によって自動で解放してくれる仕組みが備わっている*3。
しかしそうだとしてもやはり自動で動的メモリの確保と解放を（ほぼ意識することなく）行ってくれる言語と比べれば、Rustで実装するのは容易いことではない。まぁ、筆者はそれを知ったうえで、どう対処すれば良いのかわかっていたのでRustで実装してみようと思ったわけだが。
1. 前提の知識
1.1 型なし計算体系の操作的意味論
まず型なし計算体系を実装するためには、その操作的意味論における定義の要約は最低限必要である。それを以下に示す。ただし、ここで定義されているものは構造的操作的意味論によるものである。
tは項である。これは第4章において正規形*4でないものも含めたメタ変数である。succ t1のt1などは項tの部分項という。
vは値である。第4章における値とは、数値だけでなくブール値も含む。nvは値のうち数値であることを示す。
tを評価してt'となるとき、t → t'は評価関係式という。
たとえば評価規則E-IFTRUEはif true then t2 else t3 → t2という評価関係式になっているが、これは「if true then t2 else t3を評価することでt2を得る」ということを示している。
評価規則にはE-IFなど下のif t1 then t2 else t3 → if t1' then t2 else t3の上にt1 → t1'といった形の評価関係式がある場合もある。これは「t1 → t1'のとき、if t1 then t2 else t3を評価することでif t1' then t2 else t3を得る」ということを示している。
ちなみに、本来、ブール値が適用されるべきなのにブール値でなかったり、数値が適用されるべきなのに数値でなかったりする部分項が存在した場合、その部分項を持つ項はそれ以上評価できない。こういった項を行き詰まり状態という。たとえばif nv1 then t2 else t3はnv1が数値であるため、E-IFTRUE、E-IFFALSE、E-IFのいずれも当てはまらない。したがってこの項はこれ以上評価できない行き詰まり状態となる。
1.2 Rustにおける再帰型
まず今回の型なし計算体系を実装するにあたり、ツリー構造が必要である。そのため、再帰型を定義しなければならないのだが、Rustの型システムにおけるほとんどの場合においてはコンパイル時に型のメモリサイズがわかっていることを前提としているので再帰型を容易に定義することはできない。しかし、定義する型の中でボクシング*5された同じ型を定義することで再帰型を定義することが可能となる。ちなみにわかっているとは思うが、ここでいうボクシングとは、スポーツのことではなく、値をヒープメモリに格納された値へのポインタに変換することである。
Rustでボクシングするためには、Box<T>型を用いる。そしてBox<T>型を用いた簡単な再帰型の定義の例を以下に示す。
/// リスト型 enum MyList<T> { Cons(T, Box<MyList<T>>), Nil, }
ちなみにRustにおけるBox<T>型はポインタであるため、基本参照外し*が必要となる。
2. 構造的操作的意味論を用いた型なし計算体系の実装
構造的操作的意味論は、1ステップずつ評価する操作的意味論であり、小ステップスタイルとも呼ばれる。それを実装したRustコードを以下に示す。
/// 構文 #[derive(Debug, Eq, PartialEq, Clone)] enum Term { TmTrue, // 定数真 TmFalse, // 定数偽 TmIf(Box<Term>, Box<Term>, Box<Term>), // 条件式 TmZero, // 定数ゼロ TmSucc(Box<Term>), // 後者値 TmPred(Box<Term>), // 前者値 TmIszero(Box<Term>), // ゼロ判定 } impl Term { /// 条件式の単純化 #[inline] fn tm_if(t1: Self, t2: Self, t3: Self) -> Self { Self::TmIf(Box::new(t1), Box::new(t2), Box::new(t3)) } /// 後者値の単純化 #[inline] fn tm_succ(t1: Self) -> Self { Self::TmSucc(Box::new(t1)) } /// 前者値の単純化 #[inline] fn tm_pred(t1: Self) -> Self { Self::TmPred(Box::new(t1)) } /// ゼロ判定の単純化 #[inline] fn tm_iszero(t1: Self) -> Self { Self::TmIszero(Box::new(t1)) } /// 項が数値であるか判定 fn is_numeric_val(&self) -> bool { match self { Self::TmZero => true, Self::TmSucc(t) => t.is_numeric_val(), _ => false, } } /// 項が値であるか判定 fn is_val(&self) -> bool { match self { Self::TmTrue | Self::TmFalse => true, t => t.is_numeric_val(), } } /// 構造的操作的意味論による評価 fn eval1(&self) -> Option<Self> { match self { Self::TmIf(t1, t2, t3) => match &**t1 { // E-IfTrue Self::TmTrue => Some((**t2).clone()), // E-IfFalse Self::TmFalse => Some((**t3).clone()), // E-If t1_ => t1_.eval1() .map(|t1__| { Self::tm_if(t1__, (**t2).clone(), (**t3).clone()) }), }, // E-Succ Self::TmSucc(t1) => t1.eval1().map(Self::tm_succ), Self::TmPred(t1) => match &**t1 { // E-PredZero Self::TmZero => Some(Self::TmZero), // E-PredSucc Self::TmSucc(nv1) if nv1.is_numeric_val() => Some((**nv1).clone()), // E-Pred t1_ => t1_.eval1().map(Self::tm_pred), }, Self::TmIszero(t1) => match &**t1 { // E-IszeroZero Self::TmZero => Some(Self::TmTrue), // E-IszeroSucc Self::TmSucc(nv1) if nv1.is_numeric_val() => Some(Self::TmFalse), // E-Iszero t1_ => t1_.eval1().map(Self::tm_iszero), }, // 正規形 _ => None, } } /// 評価 /// 正規形(`None`)になるまで評価を繰り返す fn eval(self) -> Self { if let Some(t) = self.eval1() { t.eval() } else { self } } }
一つずつ見ていこう。
2.1 構文
1.1にて定義した構文通りにRustで書いたのが以下の部分である。
/// 構文 #[derive(Debug, Eq, PartialEq, Clone)] enum Term { TmTrue, // 定数真 TmFalse, // 定数偽 TmIf(Box<Term>, Box<Term>, Box<Term>), // 条件式 TmZero, // 定数ゼロ TmSucc(Box<Term>), // 後者値 TmPred(Box<Term>), // 前者値 TmIszero(Box<Term>), // ゼロ判定 }
Term型の値そのものが項であり、部分項の型もTerm型である・・・のだが、1.2よりRustでは部分項となる値はボクシングされている必要があるのだった。そのため、部分項の型はBox<Term>型となる。
あとは、構文通り定義していくだけである。
ちなみにTaPLではすべての項にその項がどこを示しているのかなどといった情報を表現するinfo型の値が要素として含まれているがこの記事ではわかりやすさのために省略している。もしinfo型の値も含めて定義したいならば、独自にInfo型を定義し、以下のように書く必要があるだろう。
/// 構文 #[derive(Debug, Eq, PartialEq, Clone)] enum Term { TmTrue(Info), // 定数真 TmFalse(Info), // 定数偽 TmIf(Info, Box<Term>, Box<Term>, Box<Term>), // 条件式 TmZero(Info), // 定数ゼロ TmSucc(Info, Box<Term>), // 後者値 TmPred(Info, Box<Term>), // 前者値 TmIszero(Info, Box<Term>), // ゼロ判定 }
これ以降、Info型については無視して考える。もし含めたいならば、以降のコードは読み替える必要があることに注意。
2.2 部分項のある項の単純化
部分項のある項を生成するとき、部分項にいちいちBox::new()によって部分項をボクシングしなければならない。それを軽減させるために、普通の部分項に適用するだけで自動でボクシングしてくれる関連関数を定義した。それを以下に示す。
impl Term { /// 条件式の単純化 #[inline] fn tm_if(t1: Self, t2: Self, t3: Self) -> Self { Self::TmIf(Box::new(t1), Box::new(t2), Box::new(t3)) } /// 後者値の単純化 #[inline] fn tm_succ(t1: Self) -> Self { Self::TmSucc(Box::new(t1)) } /// 前者値の単純化 #[inline] fn tm_pred(t1: Self) -> Self { Self::TmPred(Box::new(t1)) } /// ゼロ判定の単純化 #[inline] fn tm_iszero(t1: Self) -> Self { Self::TmIszero(Box::new(t1)) } /* 省略 */ }
これによって項の生成がある程度楽になる。以下は単純化しない場合とする場合の比較である。
// 条件式 Term::TmIf(Box::new(t1), Box::new(t2), Box::new(t3)); // 条件式(単純化) Term::tm_if(t1, t2, t3); // 後者値 Term::TmSucc(Box::new(t1)); // 後者値(単純化) Term::tm_succ(t1); // 前者値 Term::TmPred(Box::new(t1)); // 前者値(単純化) Term::tm_pred(t1); // ゼロ判定 Term::TmIszero(Box::new(t1)); // ゼロ判定(単純化) Term::tm_iszero(t1);
なお、わかっているとは思うが、これらは項の生成時の負担を軽減させるためのものでしかないので、項を生成するだけなら必要はない。ただ、あったほうが圧倒的に楽になることは間違いないだろう。
2.3 「項が値であるか判定するメソッド」の定義
後の評価で必要となってくる「項が値であるか判定するメソッド」の定義を以下に示す。
/// 項が数値であるか判定 fn is_numeric_val(&self) -> bool { match self { Self::TmZero => true, Self::TmSucc(t) => t.is_numeric_val(), _ => false, } } /// 項が値であるか判定 fn is_val(&self) -> bool { match self { Self::TmTrue | Self::TmFalse => true, t => t.is_numeric_val(), } }
Term::is_numeric_val()メソッドが項でいうところのnvの判定に相当し、Term::is_val()メソッドが項でいうところのvの判定に相当する。
なお、ここで注意してほしいのは、Term::is_val()メソッドは実際のところ使わないという点である。これはTaPLではisVal関数といった形で定義されている。それが評価の実装では使わないというだけのことである。よって、Rustでは使っていない関数があるとコンパイル時に警告を出されるので、#[allow(dead_code)]を関数定義の上に付け加える必要があることを付加しておく。
2.4 評価
最後に評価の実装を行う。TaPLのOCamlによる実装では単純にパターンマッチングさせているだけだが、Rustでは手動でボクシングする必要性がある都合上、パターンマッチングだけでなく一工夫必要である*6。そのため、Ocamlの実装よりも少々複雑な実装となっている。それを以下に示す。
/// 構造的操作的意味論による評価 fn eval1(&self) -> Option<Self> { match self { Self::TmIf(t1, t2, t3) => match &**t1 { // E-IfTrue Self::TmTrue => Some((**t2).clone()), // E-IfFalse Self::TmFalse => Some((**t3).clone()), // E-If t1_ => t1_.eval1() .map(|t1__| { Self::tm_if(t1__, (**t2).clone(), (**t3).clone()) }), }, // E-Succ Self::TmSucc(t1) => t1.eval1().map(Self::tm_succ), Self::TmPred(t1) => match &**t1 { // E-PredZero Self::TmZero => Some(Self::TmZero), // E-PredSucc Self::TmSucc(nv1) if nv1.is_numeric_val() => Some((**nv1).clone()), // E-Pred t1_ => t1_.eval1().map(Self::tm_pred), }, Self::TmIszero(t1) => match &**t1 { // E-IszeroZero Self::TmZero => Some(Self::TmTrue), // E-IszeroSucc Self::TmSucc(nv1) if nv1.is_numeric_val() => Some(Self::TmFalse), // E-Iszero t1_ => t1_.eval1().map(Self::tm_iszero), }, // 正規形 _ => None, } } /// 評価 /// 正規形(`None`)になるまで評価を繰り返す fn eval(self) -> Self { if let Some(t) = self.eval1() { t.eval() } else { self } }
構築子Term::TmIfの部分を例に見てほしい。OCamlの実装では以下のように実装されていた。
(** 構造的操作的意味論による評価 *) let rec eval1 t = match t with (* E-IfTrue *) TmIf(TmTrue, t2, _) -> t2 (* E-IfFalse *) | TmIf(TmFalse, _, t3) -> t3 (* E-If *) | TmIf(t1, t2, t3) -> let t1' = eval1 t1 in TmIf(t1', t2, t3) (* 省略 *)
ところがRustではパターンマッチングをさせるときに、部分項がボクシングされていると特定の定数にマッチしてくれない。つまりあくまで部分項の型はBox<Term>型であるので、一度アンボクシング*7をする必要がある。
/// 構造的操作的意味論による評価 fn eval1(&self) -> Option<Self> { match self { Self::TmIf(t1, t2, t3) => match &**t1 { // E-IfTrue Self::TmTrue => Some((**t2).clone()), // E-IfFalse Self::TmFalse => Some((**t3).clone()), // E-If t1_ => t1_.eval1() .map(|t1__| { Self::tm_if(t1__, (**t2).clone(), (**t3).clone()) }), }, /* 省略 */ } }
ちなみに要所要所で2度参照外しを行っているが、これには理由がある。実は構造的操作的意味論による評価の実装では、あまり効率の良い実装が思いつかなかった*8。その関係で、部分項は厳密には&Box<Term>型となっており、これにより所有権のムーブが起こらないようにしている。そのため、参照→Box→部分項といった感じで2度参照外しする必要があるわけである。
またTerm型にCloneトレイトを実装することによって部分項を返すときに値のコピーを行うようにしている。
ほかの構築子も一部Term::is_numeric_val()メソッドを使いガードをしている*9以外は同様である。
そして、今回の実装は構造的操作的意味論によるものなので、1ステップの評価しかされない。そのため、項が正規形となるまで繰り返すメソッドTerm::eval()を定義している。
/// 評価 /// 正規形(`None`)になるまで評価を繰り返す fn eval(self) -> Self { if let Some(t) = self.eval1() { t.eval() } else { self } }
以上で今回の実装について大雑把にではあるが、一通りの解説をした。以下の外部リンクにより、評価を試すことができる。
3. 自然意味論を用いた型なし計算体系の実装
自然意味論とは、「項が最終的に正規形に評価される」ことを定式化した操作的意味論であり、大ステップスタイルとも呼ばれる。構文は構造的操作的意味論と同様であるが、評価規則は以下のようになっている。
以上の評価規則をもとにした実装を以下に示す。
/// 構文 #[derive(Debug, Eq, PartialEq)] enum Term { TmTrue, // 定数真 TmFalse, // 定数偽 TmIf(Box<Term>, Box<Term>, Box<Term>), // 条件式 TmZero, // 定数ゼロ TmSucc(Box<Term>), // 後者値 TmPred(Box<Term>), // 前者値 TmIszero(Box<Term>), // ゼロ判定 } impl Term { /// 条件式の単純化 #[inline] fn tm_if(t1: Self, t2: Self, t3: Self) -> Self { Self::TmIf(Box::new(t1), Box::new(t2), Box::new(t3)) } /// 後者値の単純化 #[inline] fn tm_succ(t1: Self) -> Self { Self::TmSucc(Box::new(t1)) } /// 前者値の単純化 #[inline] fn tm_pred(t1: Self) -> Self { Self::TmPred(Box::new(t1)) } /// ゼロ判定の単純化 #[inline] fn tm_iszero(t1: Self) -> Self { Self::TmIszero(Box::new(t1)) } /// 項が数値であるか判定 fn is_numeric_val(&self) -> bool { match self { Self::TmZero => true, Self::TmSucc(t) => t.is_numeric_val(), _ => false, } } /// 項が値であるか判定 fn is_val(&self) -> bool { match self { Self::TmTrue | Self::TmFalse => true, t => t.is_numeric_val(), } } /// 自然意味論による評価 fn eval(self) -> Self { match self { Self::TmIf(t1, t2, t3) => match t1.eval() { // B-IfTrue Self::TmTrue => t2.eval(), // B-IfFalse Self::TmFalse => t3.eval(), // Stuck t1_ => Self::tm_if(t1_, *t2, *t3), }, // B-Succ Self::TmSucc(t1) => Self::tm_succ(t1.eval()), Self::TmPred(t1) => match t1.eval() { // B-PredZero Self::TmZero => Self::TmZero, // B-PredSucc Self::TmSucc(nv1) if nv1.is_numeric_val() => *nv1, // Stuck t1_ => Self::tm_pred(t1_), }, Self::TmIszero(t1) => match t1.eval() { // B-IszeroZero Self::TmZero => Self::TmTrue, // B-IszeroSucc Self::TmSucc(nv1) if nv1.is_numeric_val() => Self::TmFalse, // Stuck t1_ => Self::tm_iszero(t1_), }, // 正規形 v => v, } } }
この実装では行き詰まり状態となる項も返すようになっている。行き詰まり状態をエラーとしたい場合、実装を一部変更する必要がある点に注意。
またこの実装は、TaPLでは演習問題となっているので、詳細は解説しない。
*1:ただしRustでは循環参照によるメモリリークも「メモリ安全」だと定義している。そのためメモリ関連の問題がすべて解決できるわけではない。しかしそれを除いてRustのメモリ安全性はメモリ関連の問題をほぼクリアしている
*2:リソース確保をオブジェクト生成時に行い、オブジェクト破棄時に自動的に解放するという手法である
*3:ただしリソースを確保し、後に解放するデータ構造を自作しない場合に限る
*4:これ以上評価できない項のことである
*5:ボックス化ともいう
*6:一応RustのバージョンをNightlyにして、Unstable Featureである「box_syntax」を有効にすることでOcamlと同じように単純なパターンマッチングのみで解決した実装も可能となるが、今回はStable Rustのみで実装する
*7:ボクシングを解除すること。ボックス化解除、非ボックス化とも呼ばれる
*8:ちなみに後に紹介する自然意味論による実装では効率の良い実装ができた。これはTaPLでも書かれていたが、どうやら構造的操作的意味論は効率の良い実装が難しいようである
*9:ガードをしている理由は、部分項が数値以外である場合を避けるためである
