adapter の設計

設計目標

下流リポジトリは独自の AST（多項式、数値式の木、型付きコア）を持っており、正しい束縛の意味論を得るためにそれらを Term[T] に変換する必要があってはならない。adapter の設計は、そのような AST が @syntax.BindingSyntax を通じて共有アルゴリズムとどう接続するか、実装が何を保証しなければならないか、その保証をどうテストするかを定める。adapter パッケージは参照用の契約テストを持ち、公開 API はない。

数学的背景

ビュー

$N$ を下流の AST とし、

F(X) = 1 + \mathcal{N} + X \times X^{*} + \mathcal{N} \times X

を束縛構文のシグネチャ関手とする。その直和成分は BindingView[X] の Opaque、Variable、Apply、Bind である。adapter は射影（余代数）と構築子（部分代数）からなる。

\pi : N \to F(N) \quad (\texttt{project}), \qquad \kappa : F(N) \setminus 1 \to N \quad (\texttt{variable},\ \texttt{apply},\ \texttt{bind}).

ビュー法則

すべての名前 $x$ 、ノード $h, b, n$ 、配列 $\bar a$ について：

\begin{aligned} \text{(V1)}\quad & \pi(\kappa(\mathsf{Variable}(x))) = \mathsf{Variable}(x), \\ \text{(V2)}\quad & \pi(\kappa(\mathsf{Apply}(h, \bar a))) = \mathsf{Apply}(h, \bar a), \\ \text{(V3)}\quad & \pi(\kappa(\mathsf{Bind}(x, b))) = \mathsf{Bind}(x, b), \\ \text{(V4)}\quad & \pi(n) \ne \mathsf{Opaque} \implies \kappa(\pi(n)) \equiv n, \\ \text{(V5)}\quad & \pi(n) = \mathsf{Opaque} \implies n \text{ contains no variable occurrence}, \\ \text{(V6)}\quad & \pi(n) = \mathsf{Apply}(h, \bar a) \text{ or } \mathsf{Bind}(x, h) \implies h, a_i \text{ are smaller than } n. \end{aligned}

(V1)–(V3) は構築子が射影の報告するものを構築することを述べ、(V4) は射影したノードを再構築すると同値なノードに戻ることを述べる（ $\equiv$ は下流における等価性の概念で、多くの場合 == である）。(V5) は Opaque の「閉じたアトム」契約であり、(V6) は $\pi$ を通じた構造的再帰を停止させる。(V1)–(V4) のもとで、非 opaque ノードに制限した $\pi$ と $\kappa$ は互いに逆であり、したがって opaque ノードを除いた $N$ は $N$ 上の束縛構文 1 層と同型である。

これらの法則で十分な理由

すべての汎用アルゴリズムは $\pi$ を通じた構造的再帰で定義され、 $\kappa$ で再構築する。各アルゴリズムについて、syntax と substitution の設計における Term[T] 上の法則の証明は、Term に関するちょうど 2 つの事実を使う。パターンマッチが構築子を見られること、そして構築子がまさにそのノードを構築することである。(V1)–(V4) はこれらの事実を $N$ について述べる。(V5) は opaque ノードを $\mathrm{FV} = \mathrm{names} = \varnothing$ として扱うことを正当化し、(V6) は整礎帰納法を与える。したがって、法則を満たす adapter について次が成り立つ。

generic_free_variables と generic_all_names は、ノードを束縛構文として読んだときの $\mathrm{FV}$ と $\mathrm{names}$ を計算する。
generic_alpha_rename_bound は alpha ステップを満たす。
GenericSubstitution::apply_once は同時かつ捕獲回避的である（substitution の設計の補題 1–3）。
generic_top_down_once は rewrite の設計の単一簡約基契約と正規形補題を満たす。

設計上の決定

変換ではなくビュートレイト

問題。 下流の AST は Term[T] に変換し、処理してから変換し戻すこともできる。

選択肢。 変換関数、汎用走査ライブラリ（map を持つ関手）、ビュートレイト。

選択。 1 つの射影と 3 つの構築子を持つビュートレイト。変換と異なり、アルゴリズムが再構築するノードだけを割り当て、下流のノード種別を保つ。Apply として射影された和ノードは、適用ではなく和ノードとして再構築される。一般の関手と異なり、MoonBit にはない高カインド型を必要としない。ビューは具体型 BindingView[N] である。

ビューは束縛に必要なものだけを区別する。和・積・冪を持つ下流 AST は 3 つすべてを Apply として射影してよい。その場合、構築子 apply(head, args) は正しい種別を再構築しなければならず、それは種別が head または引数から復元できる場合にのみ可能である。契約テストの和ノードは最も単純な場合で、Apply に相当するノード種別が 1 つだけである。複数の種別を再構築する必要がある場合は、演算子を head に（たとえば opaque な演算子ノードとして）エンコードし、(V4) が成り立つようにする。

Opaque ノードはアトムである

Opaque ノードはそのまま返され、変数が探索されることはない。これは Term[T] における Value(T) と同じ契約であり、任意の型のリテラル（整数、浮動小数点数、有理数）が独自のトレイトなしに参加できるのはこのためである。変数を含むノードを Opaque として射影してはならない（V5）。さもなければ代入はそれらを黙って飛ばしてしまう。

ドメインのポリシーは下流に置く

トレイトが与えるのは束縛構造だけである。標準形、演算子の評価、簡約の順序、不動点反復は、下流パッケージが rewrite を通じて与える規則と戦略であり、基盤はそのいずれも固定しない。これによりライブラリは特定の代数から独立し、各下流パッケージが自身のポリシーを文書化できる。

変数型の橋渡し

下流の変数型は単射（異なる変数を異なる名前へ写す）によって @core.Name に変換される。単射性によって名前の等しさが変数の同一性と一致し、下流の変数について新鮮さと捕獲の検査が正しくなる。

正しさ / 不変条件

契約テスト src/adapter/poly_adapter_wbtest.mbt は、4 種類のノードを持つ AST について法則を満たす adapter を検査する。

性質	検査
同時・1 パスの代入	$x + y$ に $\{x \mapsto y, y \mapsto 2\}$ を適用すると $y + 2$
写されない変数は保たれる	$x + y$ に $\{x \mapsto 3\}$ を適用すると $3 + y$
書き換えは構築子を通じて再構築する	パス `[ApplyArgument(0)]` で $1 + (0 + 2) \to 1 + 2$

下流の adapter は自身のノード種別について (V1)–(V5) のテストを追加すべきである。各構築子の結果を射影し、射影した各ノードを再構築し、opaque ノードが自由変数を持たないことを検査する。

却下した代替案

Term[T] を唯一の AST にする。 下流の AST は Term[T] では表現できない不変条件（正規化された係数、型付きノード）を持つため却下した。
ソートや多重束縛子を持つより大きなビュー。 ケースが増えるとすべての adapter とすべての汎用アルゴリズムが大きくなる。多重束縛子は入れ子の Bind ノードで表現できる。
実行時に法則を検査する。 法則はすべてのノードにわたる等式であり、強制するのではなくテストする。

境界

このトレイトは、スコープが 1 つの子でない束縛子や、異なる子で複数の名前を束縛するノードを表現できない。
法則を満たすことは実装者の責任である。法則を満たさない adapter では汎用アルゴリズムの結果は未定義となる。
adapter パッケージは何もエクスポートせず、契約をテストするだけである。