程式語言為了讓使用者省略不必要的輸入，必須為使用者推導內容，這種需求催生了合一這種類型的演算法。比如很多程式語言允許泛型，比如下面的 OCaml 程式碼

let id (x : 'a) : 'a = x

Elaboration zoo 這個教學專案，它的程式碼要解決的，是一類更複雜的程式語言，叫做 dependent type 的系統中的合一問題，這類系統最重要的特性，就是類型也只是一種值，值也因此可以出現在類型中，但這就比較不是本篇的重點，有興趣的讀者可以閱讀 The Little Typer 來入門。在解釋完它的合一之後，我會介紹它隱式參數的解決方案

Algorithm. 合一演算法的過程 [tt-0007]

假設有程式碼

let id {A : U} (x : A) : A := x
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                 let id2 {B : U} (x : B) : B := id _ x

這裡 id _ x 中的底線表示「省略的引數」，被稱為 hole，我們並沒有明確的給它任何值，比如 B。在展開這個 hole 時，我們用 meta variable ?0 替換它。但 meta variable 必須考慮 contextual variables 的 rigid form，因此進行套用得到 ?0 B x。這引發問題

什麼是 contextual variables？為什麼 contextual variables 是 B 與 x？ [tt-0009]

答案是，這些是 ?0 能看到且實際內容未知的變數，只能用 rigid form 替代

什麼是 rigid form？ [tt-000A]

rigid form 是 dependent type 中即使是 open term 也必須先進行計算而被迫在實作中出現的一種值；由於 meta variable 而被迫出現的值則叫做 flex form

現在我們手上有的 term 是 id (?0 B x) x，現在執行 id (?0 B x)，我們得到型別為

(x : (?0\ B\ \textcolor{red}{x})) \to (?0\ B\ \textcolor{red}{x})

的 term

\lambda x. x

注意到 $(x\ :\ (?0\ B\ \textcolor{red}{x}))$ 中兩個 $x$ 來源不同，不可混用，我用顏色表示它們的 scope 其實不同這件事

現在進入到把這個 term 套用到 x 上的環節了，因此觸發 $x\ :\ B$ 是否是 $?0\ B\ x$ 的 term 的合一計算，我們概念上紀錄成

?0\ B\ x \stackrel{?}{=} B

現在合一演算法必須找出合適的 $?0$ 來滿足等式。我們知道 $?0$ 應該是某種 lambda

\lambda 1. \lambda 2. \fbox{?}

，顯然 $\fbox{?} = 1$ 就會給出我們想要的答案，但這部分要怎麼做到？elaboration zoo 的演算法分成三個階段

Invert [tt-000B]

這裡的重點是，既然 $?0$ 已經套用了 $B$ 與 $x$ ，因此就創立關聯它所創立的 lambda 變數到其 contextual variables 的 map

1 -> B
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                     2 -> x

現在右手邊的 term 只需要看自己的每個 rigid form 有沒有被指向，只要這個 map 裡面查找到有變數是指向 rigid form 自己即反過來創立 rigid form 指向新名字的 map

Rename [tt-000C]

因為我們右手邊的 term 是一個 rigid form $B$ ，因此 map 是

B -> 1

用第二個 map 去改寫右手邊 term $B$ 的內容，這樣我們就得到 $\fbox{?} = 1$

Lambda 化 [tt-000D]

最後進行 abstraction，就得到了

\lambda 1. \lambda 2. 1

安插隱式參數的方法 [tt-0008]

在最開始的程式碼

let id {A : U} (x : A) : A := x
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                 let id2 {B : U} (x : B) : B := id _ x

裡面，其實 {} 中的綁定叫做隱式參數，這表示我們其實也可以用 id x 來調用該函數。但這時候要怎麼知道需要補一個 hole 進去呢？elaboration zoo 作者提出的簡易方案就是區分 implicit $\Pi$ type 與 implicit application，如此一來，當一個 implicit $\Pi$ type 被 explicit apply 的時候，我們就知道要安插 hole 了

以 id x 而言，如果要明確的用 implicit 調用它，就必須寫成 id {B} x，在語法就進行明確的區分。

這時候跳回去看「contextual variables 是 $?0$ 能看到且實際內容未知的變數」就更能了解其理由了，因為已經能明確知道其內容的變數，如

let x = t

x 就是指向 t 的情況，若右手 term 是 x，其實也會是 t 去進行 unify。若右手 term 已經是 rigid form 又可參照，就更不需要成為 contextual variables，因為其 solution 就是把右手 term 原封不動放入，在反轉 map 的時候，只要記得這個 rigid 是非 contextual，就可以為它寫一個 identity mapping。