elab の設計

elab パッケージは、項に現れるすべての名前の意味をエラボレーション時に一度だけ確定し、その後シグネチャが変わってもその意味を保つ。このページでは、これが解く問題、実装する二つの判断、そしてカーネルが何かを検査する前に解決しても安全であることを保証する安定性の性質を説明する。

設計目標

ユーザーは名前を書き、カーネルは定数の同一性で動く。その間には、push、add、pop が名前の指すものを変えるスコープ付きシグネチャがある。目標は、ユーザーの知らないところで意味が変わらない解決ステップである。あるスコープで解決された項は、解決された定数をそのまま保つか、失敗するかのどちらかであり、同名のより新しい宣言を黙って拾うことは決してない。

数学的背景

形式仕様は二つの判断を区別している。

名前付きエラボレーション は、名前付きの項 $t$ を、ローカルコンテキスト $\Gamma$ とシグネチャ $\Sigma$ のもとで、解決済みの項 $d$ へ解決する。

\Sigma ; \Gamma \vdash t \Downarrow d

その規則は次のとおりである。 $\Gamma$ で束縛された名前は変数になる。そうでなければ、 $\Sigma$ で可視な名前は、同一性 $\iota$ 、宣言スキーマ $\sigma$ 、出現型 $\tau$ をもつ定数 $c^{\iota}_{\tau \preceq \sigma}$ になる。適用と抽象は成分ごとに解決され、束縛子は $\Gamma$ に追加される。「ローカルが先、次に定数」という順序は固定である。

コア型付け は、名前を引かずに解決済みの項を検査する。

\frac{(x : \tau) \in \Gamma}{\Sigma ; \Gamma \vdash_r x : \tau} \qquad \frac{\Sigma(\iota) = (c, \sigma) \quad \tau \preceq \sigma}{\Sigma ; \Gamma \vdash_r c^{\iota}_{\tau \preceq \sigma} : \tau} \qquad \frac{\Sigma;\Gamma \vdash_r f : \alpha \to \beta \quad \Sigma;\Gamma \vdash_r u : \alpha}{\Sigma;\Gamma \vdash_r f\,u : \beta}

そして抽象の規則は $\Gamma$ を拡張する。定数の規則が読むのは $\Sigma(\iota)$ 、すなわち同一性 $\iota$ をもつ宣言であり、名前 $c$ のもとで現在可視な宣言ではない。実装では、elab_core_type_of の中の検査 id == rc.const_id && schema == rc.schema_ty がこれにあたる。

設計判断

一度だけ解決し、同一性を凍結する

問題。 項が名前を保持し、使うたびに引くとすると、スコープの変更の前後で同じ項が二つの異なる意味をもちうる。

選択肢。 使用のたびに再解決する、カーネル項のみを保持する、同一性付きの解決済み項を保持する。

選択。 RTerm は各定数を、同一性、スキーマ、インスタンス型をもつ ResolvedConst として保持する。コア型付けはこれらを状態と比較し、差異があれば失敗する。

理由。 仕様の「Resolution Freeze under Scope Mutation」定理は、これによって得られる性質を述べている。 $\Sigma; \Gamma \vdash t \Downarrow d$ であり、push、add、pop の列が $\Sigma$ を $\Sigma'$ に変えるとき、 $d$ は変わらず、 $d$ についてのどの判断も、成り立ち続けるか、目に見える形で失敗するかのどちらかである。証明の要点は、 $d$ が遅延された検索ではなく同一性を含んでおり、同一性は決して再利用されないこと（カーネルは単調なカウンタから割り当てる）である。カーネル項のみを保持してもカーネルにとっては機能するが、フロントエンドにはインスタンス化エラーを報告し、ローワリングの前に項を検査するためのスキーマが必要である。

ローカルが定数に先立つ

ローカルは常に同名の定数を隠蔽する。これは通常のレキシカルスコープであり、仕様が定める規則であり、タクティク層が仮定名と定理名について従う規則でもある。elab API の例では、ローカル c が定数 c を隠蔽する様子を示している。

独立したパッケージ

問題。 解決は、その主な利用者であるパーサの中に置くこともできた。

選択。 カーネルとパーサの間にある独立のパッケージとし、カーネルのみに依存させる。

理由。 解決の契約は仕様の一部であり、単独でテストされる。パーサはこれに触れずに文法を変更でき、他のフロントエンドも再利用できる。コードガバナンスの kernel → logic/elab → parser という階層化はこれを記録している。

エラーはデータ、型付けはオプション

解決は Result[_, ElabError] を返し、コア型付けは HolType? を返す。名前引きの失敗には報告する価値のある理由がある（UnknownName、InvalidConstInstance）。一方、型検査の失敗は単一の事実（CoreTypingFailure）であり、その詳細はカーネルがいずれにせよ繰り返すことになる。

正しさと不変条件

健全性は問題にならない。 elab は項を構築するが、定理は構築しない。誤った解決が生み出しうるのは、カーネルが拒否する項か、意図したものとは別の主張についての定理だけである。後者を防ぐのが凍結である。
ローワリングは同一性を保つ。 elab_lower_to_term は $c^{\iota}_{\tau \preceq \sigma}$ を、同一性 $\iota$ をもつカーネル定数 $c{:}\tau$ に写す。そのため、カーネルの許容性検査はユーザーが解決した同一性を見ることになり、その後に定数が隠蔽された定理を拒否する。
ラウンドトリップ。 状態 $\Sigma$ で構築された項 $t$ について、elab_roundtrip_term(Σ', Γ, t) が成功するのは、 $\Sigma'$ で $t$ を再解決して同じ同一性が得られるときであり、かつそのときに限る。したがってスコープのずれを検出できる。
等号は組み込みである。 = は、どの状態でも同一性 -1、スキーマ $\alpha \to \alpha \to \mathit{bool}$ に解決される。宣言することも隠蔽することもできない。

却下した代替案

カーネル時の検索。 名前をカーネルに渡して解決させると、スコープの扱いが信頼基盤に入り込み、定理の意味が使用時の状態に依存してしまう。
グローバルな一意名。 すべての定数名を一意に要求すれば、隠蔽も同一性も不要になるが、仕様のスコープ付きシグネチャは、局所的な開発で名前を再利用できるようにするために存在する。
型推論。 リゾルバは書かれた型を検査するが、束縛子の型を推論したり、文脈から多相定数をインスタンス化したりはしない。

境界

パースは行わない。パーサがテキストを構文に変換し、このパッケージを呼ぶ。
型推論も単一化もない。すべての束縛子の型は明示的であり、定数はインスタンスが要求されない限りスキーマ型で使われる。
オーバーロード、型強制、暗黙の引数、型クラスはない。
定理も権限もない。ローワリングが生成するのはカーネル項のみである。