またか. またなのか. 何回目だ. ということで, ラムダ計算のインタプリタの実装としては4回目くらい*1, コンパイル時計算でやるものとしても3回目くらいになってしまうけど, ラムダ計算の処理系をまた書いてしまった.
今回の目的は, Scala 3にはmatch typesという機能があり, これだけでチューリング完全なのではないか, というのを検証するため. また, 文字列リテラル型を操作する型レベル関数が3.1.2-RC1にきていて, これを使えば構文解析器だって書ける.
経緯
もともとは, 
id:xuweiさんが文字列リテラル型でコンパイル時に動作する構文解析器を実装していたのが始まり.
ここでは足し引きするくらいの簡単な式の評価器しか実装していないけれど, 割となんでもできてしまいそうに見える.
experimental annotation必要とはいえ、これmatch typeがTuring-completeになった可能性があると思うのだけれど、
— Kenji Yoshida (@xuwei_k) 2022年3月1日
Scala 3は2と違ってtype systemはTuring-completeではないぞ!
というのを意識してたはずだけど、これはいいんですか？
という話題を誰か…
match typesは再帰もできるっぽいので, まぁたぶん普通にチューリング完全になってるなこれは, というのは感覚としてわかっているけど, このときはまだ「ふーん」くらいでスルーしていた.
そうしていたら吉村さんがmatch typesで正規表現エンジンを実装していて,
なんかこれはもう僕がラムダ計算の処理系を書かないといけない流れなのではないか, という感じがしてきた.
過去の事例
Scala 2の型システムはうっかりチューリング完全になっているため, ラムダ計算の評価器も実装可能. 実際にやっている人がいる. 僕です. Scalaを書き始めて1ヶ月だったけど, これでScalaの型システムへの理解が深まった.
ただ, Scala 2だとパターンマッチも特殊形式の条件分岐もなく, 再帰もかなり癖のあるやり方でしかできない*2. 数値リテラル型もないから, ペアノの公理に沿って自分で自然数を定義することになる.
C++だともう少しストレートにできて, パターンマッチと再帰のある関数型言語が型レベルで存在しているような感じになっている. 構文はかなりやりづらいけど. これも実際にやっている人がいる. 僕です.
このときはC++03でやっているので, 最近だときっともっと書きやすいと思う. C++03の場合は以下のような感じだった.
関数と返り値
テンプレートメタプログラミングではテンプレートクラスを関数だと思って使う. そして返り値は
typedefして返す. たとえば任意の型S,Tを受け取って前者を返す関数firstはtemplate<typename S, typename T> struct first { typedef S return_value; };のように書ける. 使う側は
class A {}; class B {}; typedef first<A,B>::return_value a;のようにすることで, 返り値を
aという名前で受け取る.
パターンマッチと再帰呼出し
テンプレートの特殊化構文を使うと, 関数(だと思っているもの)の引数をパターンマッチできる. さらに関数(だと思っているもの)の再帰呼出しもできる.
struct nil {}; template<typename car, typename cdr> struct cons {}; template<typename list> struct length { // デフォルトケース }; template<> struct length<nil> { // 引数の形がnilだったとき static const int return_value = 0; }; template<typename head, typename rest> struct length< cons<head,rest> > { // 引数の形がcons<head,rest>だったとき static const int return_value = length<rest>::return_value + 1; }; length<nil>::return_value; // 0 length<cons<A,cons<B,cons<C,nil> > > >::return_value; // 3 length<A>::return_value; // コンパイルエラー (デフォルトケースではreturn_valueは未定義のため)
Scala 3の型レベル言語
match types
Scala 3のmatch typesはだいたいC++と同じで, しかも構文はだいぶわかりやすい. 上のC++での例をScalaで書くとこうなる.
type First[S, T] = S trait A trait B summon[First[A, B] =:= A] // summon は指定した型の implicit 値を解決するメソッド // =:= は両辺の型が等しいときに implicit 値が得られるような型 // (つまりこれは (等式が成り立つ) <=> (コンパイルが通る) となるような式) import scala.compiletime.ops.int sealed trait List case class Cons[Car, Cdr](car: Car, cdr: Cdr) extends List case class Nil() extends List type Length[L <: List] <: Int = L match { case Nil => 0 case Cons[_, cdr] => int.+[1, Length[cdr]] } trait C summon[Length[Nil] =:= 0] summon[Length[Cons[A, Cons[B, Cons[C, Nil]]]] =:= 3]
めちゃくちゃわかりやすい. もうなんかこういう言語だと思えばこれで生活できる.
リテラル型操作
既に上の例で使ってしまっているけど, scala.compiletime.ops.{boolean, int, string}などで, リテラル型の操作ができる. リテラル型の(型レベルでの)値はそのままリテラルを書けばよいけど, それを操作した結果もリテラル型にするためには, 型レベルの操作ができる必要がある.
import scala.compiletime.ops.string summon[string.+["foo", "bar"] =:= "foobar"]
これがいま3.1.2-RC1では文字列型に関してだいぶリッチになっていて, 正規表現マッチなんかもある(ただし使うときは@annotation.experimentalが必要).
ラムダ計算の実装
基本的には(構文解析器以外は)C++版を翻訳していけばよい. どちらかと言うとScala 3版を書くよりもC++版を読む方がだるい.
評価
まずは項はこういう感じに定義しよう. case classにしてしまって, 値の方で書いても同じものが表現できるようにしておくとなにかとべんりそうなのでそうしておく.
sealed trait Term case class Var[V <: String](v: V) extends Term case class Abs[V <: String, T <: Term](v: V, t: T) extends Term case class App[T1 <: Term, T2 <: Term](t1: T1, t2: T2) extends Term
評価器の実装の仕方はいくつかあるけど, 難しいポイントは変数名がかぶったときの扱い. やり方は何通りかあるけど, C++版と同様にDe Bruijn indexでやっている. 以下はC++版を書いたときの説明.
ラムダ計算では構文上は
λx.λx.xみたいなものも書けて, 最後のxはふつう2番目のxをさしていることにする. 構文上同じ変数による入れ子の抽象を禁止したとしても, たとえば(λxy.x) (λy.y)が簡約されるとλy.λy.yになるので, やっぱり同じ変数で入れ子の抽象をしている場合のことを考えないといけない. さもなければ, すべての変数を違う名前にする必要がある. さらに厄介なことに,λy.(λxy.x y) yの内側を簡約するとλy.(λy.y y)となって, 最後のyは2番目のyをさしていて, 最後から2番目のyは最初のyをさしているはずなのに, 両方とも2番目のyをさしている場合と構文上は区別がつかない.
De Bruijn indexは, そもそも束縛関係を名前で管理するのをやめて, 変数から見ていくつ外側の抽象をさしているかという数値情報を使う. これを使うと
(λxy.x) (λy.y)は(λλ.2) (λ.1)のように表現できる. ただし, 簡約するとき(代入するとき)には数値を適切にシフトしないといけない. たとえばλy.(λxy.x y) yはλ.(λλ.2 1) 1と書けて, これを簡約するには2のところに最後の1を代入すればよいけれど, 結果はλλ.1 1ではなく, 1段階深いところへ代入したのでシフトしてλλ.2 1にしないといけない.
De Bruijn indexで表現された項はあくまで簡約するときの中間表現で, 最後には元の変数名に戻したいから, 実際は名前を完全には消してしまわない方がよい.
つまり, こう
object DeBruijn { sealed trait Term case class Var[I <: Int](i: I) extends Term case class Abs[T <: Term](t: T) extends Term case class App[T1 <: Term, T2 <: Term](t1: T1, t2: T2) extends Term }
ではなく, こう
object DeBruijn { sealed trait Term case class Var[I <: Int, V <: String](i: I, v: V) extends Term case class Abs[V <: String, T <: Term](v: V, t: T) extends Term case class App[T1 <: Term, T2 <: Term](t1: T1, t2: T2) extends Term }
しておいた方がよい.
このDeBruijn.Termの1ステップの簡約は以下のようになる. 基本的には簡約基の場合だけ代入処理をして, それ以外の場合は再帰的に処理するというだけ. いつもの感じですね.
type Eval1[T <: DeBruijn.Term] <: (DeBruijn.Term, Boolean) = T match { case DeBruijn.App[DeBruijn.Abs[v, t1], t2] => // beta-redex (Subst[t1, t2, 1], true) case DeBruijn.App[t1, t2] => Eval1[t1] match { case (_, false) => Eval1[t2] match { case (t3, true) => (DeBruijn.App[t1, t3], true) case (t3, false) => (DeBruijn.App[t1, t3], false) } case (t3, true) => (DeBruijn.App[t3, t2], true) } case DeBruijn.Abs[v, t] => Eval1[t] match { case (t2, true) => (DeBruijn.Abs[v, t2], true) case (t2, false) => (DeBruijn.Abs[v, t2], false) } case _ => (T, false) }
summon[Eval.Eval1[DeBruijn.Of[App[Abs["x", Abs["y", Var["x"]]], Abs["y", Var["y"]]]]] =:= (DeBruijn.Abs["y", DeBruijn.Abs["y", DeBruijn.Var[1, "y"]]], true)]
まぁ実際は代入処理(とそれに伴うインデックスのシフト)がテクいし, みんながハマるところなんだけど, 説明は省略. なんというか, どういう処理をすべきなのかよく考えて注意深く書くだけ. 理解を深めたい人はソースコードを参考に自分で書いてみよう.
印字
テスト時など, 抽象構文木で扱うと面倒なので, 文字列化できるようにしておくとよい. これも文字列リテラル型とその操作が可能だから型レベルでできる. あとは括弧が大量にあると見づらくなるから, 括弧は必要最小限にできるとよい. まぁとにかくコードを見てみよう.
type Show[T <: Term] <: String = T match { case Var[v] => v case Abs[_, _] => string.+["λ", Show.AbsBody[T]] case App[t1, t2] => string.+[Show.AppL[t1], string.+[" ", Show.AppR[t2]]] } object Show { type AbsBody[T <: Term] <: String = T match { case Var[_] => string.+[".", Show[T]] case Abs[v, t] => string.+[v, AbsBody[t]] case App[_, _] => string.+[".", Show[T]] } type AppL[T <: Term] <: String = T match { case Var[_] => Show[T] case Abs[_, _] => string.+["(", string.+[Show[T], ")"]] case App[t1, t2] => Show[T] } type AppR[T <: Term] <: String = T match { case Var[_] => Show[T] case Abs[_, _] => string.+["(", string.+[Show[T], ")"]] case App[_, _] => string.+["(", string.+[Show[T], ")"]] } }
summon[Show[Abs["x", Abs["y", Abs["z", App[App[Var["x"], Var["z"]], App[Var["y"], Var["z"]]]]]]] =:= "λxyz.x z (y z)"]
構文要素ごとに表示関数を分け, それぞれ子要素の形で場合分けすることで必要なパターンだけ括弧をつけるようにできる. なんかこれはもうこうするとすっきり書けると知ってるかどうかの問題.
構文解析
型レベルの構文解析器は初めて書くので, それなりに苦労した. 型レベルだから苦労したというより, 純粋関数型の極小言語で, コンパクトにすっきり, でもなるべく手早くやるにはどうしたらいいかというところ.
括弧を書いても省略してもうまく解析できてほしいし, なんかいかにも面倒くさそうな感じがする. パーサコンビネータとかで書きたい. 勢い余って型レベルのパーサコンビネータを実装しようかと思ったけど, あくまで型レベルの言語として見たときの抽象化能力はそこまで高くなさそうで, かなり大変そうで諦めた. しかし諦めたら割とすんなり書けた.
考え方としては, パーサコンビネータで書くようなつもりでやるが, コンビネータの合成はやらずに手で埋め込んでいく. まずはパーサコンビネータで書きやすそうな形(なんか名前とか理論とかあるような気もするけど, わからんので勘で)のBNFを書こう. トップレベルとなる要素に名前もつけておく. ぱぱっと書いて括弧を省略できない部分はどこかを考えて(印字のときに考えていたのとほぼ同じこと)調整していくとこんな具合のものができる.
// e := λf [ParseExp] // a // f := x.e [ParseAbs] // xf // a := p [ParseApp] // a p // p := x [ParsePrimary] // (e)
パーサコンビネータっぽいなにかを作ろうとしているから, 入力を受け取って, 解析結果と残りの入力を返す関数として定義するとよいはず. 入力は本来は字句解析結果になるけど, 案外文字列そのままにしてしまってコンビネータの中で正規表現マッチとかしてしまった方がお手軽に実装できるみたいな話をどこかで見た記憶があるので今回はそうしてみる. こういうイメージ.
type Parse[S <: String] <: (Term, String)
しかし解析エラーも扱いたいから, 返り値はちゃんと型を定義した方が見通しがよい. するとこうなる.
sealed trait ParseResult case class ParsedTerm[T <: Term, R <: String](term: T, rest: R) extends ParseResult case class ParseError[R <: String](reason: R) extends ParseResult
type Parse[S <: String] <: ParseResult
ということでこれに沿って, BNFで書いた各ルールを実装していけばよい. まずは一番簡単なParsePrimaryから.
type ParsePrimary[Src <: String] <: ParseResult = Matches[SafeSubstring[Src, 0, 1], "[a-z]"] match { case true => ParsedTerm[Var[Substring[Src, 0, 1]], Substring[Src, 1, Length[Src]]] case _ => SafeSubstring[Src, 0, 1] match { case "(" => ParseExp[Substring[Src, 1, Length[Src]]] match { case ParsedTerm[t, rest] => Substring[rest, 0, 1] match { case ")" => ParsedTerm[t, Substring[rest, 1, Length[rest]]] case _ => ParseError["unclosed parenthesis"] } case ParseError[s] => ParseError[s] } case _ => ParseError["variable or parenthesis expected"] } }
変数のみの場合(xの方のパターン)と括弧があるときに場合分けしている. 場合分けしたり1文字読んだりする部分が, パーサコンビネータだったら別々のコンビネータになっていて合成して表現するところだけど, そのまま埋め込んで書いてあるイメージ. 括弧の方の中身はParseExpを相互再帰的に呼び出して読む.
次はParseAppを見てみよう.
type ParseApp[Src <: String] <: ParseResult = ParsePrimary[Src] match { case ParsedTerm[t, rest] => ParseApp1[t, rest] case ParseError[s] => ParseError[s] } type ParseApp1[Prev <: Term, Src <: String] <: ParseResult = SafeSubstring[Src, 0, 1] match { case " " => ParsePrimary[Substring[Src, 1, Length[Src]]] match { case ParsedTerm[t, rest] => ParseApp1[App[Prev, t], rest] case ParseError[s] => ParseError[s] } case _ => ParsedTerm[Prev, Src] }
ルールをよく眺めるとスペース区切りでParsePrimaryをできるだけやればよいとわかる. Appは左結合なので, 1つ前に見たものを引数で受け取るParseApp1を用意して, 次を読む度にAppのインスタンスを作っていくようにする. 区切りのスペースが現れなくなったらすべて読み切ったのでこれまでに作った項をそのまま返せばよい.
最後にParseAbsを見てみよう.
type ParseAbs[Args <: HList, Src <: String] <: ParseResult = Matches[Src, "[a-z][.].*"] match { case true => ParseExp[Substring[Src, 2, Length[Src]]] match { case ParsedTerm[t, rest] => ParsedTerm[MakeAbs[Substring[Src, 0, 1] :+: Args, t], rest] case ParseError[s] => ParseError[s] } case _ => Matches[SafeSubstring[Src, 0, 1], "[a-z]"] match { case true => ParseAbs[Substring[Src, 0, 1] :+: Args, Substring[Src, 1, Length[Src]]] case _ => SafeSubstring[Src, 0, 1] match { case "" => ParseError["unexpected EOF"] case _ => ParseError[string.+["unexpected token: ", Substring[Src, 0, 1]]] } } }
まずx.eの形になっているか調べる(先頭がx.になっているか見る). なっていれば次はeなのでParseExpを呼ぶ.
もう1つのxfの形の場合は, まずxの部分を読んで, 次はfなのでParseAbsを再帰的に呼び出す. 読んだxのところをArgsに積んでいってるのがポイントで, これはあとで1つ目のパターンでMakeAbsに渡して一気にAbsの抽象構文木を組み立てる. Argsには逆順に積まれることになるけど, 内側から作りたい(右結合的になっている)のでむしろ都合がよい.
なんか一般論として, 抽象構文木の組み立ては, 左結合の場合は1つ前のやつを次へ渡して都度やる, 右結合の場合は逆順にリストに溜めていってまとめてやる, という感じでイケるんだろうか??
ここまでできると, 文字列をパースして実行結果を文字列で返すことができるようになる.
type ReadEvalPrint[Src <: String] <: String = Src match { // 無意味な match を挟まないとなんか変にエラーになる case _ => Show[Eval[Parse[Src]]] }
summon[ReadEvalPrint["(λxyz.x z (y z)) (λxy.x) (λxy.x)"] =:= "λz.z"]
型推論 (型検査)
型検査器は評価器とは独立した概念で, 構文解析した結果に対して型を返すものとして実装できる.
summon[Show[Type.Infer[lambda.Parse["(λxyz.x z (y z)) (λxy.x) (λxy.x)"]]] =:= "a -> a"]
どうやって実装するか. これはもう, ちょっと逐次説明するのは大変すぎる(前提となる話だけでも長大な記事になる)から, この辺のを読んでください(とくに4.4と4.5の辺り). だいたいやってることは同じ.
この資料の講義(を五十嵐淳先生がやっていた頃)のTAを昔やっていたから, 型推論器の実装は100万回くらいやっていてハマりどころもわかっているんだけど, それでもデバッグはちょっと大変だった.
いちおう, どういう(型レベル言語上の)値になっているか確認したかったら,
def test: SomeType = ""
とかやれば(見たい型が文字列型だったら適当に= 1とでもする)コンパイルエラーのメッセージでSomeTypeがどうなってるか見えるから, printfデバッグ的なことができなくはない. けどまぁだるい.
ちなみに今回は, Appの式の型を返すところで, フレッシュに割り当てた変数を返すのが正しいところを, 間違って関数適用の左辺の型を返してしまっていて, それに気づくまでに1時間くらいかかったりした.
とはいえ今回の実装は, OCamlとかで書いたものと比較しても, 割とすっきり書けている気がする. 言語機能なんてパターンマッチと再帰呼び出しだけあればそれでよかったんや, という気持ちになってくる.
