Как ввести проверки рекурсивных определений с использованием алгоритма W?

Я реализую Алгоритм W (система типа Hindley-Milner) в 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);
    }
}

Немного о типах данных:

Контекст - это объект, который сопоставляет идентификаторы с политипами.
```
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 специализируется на политипе, а функция gen обобщает монотип.

В любом случае, я хочу расширить функцию typecheck, чтобы позволить рекурсивные определения:

Где:

Однако, я застрял с проблемой курицы и яйца. Контекст номер один имеет предположения 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, что вывод типа для рекурсивных полиморфных функций неразрешим. Например, 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 , тогда определение данных Nested становится недействительным, поскольку оно не является индуктивным; и если я не ошибаюсь, то вывод типа индуктивных полиморфных функций действительно разрешима. Если да, то каков алгоритм, используемый для определения типа полиморфных индуктивных функций?

Ответы

Ответ 1

Вы можете ввести проверку, используя явную рекурсию с примитивным fix с типом (a -> a) -> a. Вы можете вставить исправление вручную или автоматически.

Если вы хотите расширить выходы типа, то это тоже очень легко. Когда встречается рекурсивная функция f, просто создайте новую переменную унификации и поместите f с этим типом в среду. После проверки типа тела, объедините тип тела с этой переменной, а затем обобщите, как обычно. Я думаю, это то, что вы предлагаете. Это не позволит вам вывести полиморфную рекурсию, но это вообще неразрешимо.