解析 conversion check

今天要解析的是 elaboration-zoo 中的一段程式，其中用到了 conversion check 的技術。

1. 型別檢查

這裡列出重要的兩個定義：

environment：儲存變數的計算結果
context：儲存變數的型別

type Env = [(Name, Val)]
type Ctx = [(Name, VTy)]

下面逐步介紹整個型別檢查的元件

1.1. 推導

在最上層的程式中，推導函數會直接被調用來得出 term 的 type，它會適當的調用 check 去檢查是否有型別錯誤

infer :: Env -> Ctx -> Raw -> M VTy
infer env ctx = \case
  SrcPos pos t -> addPos pos (infer env ctx t)
  Var x -> case lookup x ctx of
    Just a -> return a
    Nothing -> report $ "Name not found: " ++ x
  U -> return VU
  t :@ u -> do
    tty <- infer env ctx t
    case tty of
      VPi _ a b -> do
	check env ctx u a
	return $ b $ eval env u
      tty -> report $ "Cannot apply on: " ++ quoteShow env tty
  Lam {} -> report "cannot infer type for lambda expression"
  Pi x a b -> do
    check env ctx a VU
    check ((x, VVar x) : env) ((x, eval env a) : ctx) b VU
    return VU
  Let x a t u -> do
    check env ctx a VU
    let ~a' = eval env a
    check env ctx t a'
    infer ((x, eval env t) : env) ((x, a') : ctx) u

SrcPos 這個情況只需要加上位置訊息之後往下 forward 即可
遇到變數時，查找當前的 context 就可以知道型別了
再來 universe 的 type 就是 universe
application（=t :@ u=）也就是函數套用（\(\beta\)-reduction）的情況就比較複雜了
1. 首先要馬上推導 t 得到 tty
2. 要是 tty 不是一個函數型別（\(\Pi\) type）就 report 錯誤
3. 要是 tty 是 \(\Pi (x : A) \to B\) 就可以檢查 u 是一個 \(A\)
4. 這時把 \(\Pi (x : A) \to B\) 套上 u 就可以得出正確的型別了
lambda 設定成不能推導，避開 undecidable 的情況
對 \(\Pi (x : A) \to B\) 先檢查 \(A\) 是不是型別（\(\mathbb{U}\)），接著擴張 environment 跟 context 再檢查 \(B \; x\) 是不是 \(\mathbb{U}\)
let 語法寫成 =let x : a = t in u=，推導的過程如下
1. 檢查 a 是 \(\mathbb{U}\)
2. 執行 a 得到 a'=，因為要從 =Tm 變成 =Val=（化簡過的 =a=）
3. 檢查 t 是否是 a=，但要用剛剛執行出來的 =a'
4. 把 x : a' 以及 x : t= 分別推進 context 跟 environment 再拿它們去推導 u

最後使用 infer 時，就像是這樣（=…= 是省略號）：

tm <- parse ...
case infer [] [] tm of
  Left err -> ...
  Right ty -> ...

1.2. 檢查

檢查函數接收一個 term 跟一個 type 用來找出 term 實際類型不匹配 type 的情況

check :: Env -> Ctx -> Raw -> VTy -> M ()
check env ctx t a = case (t, a) of
  (SrcPos pos t, _) -> addPos pos (check env ctx t a)
  (Lam x t, VPi (fresh env -> x') a b) ->
    -- after replace x in b
    -- check t : bx
    check ((x, VVar x') : env) ((x, a) : ctx) t (b (VVar x'))
  (Let x a' t' u, _) -> do
    check env ctx a' VU
    let ~a'' = eval env a'
    check env ctx t' a''
    check ((x, eval env t') : env) ((x, a'') : ctx) u a
  _ -> do
    tty <- infer env ctx t
    unless (conv env tty a) $
      report (printf "type mismatch\n\nexpected type:\n\n  %s\n\ninferred type:\n\n  %s\n" (quoteShow env a) (quoteShow env tty))

SrcPos 這個情況只需要加上位置訊息之後往下 forward 即可
要是 term 是 lambda \(\lambda x . t\) 且 type 是 \(\Pi (x' : A) \to B\)
1. 這裡 \(\Pi\) type 用了 view patterns 這個 extension：=fresh env -> x'=
  - 這部份是因為 x 跟 x' 可能是同名的，=fresh= 確保了它們不會被搞混
  - 這個語法的意思是 expression -> pattern
  - pattern 用來 matching
  - expression 在 match 到之後套用到該 pattern 對應的 expression
2. 接著讓環境擴張成 x = x' 跟 x : A
3. 拿新環境檢查 =t=（lambda 的 body）的型別是 \(B \; x\)
  - 檢查 lambda 的方式就是讓 lambda 跟 \(\Pi\) 套用同一個參數之後再看一次
term 是 let 語法時跟推導的情況完全一樣，只差在最後一段是檢查 u 在新環境下是不是 check 拿到的那個 type 而不是去推導 u
除此之外的情況就是調用回去 infer 找出 term 的型別，然後讓它跟 check 拿到的 type 做 conversion check

1.3. 化簡

化簡函數就是把 term 變成 value 的過程，它只需要 environment 而不需要 context

eval :: Env -> Tm -> Val
eval env = \case
  SrcPos _ t -> eval env t
  Var x -> fromJust $ lookup x env
  t' :@ u' -> case (eval env t', eval env u') of
    (VLam _ t, u) -> t u
    (t, u) -> VApp t u
  U -> VU
  Lam x t -> VLam x (\u -> eval ((x, u) : env) t)
  Pi x a b -> VPi x (eval env a) (\u -> eval ((x, u) : env) b)
  Let x _ t u -> eval ((x, eval env t) : env) u

SrcPos 一如既往的只是 forward
變數就是上環境尋找
\(\beta\)-reduction 的情形就是先化簡要操作的兩端，然後看情況
1. 函數那頭是 lambda，就可以當場套用它的 host lambda 得到結果
2. 這個情形比較有趣，有很多名字像是卡住、中性之類的描述，簡單來說就是沒辦法繼續化簡的情況。我們用 VApp 儲存這個結果，conversion check 裡面會講到怎麼處理這些東西
universe 的值還是 universe
lambda 跟 \(\Pi\) 好玩的地方在 host lambda，這個 lambda 定義成 \u -> ...
- 會用 u 去擴展 environment，也就是 (x, u) : env
- 接著用擴展的 environment 執行 =t=（在 \(\Pi\) 的情況就是執行 =b=）
let x : a = t in u 語法就是把 x = t 丟進 environment 去執行 u 而已

卡住在 dependent type 裡非常常見，舉例來說你有個函數
foo : (f : A -> U) -> (a : A) -> f a
在檢查 foo 時執行到 f a 就沒辦法被化簡，因為我們拿到的 f 是一個 VVar "f" 而不是 VLam x t

1.4. Conversion check

conversion 是在 environment 中判斷兩個 value 是否能夠互相轉換的函數

conv :: Env -> Val -> Val -> Bool
conv env m n = case (m, n) of
  (VU, VU) -> True
  (VPi (fresh env -> x) a b, VPi x' a' b') ->
    conv env a a' && conv ((x, VVar x) : env) (b (VVar x)) (b' (VVar x))
  (VLam (fresh env -> x) t, VLam x' t') ->
    conv ((x, VVar x) : env) (t (VVar x)) (t' (VVar x))
  (VLam (fresh env -> x) t, u) ->
    conv ((x, VVar x) : env) (t (VVar x)) (VApp u (VVar x))
  (u, VLam (fresh env -> x) t) ->
    conv ((x, VVar x) : env) (VApp u (VVar x)) (t (VVar x))
  (VVar x, VVar x') -> x == x'
  (VApp t u, VApp t' u') -> conv env t t' && conv env u u'
  _ -> False

兩個 universe 當然可以互相轉換（注意這個語言從頭到尾都沒在管 universe level 的問題）
兩個 \(\Pi(x:A) \to B\) type 的檢查
1. 先看兩個 \(A\) 的部分能不能轉換
2. 再看統一套用一個變數 x 能不能讓兩個 \(B \; x\) 轉換
3. 兩步驟都成功的話，就可以說這兩個 \(\Pi\) type 可以轉換
兩個 lambda 是上面的 \(\Pi\) type 的簡化版，拿掉 \(A\) 的部分就是一樣的
lambda 跟任意 term 或是任意 term 跟 lambda 這兩種情況是對稱的，這時候可以轉換是指：=VApp u (VVar x)= 跟 t (VVar x) 可以轉換，當
1. 擴張 environment 加上 x = VVar x
2. 任意 term 寫成 u
3. host lambda 寫成 t
兩個變數是檢查它們是不是同一個變數
兩個卡住值的情況下，把裡面儲存的值拿出來看能不能轉換
走到這裡就是不能轉換

2. 輔助程式

這裡就不再列出全部的列印（printing）跟解析（parsing）相關程式，主要關注對上面的程式有用途的部分。

2.1. 語言的定義

原始語言的定義如下

type Name = String
type Ty = Tm
type Raw = Tm

data Tm
  = Var Name            -- x
  | Lam Name Tm         -- \x.t
  | Tm :@ Tm            -- t u
  | U                   -- universe
  | Pi Name Ty Ty       -- (x : A) -> B x
  | Let Name Ty Tm Tm   -- let x : A = t; u
  {- helper -}
  | SrcPos SourcePos Tm -- annotate source position
  deriving (Eq)

執行會產出的語言的定義如下，可以看到 lambda 跟 \(\Pi\) 都運用了宿主環境的函數

type VTy = Val

data Val
  = VVar Name
  | VApp Val ~Val
  | VLam Name (Val -> Val)
  | VPi Name Val (Val -> Val)
  | VU

2.2. 避免命名衝突

fresh 用在生成臨時變數時，不會引發命名衝突

fresh :: Env -> Name -> Name
fresh env "_" = "_"
fresh env x = case lookup x env of
  Just _ -> fresh env (x ++ "'")
  _ -> x

2.3. 型別檢查的 monad

型別檢查時，下列的程式定義了檢查時的 monad 跟定位錯誤的工具

type M = Either (String, Maybe SourcePos)

report :: String -> M a
report s = Left (s, Nothing)

addPos :: SourcePos -> M a -> M a
addPos pos ma = case ma of
  Left (msg, Nothing) -> Left (msg, Just pos)
  ma -> ma

2.4. 還原與正規化

這主要就是為了讓執行完的程式印出來的東西可以看

quote :: Env -> Val -> Tm
quote env = \case
  VVar x -> Var x
  VApp t u -> quote env t :@ quote env u
  VLam (fresh env -> x) t -> Lam x $ quote ((x, VVar x) : env) (t (VVar x))
  VPi (fresh env -> x) a b -> Pi x (quote env a) $ quote ((x, VVar x) : env) (b (VVar x))
  VU -> U

nf :: Env -> Tm -> Tm
nf env = quote env . eval env

3. 結論

除了學到 addPos 跟 withPos 的有趣小技巧之外，寫下這篇紀錄也讓我更了解 conversion check 的過程跟各個部件的用途，像是 stuck 的存在跟如何處理，或是 lambda 為什麼不共用 infer 再調用 conv 等等。希望對你也一樣有幫助