Типы-функции и контекст типизации

Два кирпича STLC: стрелочный тип для функций и контекст, помнящий типы переменных.

Контекст типизации Γ — конечное отображение свободных переменных в их типы; суждение Γ |- e : T читается «в контексте Γ выражение e имеет тип T».

Стрелочный тип

Главный составной тип STLC — тип функции, записываемый стрелкой. A -> B — тип функций, принимающих аргумент типа A и возвращающих результат типа B. Стрелка правоассоциативна: A -> B -> C значит A -> (B -> C) — функция, которая по A возвращает функцию B -> C. Это согласовано с каррированием: многоместная функция — это вложенные одноместные.

Int -> Int            -- из Int в Int
Int -> Int -> Int      = Int -> (Int -> Int)   -- два аргумента через каррирование
(Int -> Int) -> Int    -- принимает функцию, возвращает Int

Скобки слева от стрелки важны: (Int -> Int) -> Int (функция высшего порядка) и Int -> (Int -> Int) — разные типы.

Контекст типизации

Чтобы узнать тип переменной, нужно где-то хранить «кто какого типа». Это и есть контекст Γ (гамма) — список пар «переменная : тип». Когда мы входим под абстракцию \x : A. e, мы добавляем в контекст пару x : A и проверяем тело e уже в расширенном контексте Γ, x : A.

Г =  y : Int,  f : Int -> Bool

Г |- y        : Int           -- посмотрели в контекст
Г |- f        : Int -> Bool
Г |- f y      : Bool          -- применили f : Int -> Bool к y : Int

Как читать суждение

Запись Γ |- e : T (турникет «|-») — это утверждение «при данных типах свободных переменных из Γ выражение e имеет тип T». Это центральная форма всей теории типов: и проверка, и вывод, и доказательства формулируются как «вывести такое суждение». В следующем уроке мы увидим правила, которые позволяют это суждение строить.

Демонстрация: контекст и проверка переменной/аппликации

Смоделируем контекст словарём и две простейшие проверки: тип переменной (поиск в Γ) и тип аппликации (функция-стрелка плюс совпадение аргумента).

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])

def type_of_var(gamma, x):
    if x not in gamma:
        raise TypeError("переменная " + x + " не в контексте")
    return gamma[x]

def type_of_app(fun_t, arg_t):
    if not isinstance(fun_t, tuple):
        raise TypeError("применяется не-функция: " + show(fun_t))
    if fun_t[1] != arg_t:
        raise TypeError("ожидался " + show(fun_t[1]) + ", получен " + show(arg_t))
    return fun_t[2]

gamma = {"y": "Int", "f": arrow("Int", "Bool")}
print("y      :", show(type_of_var(gamma, "y")))
print("f      :", show(type_of_var(gamma, "f")))
print("f y    :", show(type_of_app(gamma["f"], gamma["y"])))
try:
    type_of_app(gamma["f"], "Bool")    # f ждёт Int, дали Bool
except TypeError as e:
    print("f true :", e)

Вывод:

y      : Int
f      : Int -> Bool
f y    : Bool
f true : ожидался Int, получен Bool

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

Контекст ведёт себя как стек областей видимости: при входе под лямбду в него кладётся новая пара, при выходе она исчезает. Если имя переменной перекрывается (shadowing), новая пара «затеняет» старую — это естественно моделируется добавлением в начало списка или обновлением словаря с восстановлением. Реальные чекеры так и устроены: рекурсивный обход дерева с растущим/сжимающимся контекстом.

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

• Путать ассоциативность стрелки. A -> B -> C — это A -> (B -> C), а не (A -> B) -> C.
• Забывать расширять контекст под лямбдой. Тело \x:A. e проверяется в Γ, x:A, иначе x покажется несвязанной.
• Сравнивать типы «по имени» вместо структуры. Совпадение типов аргумента и параметра — это структурное равенство деревьев типов.

Итоги

• Стрелочный тип A -> B описывает функции; стрелка правоассоциативна.
• Контекст Γ хранит типы свободных переменных; под лямбдой он расширяется.
• Суждение Γ |- e : T — центральная форма теории типов.
• Проверка переменной — поиск в Γ; проверка аппликации — стрелка плюс совпадение аргумента.