我正在实现 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);
    }
}

一些关于数据类型的知识:

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 函数专门化了一个多类型，gen 函数泛化了一个单类型。

无论如何，我想扩展我的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 绑定(bind)的方法。但是，此方法不会产生最通用的类​​型，如下面的 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 的回答中了解到递归多态函数的类型推断是不可判定的。例如，如果没有额外的类型注释，Haskell 无法推断出以下 size 函数的类型:

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

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

如果我们指定类型签名 size::Nested a -> Int 然后 Haskell 接受程序。

但是，如果我们只允许代数数据类型的一个子集，inductive types ，则数据定义 Nested 变得无效，因为它不是归纳的；如果我没记错的话，归纳多态函数的类型推断确实是可判定的。如果是这样，那么用于推断多态归纳函数类型的算法是什么？

最佳答案

您可以使用具有类型 (a -> a) -> a 的原始 fix 显式递归来对其进行类型检查。您可以手动或自动插入修复程序。

如果您想扩展类型推断，那也很容易。遇到递归函数f，只要生成一个新的统一变量，把这个类型的f放到环境中即可。对主体进行类型检查后，将主体类型与此变量统一，然后照常进行泛化。我想这就是你的建议。它不允许您推断多态递归，但这通常是不可判定的。

关于javascript - 如何使用算法 W 键入检查递归定义？，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/29806121/