如何使用算法W鍵入檢查遞歸定義？

Question

我實現Algorithm W（該Hindley-Milner type system）在JavaScript：

它實現了上述規則的功能是typecheck並且其具有以下特徵：

typecheck :: (Context, Expr) -> Monotype 

其被定義爲如下：

function typecheck(context, expression) { 
    switch (expression.type) { 
    case "Var": 
     var name = expression.name; 
     var type = context[name]; 
     return inst(type); 
    case "App": 
     var fun = typecheck(context, expression.fun); 
     var dom = typecheck(context, expression.arg); 
     var cod = new Variable; 
     unify(fun, abs(dom, cod)); 
     return cod; 
    case "Abs": 
     var param = expression.param; 
     var env = Object.create(context); 
     var dom = env[param] = new Variable; 
     var cod = typecheck(env, expression.result); 
     return abs(dom, cod); 
    case "Let": 
     var assignments = expression.assignments; 
     var env = Object.create(context); 

     for (var name in assignments) { 
      var value = assignments[name]; 
      var type = typecheck(context, value); 
      env[name] = gen(context, type); 
     } 

     return typecheck(env, expression.result); 
    } 
} 

A li關於數據類型的一點點：

1. 上下文是一個將標識符映射到多類型的對象。

   type Context = Map String Polytype 
   

2. 的表達式由下面的代數數據類型定義：

   data Expr = Var { name  :: String       } 
         | App { fun   :: Expr,   arg :: Expr } 
         | Abs { param  :: String,   result :: Expr } 
         | Let { assignments :: Map String Expr, result :: Expr } 
         | Rec { assignments :: Map String Expr, result :: Expr } 
   

此外，我們具有由所述算法需要的，但是不能在一個問題必需以下功能：

inst :: Polytype -> Monotype 
abs :: (Monotype, Monotype) -> Monotype 
gen :: (Context, Monotype) -> Polytype 

該inst功能專門化polytype和d gen函數概括了一個monotype。

不管怎樣，我想延長我的typecheck功能允許recursive definitions還有：

其中：

1. 
2. 

但是，我陷入了雞和雞蛋的問題。上下文第一個假設爲v_1 : τ_1, ..., v_n : τ_n。此外，這意味着e_1 : τ_1, ..., e_n : τ_n。因此，您首先需要創建上下文以查找e_1, ..., e_n的類型，但爲了創建上下文，您需要查找e_1, ..., e_n的類型。

你如何解決這個問題？我正在考慮給標識符v_1, ..., v_n分配新的單型變量，然後將每個單型變量與其各自的類型統一起來。這是OCaml爲其let rec綁定使用的方法。然而，這種方法不會產生如由以下OCaml的代碼演示了最普遍的類型：

$ ocaml 
     OCaml version 4.02.1 

# let rec foo x = foo (bar true)  
    and bar x = x;; 
val foo : bool -> 'a = <fun> 
val bar : bool -> bool = <fun> 

但是，GHC並計算出最普遍的類型：

$ ghci 
GHCi, version 7.10.1: http://www.haskell.org/ghc/ :? for help 
Prelude> let foo x = foo (bar True); bar x = x 
Prelude> :t foo 
foo :: Bool -> t 
Prelude> :t bar 
bar :: t -> t 

正如你所看到的，OCaml的推斷類型val bar : bool -> bool而GHC推斷類型bar :: t -> t。Haskell如何推斷最常用的函數bar？

我從@augustss'回答中瞭解到遞歸多態函數的類型推斷是不可判定的。例如，哈斯克爾不能沒有額外的類型註釋推測出以下size函數的類型：

data Nested a = Epsilon | Cons a (Nested [a]) 

size Epsilon  = 0 
size (Cons _ xs) = 1 + size xs 

如果我們指定類型簽名size :: Nested a -> Int然後哈斯克爾接受的方案。但是，如果我們只允許代數數據類型的一個子集inductivetypes，那麼數據定義Nested就會變得無效，因爲它不是歸納的;因此，數據定義Nested是無效的。如果我沒有弄錯，那麼歸納多態函數的類型推斷確實是可以確定的。如果是這樣，那麼用於推斷多態感應函數類型的算法是什麼？

Answer 1

您可以使用顯式遞歸進行檢查，並使用類型爲(a -> a) -> a的原始fix進行檢查。您可以手動或自動插入修補程序。

如果你想擴展類型推斷，那麼這也很容易。當遇到遞歸函數f時，只需生成一個新的統一變量，並將f與這種類型放在環境中。在類型檢查正文後，將正文類型與此變量統一，然後像平常一樣進行概括。我認爲這是你的建議。它不會讓你推斷多態遞歸，但這通常是不可判定的。