型検査器：Hindley–Milner を Mere で書く

評価器は、プログラムが意味を成すかを気にせず走らせる。型検査器はそれを気にする部品だ —— 1 + "hello" を、途中で失敗する代わりに、走る前に拒むもの。二つのうちセルフホストするのがより難しく、その理由は種類の 違いにある：評価器はただ計算すればよく、木を歩いて値を生むが、型検査器は解かねばならず、言語の まさに中心に座る静かな推論アルゴリズムを走らせる。

評価器が要さなかったアルゴリズム

そのアルゴリズムは Hindley–Milner 推論、最小コアの回で名づけられたのと同じもの —— 型注釈なしで fn x -> x と書け、それが int でも bool でも使えることをコンパイラが自分で導き出す、その機構だ。 型検査器をセルフホストするとは、その機構を Mere で建て直すことで、それはどの HM 実装にも繰り返し現れる いくつかの部品に帰着する。

新しい型変数がある —— まだ知られていない型のプレースホルダで、検査器が即座に確定できないものに 出会うたびに鋳造される。unification がある、その全体の心臓：等しくあらねばならない二つの型 —— 関数が期待するパラメータと、渡された引数 —— を与えられて、進みながら未知を束縛して等しくするか、 和解できなければ失敗する（int 対 str は型 error；関数型対関数型は引数と結果に再帰する）。unification は occurs check で守られる。それは、変数を自分を含む型に束縛するのを拒み、推論が無限型を建てられない ようにする。そして多相を動かす対がある：一般化、推論された型を、本当に自由な未知について量化する ことで再利用可能なスキームに変えるもの、そして instantiation、多相値の各使用に、そのスキームの 自分だけの新しい写しを与えるもの。一般化してから instantiate することこそ、一つの id があらゆる型に 仕えることを可能にする —— let 多相の微妙で、荷重を担う細部であり、静かに間違えるのが最も容易な部分だ。

評価器はこのどれも要さなかった。値を計算するのは直接だ；型を解くのは制約問題で、その解法器を Mere で 表現することは、言語が、自分に型を与えるまさにその機構を明確に述べることだ。

元の大半は scope 外

OCaml 型検査器は千九百行近く、そして評価器と同じく、正直な一手はそのどれだけが self-host を要さない かに気づくことだ。そのおよそ三分の一は前の Part の高度な静的解析 —— 借用検査器、region 追跡、能力と エフェクトの推論、Part II と III の機構だ。もう一片はユーザ体験の磨きだ：綴りを間違えた名前への 「もしかして」提案、error メッセージを親切にする気配り。それらを、当面 scope 外として脇に置くと、残るのは core の Hindley–Milner 推論 —— 七百行ほどの Mere、評価器と同じ桁の規模だ。

その scope 設定はそれ自身、Part IV のカバレッジ台帳の精神で、平然と述べる価値のある決定だ。セルフ ホスト型検査器は、言語の多相関数的な心臓部を検査する；それはまだ、Mere を特徴づける借用モードも、region も、エフェクトシステムも再実装しない。それらは当面 OCaml リファレンスに留まり、そう言うことは、「型 検査器はセルフホストされた」が実際以上を含意するのを許すより正直だ。セルフホストは一度に一層ずつ進み、 この層は古典的なコアだ。

二つの変数を区別せねばならなかった一箇所

小さいが物語る皺が始まりに座る。構文木にはすでに型変数の概念がある —— プログラマが注釈に書く 'a、 パーサが運んでくるもの。だが推論アルゴリズムは自分の種類の変数を要する：解きながら発明する新しい未知、 それはまったく別のものだ。一つはユーザが書いた名前；もう一つは検査器が埋めようとしている穴。それらは 似て見える —— 両方「型変数」だ —— そして混同すればバグになるから、セルフホスト検査器は推論の未知に別の 表現を与えねばならなかった。

これは言語自身の繰り返す本能 —— 一つの名前がこっそり二つの意味を運ぶなら、割る —— が、いま自分自身の 実装の中で表面化したものだ。region と arena を統一し、借用の二軸を分けたのと同じ規律が、ここでは、 両方たまたま型変数と呼ばれ同じでない二つのものに適用される。型検査器を Mere で書くことは、言語の設計が 気にする区別に、言語の設計を強制する検査器の中で、直面することを意味した。

パイプラインが閉じる

どのセルフホスト部品ともそうであるように、型検査器は cross-validate される：それが推論する型は、 プログラムのコーパスの上で OCaml 型検査器が推論する型に対してチェックされ、一致を要求される。そして それが据わって、端から端までのパイプライン全体が Mere に存在する —— パース、型検査、評価 —— 各段が 言語で書かれ、一つの構文木を共有し、それぞれが OCaml リファレンスに保たれる。Wasm にコンパイルされ ブラウザに落とされて、それは三回にわたってデモが向かってきたものになる：Mere プログラムを貼ると、Mere の パイプラインがその型を推論しかつその結果を計算する、完全にセルフホストされて。

名づける価値のあるループの閉じがある。まさに最初の回々は、Mere が確信できるプログラムを最適化し、推論と 明示は戦うのでなく和解するためのものだ —— 大事な型を書き、残りは推論させる —— と論じた。型検査器は、 その和解を現実にする機械であり、それがいま Mere 自身で書かれている。言語にその保証を与える機構が、それが 保証する言語で表現される。

セルフホストの集合からまだコンパイラの一片が欠けている。パイプラインは Mere を読み、検査し、解釈 できる —— だが解釈することはコンパイルすることではない。セルフホストを完全に閉じるには、Mere はコードを 吐けねばならない：検査済みプログラムを取り、マシンが直接走らせる何かを生む。次回：Mere で書かれた コード生成器、そして、言語が自分自身をコンパイルできる瞬間。