新しい言語をさわったらとりあえずラムダ計算のインタプリタを実装するよね! Scalaでふつうにラムダ計算のインタプリタを実装するのはあまりに簡単*1なので, 型レベルでやってみた.
まじめな話をしておくと, C++のテンプレートがチューリング完全なのは有名な話だけど, Scalaではどうなのか気になった. 以前C++のテンプレートでラムダ計算のインタプリタを実装したのと同様のことができるか思考実験してみると, だいたいできそうに思えたのでやってみた.
できたもの
例
import lambda._ case class Equals[A >: B <: B, B]() // 型レベルの同値性チェック用 type S = x ->: y ->: z ->: ( x @@ z @@ (y @@ z) ) type K = x ->: y ->: x type result = ( S @@ K @@ K @@ a ) # ->* Equals[result, a]
構文
a,b, ...,z- 変数
v ->: M- 関数抽象
M @@ N- 関数適用
M# ->- 1ステップβ簡約
M# ->*- 複数ステップ(正規形になるまで)β簡約
本当は->で抽象にしたかったけど最後を:にしないと右結合にできないので妥協. 本当は空白か@で適用にしたいけどできないので妥協. #はtrait内のtypeを参照するための記法で, 基本的に.に相当するものが型レベルでは#になる.
実装方針
基本的にはC++版と同じで, ラムダ項 → De Bruijn Index化 → 簡約 → ラムダ項に戻す, ということをする.
いちおう評価戦略は最左簡約になっているはず. 1ステップは大丈夫で複数ステップの場合は若干あやしい(後述).
チューリング完全性
実装できて, コンパイラを無限ループさせることもできた. やったね, チューリング完全だ!
チューリング完全かどうかだけ知りたいなら実は既にSKIコンビネータのScalaの型レベル実装がある: Scala type level encoding of the SKI calculus | Michid's Weblog
どうでもいいけどIコンビネータはS K Kとβ同値なのでわざわざ定義する必要はないですね. (おそらく, 簡約ステップを減らして現実的な処理速度にするためにはあった方がよい.)
C++版との差異
型引数にプリミティブ型定数を取れない
C++版ではたとえばラムダ計算の変数を, char定数を1つ型引数に取るクラスで表現していて, 変数の同一性はchar定数の同一性に帰着できる. Scalaではそういうことは(僕の知る限りでは)無理なので, 独自に自然数(の必要な部分だけ)を型レベルで定義して, それを型引数としている. けっこうめんどくさいし, たぶんこれのせいで処理速度がすごく遅い.
型引数をパターンマッチできない
C++だとテンプレートの特殊化構文を使って, 型引数に何が入ってきたかに応じて場合分けできるけれど, Scalaにはそういうのは(僕の知る限りでは)ないので, 代わりに親traitに抽象型定義をしておいて, 子traitでそれぞれ別々の実際の型定義を与えるというスタイルになる. これはこれでオブジェクト指向の王道っぽいかんじでわかりやすいけれど, 場合分けを外部化できないので, たとえば項の定義とは独立に評価戦略を外部で与える, ということが難しくなる(ちゃんとやろうとするとvisitorパターンとかにしないといけないはず).
型レベル名前呼びできない(もしくは難しい)
型レベルでいろいろするために, 型レベルBool型とか定義するのだけど, そのBool型による条件分岐は特殊形式ではないので, then節とelse節両方が計算されてしまう. たとえば, 実際に使われている以下のようなコードを考えると,
type subst[t <: Term, l <: Nat] = i# == [l]# ?[Term,
t#inc[i# --, Z],
IndexedVar[i# > [l]# ?[Nat, i# --, i], v]
]
iとlが等しくてもそうでなくても, t#inc[...]とIndexedVar[...]の両方が計算されてしまう(はず). 本来要らない方の結果も計算することになるのですごく遅くなる. 遅くなるだけならまだましで, こういうのを再帰の中で迂闊にやると止まらないコードが容易にできあがってしまう.
ちゃんとやるなら, 「計算」を表す抽象的な型を用意して, その子trait(条件の真偽にあわせて2つ用意する)としてこの手の計算をぜんぶ入れ込んでおいて, 計算する内容がぜんぶ決まったら, # evalとかで一気に計算する(つまり遅延評価を模倣する)とよい. たとえばこれのとくに無限リストのところでは(型レベルの話ではないけれど特殊形式のifが存在しない計算体系で)そういうことをしている.
今回はわかりやすさ重視で速度のためのチューニングはしなかった.
再帰させるのが難しい
C++版では1ステップの簡約を定義した後で, 「簡約できなくなるまで繰り返す」処理として複数ステップ簡約を定義していた. これをScalaでやろうとすると, 直接的に型レベルの再帰的定義が入ってきてしまってillegal cyclic referenceと言って怒られる. 項の定義に埋め込んだ形で定義するしかなさそうだった. なんかすごい頑張ったらやれる方法はあるかもしれないけれど, たぶん読めなくなる. 埋め込んだ形にしたせいで1ステップの定義とは別になってしまったので, 複数ステップ簡約がちゃんと最左簡約になっているかどうか(証明書いたりしていないので)ちょっとあやしい.
型の再帰的定義が難しいという話はここに詳しく書いてある: Type-Level Programming in Scala | Apocalisp
これ何かの役に立つの?
そのまま使うつもりなら良いことはとくになさそう(すごく遅いので). 技術的には型レベルで何かやるときの参考くらいにはなるし, まともにチューニングしてScalaのふつうの型を項に入れて渡したり操作したりできるようにすれば何かの役に立つこともあるかもしれないけれど, 深堀りしていないのでわからない.
追記
Scala 3版も作った.
*1:ケースクラスの公式ドキュメントに途中まで実装が書いてあるレベル
