Правила типизации STLC

Вся система типов STLC — это три правила вывода. Читаем их и превращаем в работающий type checker.

Правило типизации — схема вида «из посылок над чертой следует заключение под чертой»; набор правил полностью определяет, какие термы и каких типов допустимы.

Три правила STLC

Правила записываются дробью: над чертой — что должно выполняться (посылки), под чертой — что мы тогда заключаем. Для STLC их ровно три.

          x : T принадлежит Г
(Var)    ----------------------
              Г |- x : T

         Г, x : A  |- e : B
(Abs)   -----------------------------
         Г |- (\x:A. e) : A -> B

       Г |- f : A -> B      Г |- a : A
(App) -----------------------------------
              Г |- f a : B

Var: если переменная числится в контексте с типом T — она имеет тип T. Abs: если в контексте, расширенном x:A, тело e имеет тип B, то функция имеет тип A -> B. App: если f — функция A -> B, а a имеет тип A, то применение даёт B. Всё. Этих трёх схем достаточно, чтобы типизировать любой терм STLC (плюс правила для базовых литералов, если они есть).

От правил к коду

Правила транслируются в рекурсивную функцию почти дословно: на каждый вид узла — своё правило. Реализуем чекер с явными аннотациями типа на лямбдах (как в чистом STLC по Чёрчу).

def arrow(a, b): return ("->", a, b)
def show(t):
    if isinstance(t, str): return t
    l = show(t[1])
    if isinstance(t[1], tuple): l = "(" + l + ")"
    return l + " -> " + show(t[2])

# термы: var, lam(имя, тип-аргумента, тело), app
def var(n):        return ("var", n)
def lam(p, ty, b): return ("lam", p, ty, b)
def app(f, a):     return ("app", f, a)
# литералы: lit(значение, тип)
def lit(v, ty):    return ("lit", v, ty)

def typecheck(e, gamma):
    if e[0] == "lit":                          # правило для литерала
        return e[2]
    if e[0] == "var":                          # (Var)
        if e[1] not in gamma:
            raise TypeError("несвязанная переменная " + e[1])
        return gamma[e[1]]
    if e[0] == "lam":                          # (Abs)
        ng = dict(gamma); ng[e[1]] = e[2]
        body_t = typecheck(e[3], ng)
        return arrow(e[2], body_t)
    if e[0] == "app":                          # (App)
        ft = typecheck(e[1], gamma)
        at = typecheck(e[2], gamma)
        if not isinstance(ft, tuple):
            raise TypeError("применяется не-функция: " + show(ft))
        if ft[1] != at:
            raise TypeError("ожидался " + show(ft[1]) + ", получен " + show(at))
        return ft[2]

# \x:Int. x   и   её применение к 5
idInt = lam("x", "Int", var("x"))
print("id      :", show(typecheck(idInt, {})))
print("id 5    :", show(typecheck(app(idInt, lit(5, "Int")), {})))
# \f:Int->Int. \x:Int. f (f x)   -- двойное применение
twice = lam("f", arrow("Int","Int"),
          lam("x", "Int",
            app(var("f"), app(var("f"), var("x")))))
print("twice   :", show(typecheck(twice, {})))

Вывод:

id      : Int -> Int
id 5    : Int
twice   : (Int -> Int) -> Int -> Int

Каждая ветка функции — это одно правило вывода. Чекер строит дерево вывода неявно: рекурсия по структуре терма и есть обход дерева вывода снизу вверх.

Как работает под капотом

Заметьте: STLC синтаксически направлен — по виду терма однозначно ясно, какое правило применять (var/lam/app). Поэтому проверка типов детерминирована и линейна по размеру терма: один проход, без поиска и возвратов. Это роскошь простых систем; в более богатых (с подтипами, выводом) приходится искать и решать ограничения — об этом разделы дальше.

Частые ошибки

• Забыть расширить контекст в Abs. Тело проверяется в Γ, x:A; без этого x «не найдётся».
• В App не проверить, что слева именно стрелка. Применение не-функции — отдельная ошибка типов, её надо явно ловить.
• Сравнивать типы по строке, а не по структуре. Для составных типов нужно структурное равенство деревьев.

Итоги

• Вся типизация STLC — три правила: Var, Abs, App (плюс литералы).
• Правила переводятся в рекурсивный чекер «один вид узла — одно правило».
• STLC синтаксически направлен: проверка детерминирована и линейна.
• Рекурсия чекера по структуре терма — это и есть обход дерева вывода.