如何使用算法W键入检查递归定义？

我正在JavaScript中实现算法W（Hindley-Milner类型系统）：

实现上述规则的函数是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);
    }
}

关于数据类型的一点点：

type Context = Map String Polytype

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， gen函数用于推广monotype。

无论如何，我想延长我的typecheck功能以允许递归定义，以及：

哪里：

但是，我陷入了鸡和鸡蛋的问题。 上下文第一号具有假设v_1 : τ_1, ..., v_n : τ_n 。 此外，它意味着e_1 : τ_1, ..., e_n : τ_n 。 因此，您首先需要创建上下文以查找e_1, ..., e_n的类型e_1, ..., e_n但为了创建上下文，您需要查找e_1, ..., e_n的类型。

你怎么解决这个问题？ 我正在考虑为标识符v_1, ..., v_n分配新的monotype变量，然后将每个monotype变量与其各自的类型统一起来。 这是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推断type 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接受程序。

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

你可以使用类型为(a -> a) -> a的基本fix ，使用显式递归进行类型检查。 您可以手动或自动插入修补程序。

如果你想扩展类型推断，那么这也很容易。 当遇到递归函数f时，只需生成一个新的统一变量，并将f与这种类型放在环境中。 在类型检查正文后，将正文类型与此变量统一，然后像平常一样进行概括。 我认为这是你的建议。 它不会让你推断多态递归，但这通常是不可判定的。

上一篇: How to type check recursive definitions using Algorithm W?

下一篇: How to get better Polymorphic Type Inference in Haskell for this example?