interp では動くのに

メモリ工事の段取りが進む間、別の probe が別の負債を測っていた。言語の ad-hoc 多相はコンパイル時 特殊化だ —— show も JSON も構造的な等価も順序も、具体型ごとに derive され、trait システムは無い —— そして正直な問いは、本物の generic コンテナ を建てたとき、それがどこまで持つかだった。probe は pairing heap: type 'a heap、順序は comparator closure、インスタンス化は二つ —— 素の整数と （距離, ノード）のペア —— そして仕上げにその上の Dijkstra。型検査器はそれを受理した。interpreter は 完璧に走らせた。C backend は、存在しない型を参照するコードを emit した。この割れ方 —— interpreter では正しく、バイナリでは壊れる —— は、このプロジェクトが知るもっとも学びの多い失敗だ。 言語の意味と実装が静かに乖離したことを意味し、そしてどこで乖離したかは、正しい形のプログラムだけが 言えるからだ。

一度も宣言されなかった tuple

一つ目の穴は、backend が何を宣言するかの側にあった。C はプログラムが使う全ての tuple 形に struct typedef を要し、その形を集める collector は main 式と全関数のシグネチャを歩いていた —— が、関数の body は決して歩かなかった。自分の引数のペアで match する多相関数 —— match (h1, h2) with …、 二つの heap の merge を書くもっとも自然な形 —— のその tuple 型は、どのシグネチャにも現れない。body の 注釈としてだけ存在し、monomorphize された instance の複製 body の中で初めて具体化する。かくして emit された C は tuple_heap_int_heap_int の一族を、その struct が一度も宣言されないまま使い、 ビルドは C コンパイラで落ちた。修正は正直な一文の長さだった: body も歩け。instance の body は複製 され型解決済みなので、歩けば per-instance の形がそのまま採れる。具体性の guard は多相のままの形を 従来どおり読み飛ばす。

考えを変えられなかった関数

tuple の宣言が通ると、二つ目の、より深い穴が現れた。monomorphizer は多相関数の具体的な使用をスキャン で見つける —— が、スキャン対象は main 式と複数インスタンス関数の body だけだった。自身が単一の型に 解決された関数の内側にある使用は、不可視だった。かくして main でペア型に現れた hp_pop は 「単一解決」された: コンパイラは元の skeleton をその一つの arrow と unify し —— 多相性を破壊し —— 以後のあらゆるインスタンス化は不可能になった。int に解決された drain が body の中から hp_pop を int で呼ぶと、emit された C はペア型の instance を int 型の struct で呼んだ。修理は三部から成った: 全 skeleton の手つかずの複製を、いかなる unification にも触れられる前に保存する。解決済み関数の body を発見スキャンに含める。そして解決済みの関数に二つ目の型が現れたら、手つかずの複製から新しい spec を切り出して多重インスタンスへ昇格する。fixpoint ループは反復の仕方をとうに知っていた。 足りなかったのは、考えを変える許可だけだった。

領収書としての Dijkstra

両方の穴が塞がると、領収書は気持ちよかった: generic heap と、教科書の 6 ノードグラフ上の Dijkstra が native で走り、interpreter とバイト単位で一致し、その例はリポジトリに恒久の回帰テストとして住み着いた。 probe は本来の任務の成果物も届けた —— 型クラス無しの生活の実測だ。heap を書くこと自体は快適。全操作に comparator closure を通すのは、目につくが耐えられる税。本当に不可能なのは、derive された順序を 型変数越しに使うことだ: fn a -> fn b -> a < b は int に固定される。特殊化には特殊化すべき具体型が 要るからだ。これはもう憶測ではなく実測されたコストで、trait question の最初の実データとして設計 キューに座っている。ただしキューに座ったままになった —— 同じ週、型システムが、不便どころではない 何かを許していたのが見つかったからだ。