[Paper] Implicit Polarized F
在論文 Implicit Polarized F: local type inference for impredicativity1 中，作者介紹了他們把 System F 放到 call-by-push-value 的計算模型上後，得出了一個 decidable 的 type inference 演算法的結果。
1. 歷史
要明白論文的意義就要先檢討 system F 的歷史，首先 system F 可以定義出 polymorphic 的程式碼，如
let fst : 'a * 'b -> 'a = fun (a, _) -> a
在完全沒有歧義的情況下可以把調用寫成 fst [int] [string] p 來表示 'a ~ int 且 'b ~ string ，但這樣的調用寫法已經到了會干擾正常使用的程度了，所以一般我們希望可以寫成 fst p 。但我們要怎麼描述這個想法？子類型規則正是在描述一個型別可以取代另一個型別的概念，所以我們等同在說子類型規則 \(a \times b \to a \le \text{int} \times \text{string} \to \text{int}\) 成立。只需要引入幾條規則就能定義出這裡需要的 subtyping，然而，其中的 \(\forall L\) 規則引發了問題。
\[ \frac{ \Theta \vdash A \; \text{type} \;\;\; \Theta \vdash [A/\alpha]B \le C }{ \Theta \vdash \forall \alpha. B \le C }{ \;\; \forall L } \]
\(\forall L\) 是 impredicative 的，因為它允許 quantifier 實例化任何型別，包含有 quantifiers 的型別。典型的例子是 id : ∀𝛼 . 𝛼 → 𝛼 ，函數調用 id [∀𝛼 . 𝛼 → 𝛼] id 被認為是 typeable。
2. 相關研究
論文中也提到了數個相關研究
2.1. 直接放棄 impredicativity
這是最常見的辦法，事實上我有很長一段時間也只簡單的認為只能這樣做。在文中提到 GHC 因為 runST 需要 impredicativity，所以特別在其中令 $ 可以被 impredicativity 的解釋。
2.2. Enriching the Type Language
\(ML^F\)2 系統藉由讓型別可以表述 bounded quantification，並且小心的選取語言構造獲得 decidable 的推導演算法，只要求會被用在兩種不同的 polymorphism 上的變數需要特別標記而已。但據說太難實現所以最終未被採用。
2.3. 啟發式演算法
由於觀察到實際上很多程式推導並不困難，啟發式方法在實務上很常使用，其中一個例子是 An Implementation of F<:3 。
3. 主要內容
首先，定義符合 call-by-push-value 的 term，這需要將程式分成兩部分
- values
- computations
舉例來說，data type 構造出來的是 value，而 lambda 則屬於 computation。直覺上的分類方式是用 pattern matching 處理 value，用 application 處理 computation。接著將型別分成兩種：
- values 對應 positive types
- computations 對應 negative types
剩下的就是解釋其宣告式的型別規則，跟要改成演算法需要的幾條修改，最後證明其 typing 跟 subtyping 的 decidability、soundness 跟 completeness。