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

Question

我在JavaScript中实现Algorithm 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);
    }
}

关于数据类型的一点点:

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函数以允许递归定义:

哪里:

1. 
2. 

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

你怎么解决这个问题？我正在考虑将新的monotype变量分配给标识符v_1, ..., v_n,然后将每个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推断类型,val bar : bool -> bool而GHC推断类型bar :: t -> t.Haskell如何推断出最常见的函数类型bar？

我从@augustss的回答中了解到,递归多态函数的类型推断是不可判定的.例如,size如果没有其他类型注释,Haskell无法推断出以下函数的类型:

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

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

如果我们指定类型签名,size :: Nested a -> Int那么Haskell接受该程序.

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

Answer 1

您可以使用fix带有类型的基元的显式递归来键入它(a -> a) -> a.您可以手动或自动插入修复程序.

如果你想扩展类型推断,那么这也很容易.遇到递归函数f时,只需生成一个新的统一变量,并在环境中放置此类型的f.在对主体进行类型检查后,使用此变量统一主体类型,然后照常进行概括.我想这就是你的建议.它不会允许你推断多态递归,但这通常是不可判定的.