如何使用W算法来检查递归定义?

I am implementing Algorithm W (the Hindley-Milner type system) in JavaScript:

我正在用JavaScript实现算法W (Hindley-Milner类型系统):

The function which implements the above rules is typecheck and it has the following signature:

实现上述规则的函数为typecheck，具有以下签名:

typecheck :: (Context, Expr) -> Monotype

It is defined as follows:

它的定义如下:

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 little bit about the data types:

关于数据类型:

1. A context is an object which maps identifiers to polytypes.

   上下文是将标识符映射到多类型的对象。

   type Context = Map String Polytype
   

2. An expression is defined by the following algebraic data type:

   表达式由以下代数数据类型定义:

   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 }
   

In addition, we have the following functions which are required by the algorithm but are not essential to the question:

此外，我们还有下列函数，这些函数是算法所需要的，但对这个问题并不重要:

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

The inst function specializes a polytype and the gen function generalizes a monotype.

inst函数专门研究一个多型，gen函数概括一个单型。

Anyway, I want to extend my typecheck function to allow recursive definitions as well:

无论如何，我想扩展我的typecheck函数，以允许递归定义:

Where:

地点:

1. 
2. 

However, I am stuck with a chicken and egg problem. Context number one has the assumptions v_1 : τ_1, ..., v_n : τ_n. Furthermore, it implies e_1 : τ_1, ..., e_n : τ_n. Hence, you first need to create the context in order to find the types of e_1, ..., e_n but in order to create the context you need to find the types of e_1, ..., e_n.

然而，我却被鸡和蛋的问题困住了。上下文第一v_1的假设:τ_1,……v_n:τ_n。此外,这意味着e_1:τ_1,…e_n:τ_n。因此，您首先需要创建上下文来查找e_1的类型，……，e_n，但是为了创建上下文，你需要找到e_1的类型，…,e_n。

How do you solve this problem? I was thinking of assigning new monotype variables to the identifiers v_1, ..., v_n and then unifying each monotype variable with its respective type. This is the method that OCaml uses for its let rec bindings. However, this method does not yield the most general type as is demonstrated by the following OCaml code:

你如何解决这个问题?我想给标识符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>

However, GHC does compute the most general type:

然而，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

As you can see, OCaml infers the type val bar : bool -> bool while GHC infers the type bar :: t -> t. How does Haskell infer the most general type of the function bar?

如您所见，OCaml推断出val bar类型:bool -> bool，而GHC推断出type bar类型::t -> t。

I understand from @augustss' answer that type inference for recursive polymorphic functions is undecidable. For example, Haskell cannot infer the type of the following size function without additional type annotations:

我从@augustss的回答中了解到递归多态函数的类型推断是不可决定的。例如，Haskell不能在没有附加类型注解的情况下推断出以下size函数的类型:

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

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

If we specify the type signature size :: Nested a -> Int then Haskell accepts the program.

如果我们指定类型签名大小::嵌套a -> Int，那么Haskell接受这个程序。

However, if we only allow a subset of algebraic data types, inductive types, then the data definition Nested becomes invalid because it is not inductive; and if I am not mistaken then the type inference of inductive polymorphic functions is indeed decidable. If so, then what is the algorithm used to infer the type of polymorphic inductive functions?

但是，如果我们只允许代数数据类型、归纳类型的子集，那么嵌套的数据定义就会变得无效，因为它不是归纳的;如果我没弄错的话，那么归纳多态函数的类型推断是可以确定的。如果是，那么用于推断多态归纳函数类型的算法是什么?

1 个解决方案

#1

You could type check it using explicit recursion with a primitive fix having type (a -> a) -> a. You can insert the fix by hand or automatically.

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

If you want to extend the type inferences then that's quite easy too. When encountering a recursive function f, just generate a new unification variable and put f with this type in the environment. After type checking the body, unify the body type with this variable and then generalize as usual. I think this is what you suggest. It will not allow you to infer polymorphic recursion, but this in general undecidable.

如果您希望扩展类型推断，那么这也很容易。遇到递归函数f时，只需生成一个新的统一变量，并将f与这种类型放在环境中。检查身体后，用这个变量统一身体类型，然后像往常一样进行推广。我想这就是你的建议。它不允许您推断多态递归，但这通常是不可决定的。