[PL] 支援 recursion 的直譯器

直譯器中表示閉包（closure）的方式一般是捕捉當前環境（environment）與紀錄函數體的 term 來達成，例如

這裡採用 DBI¹ 形式的 environment

type Env = [Val]

data Clos = Clos Env Exp

data Val
  = Lam Clos
  | ...

而化約規則是把引數插入 environment 之後執行

extend :: Env -> Val -> Env
extend env v = v : env

apply :: Val -> Val -> Val
apply (Lam (Clos env e)) v = eval (extend env v) e

eval :: Env -> Exp -> Val
eval env (App t u) = eval env t `apply` eval env u

這個方式運作良好，也很容易重複使用 Clos 到其他有一樣化約規則的形式上，例如 Pi type ，但是這個方法遇到遞迴定義的時候就會失敗

考慮下面的情況

let rec f : 'a -> 'a =
  fun x -> f x

f 可以這樣檢查：

1. 用 'a -> 'a 檢查 fun x -> f x
2. 在 context 中安插 f : 'a -> 'a
3. 在 environment 中安插 f = fun x -> f x

但要是真的這樣檢查的話，第一步就會失敗，原因是 context 中沒有 f 。於是我們可以反過來做

1. 在 context 中安插 f : 'a -> 'a
2. 用 'a -> 'a 檢查 fun x -> f x
3. 在 environment 中安插 f = fun x -> f x

這樣型別檢查應該就會通過了，但我們需要仔細思考 environment 到底是放了什麼進去。把 lambda 的 term 變成 value 的時候，一般就是把當前 environment 捕捉下來：

eval env (ELam body) = Lam (Clos env body)

因為第三步新的 Lam 需要新的 environment，然而新的 environment 也需要新的 Lam 才能構造出來，這是個不可能完成的死循環。所以上面天真的 eval 沒辦法拿到遞迴的函數自身，執行時應該會發現找不到 f 。在有參考的語言裡面，總是可以用捕獲 ref env 而非 env 來取得一個可能被更新的環境。但這個辦法會讓函數可以存取的範圍變得比預期的更大，而且在沒有這類功能的語言如 Haskell、Lean 等，這個方法是不可行的，所以我們需要不同的辦法來做這件事。

重新思考遞迴到底會發生什麼事，可以發現其實我們只是希望函數的 body 會再次成為 lambda 並可以被套用，於是解決方法也就變得明確了：

1. 在 environment 中安插 f = recur
2. 在 context 中安插 f : 'a -> 'a
3. 用 'a -> 'a 檢查 fun x -> f x
4. 在 environment 中安插 f = fun x -> f x

這時候 f 的 Lam 會捕捉到的 environment 一定有 recur : env 的形式，現在我們說這是「recur-head environment」。在 apply 裡面需要對有 recur-head 的 lambda 做特殊處置，把 recur-head lambda 複製一次再插入 environment 中，接著才插入引數並執行 body。

apply (Lam (Clos (Recur : env) t)) u =
  let lam = Lam (Clos (extend env Recur) t)
   in eval (extend (extend env lam) u) t

這個方法之所以可以運作是因為每次潛在的 recursive point 都會對 environment 進行一次替換，把 Recur 換成能化簡的 lambda，於是自我參考就會拿到合適的 value 而非 stub value。

這裡有個顯著的缺陷是每個頂層定義都會被自動當成可能 recursive 並進行替換，但要是函數其實不是遞迴函數那這個替換就是多餘的，所以也可以多做一層分析確定函數是否有參照自身，或是乾脆給個關鍵字指出函數可不可以遞迴，用不同的模式檢查函數。

另外這個方法對於需要有 stuck application 的語言也很容易通過把 Recur 轉成 Rigid 值來產生合適的 neutral value

stuck application 意思就是不需要計算函數體套用之後的結果，例如 f x 不需要知道 f 的內容，而是產生一個 neutral value 儲存本來的 f x 的形式。這也是因為有時候就是不知道 f 的內容，這個儲存用的 value 通常就叫做 Rigid 。

還有一個常見的辦法是定義 f' ，然後把 f 定義成 f' f' ，但這對有型別的語言來說是否容易成功就有點未知。另外有一個文章談到的 recusive-environment² 似乎跟這裡是類似的作法。