System F: полиморфизм, дженерики и теоремы задаром

В https://courses.digitable.life/post/lambda-calculus/09-typed-lambda/ мы построили просто типизированное лямбда-исчисление λ→ и получили за это две теоремы и одну неприятность. Неприятность такая: тождественная функция в λ→ существует только вместе с конкретным типом.

idInt  = λx:Int. x       : Int → Int
idBool = λx:Bool. x      : Bool → Bool
idPair = λx:(Int×Int). x : Int×Int → Int×Int

Три функции с одинаковым телом. Компилятор не имеет права считать их одной: Int → Int и Bool → Bool — разные типы, точка. То же самое с length для списков, со swap для пар, с map, filter и вообще со всем, что не зависит от содержимого.

Программисты знают этот тупик в лицо. Java до версии 5 (2004): List хранит Object, на выходе (String) list.get(0) с приведением типа и ClassCastException в рантайме. Go до 1.18 (2022): либо interface{} с рефлексией, либо кодогенерация, либо три копии функции. Си: макросы и void*. Вопрос, который стоял за всеми этими костылями, ровно один: как дать функции тип «работает для любого A».

Ответ дали дважды и независимо: Жан-Ив Жирар в 1972-м (в диссертации, из соображений математической логики) и Джон Рейнольдс в 1974-м (в статье Towards a theory of type structure, из соображений теории языков программирования). Система называется System F, она же полиморфное лямбда-исчисление второго порядка, она же λ2 из лямбда-куба. И это — теоретический фундамент дженериков во всех языках, которые у вас установлены.

Две новые конструкции

System F добавляет к λ→ ровно два элемента: абстракцию по типу и применение к типу.

типы:  τ ::= α                (типовая переменная)
           | τ → τ            (функция)
           | ∀α. τ            (полиморфный тип — «для любого α»)

термы: M ::= x                (переменная)
           | λx:τ. M          (обычная абстракция — по значению)
           | M M              (обычная аппликация)
           | Λα. M            (типовая абстракция — «параметр-тип»)
           | M [τ]            (типовое применение — подставить конкретный тип)

Большая лямбда Λ (заглавная) связывает типовую переменную, малая λ — обычную. Квадратные скобки в M [τ] — это применение к типу, чтобы визуально отличать его от применения к значению.

Тождественная функция теперь одна на всех:

ID = Λα. λx:α. x        : ∀α. α → α

ID [Int]  = λx:Int. x   : Int → Int
ID [Bool] = λx:Bool. x  : Bool → Bool

Если перевести на языки, которыми вы пользуетесь, всё встаёт на места мгновенно:

const id = <T>(x: T): T => x;   // <T> — это Λ, (x: T) — это λ
id<number>(42);                 // id [Int] 42 — типовое применение явное
id(42);                         // то же самое, тип выведен компилятором

static <T> T id(T x) { return x; }        // <T> перед типом результата — это Λ
String s = Main.<String>id("привет");      // явное типовое применение

fn id<T>(x: T) -> T { x }                 // <T> — Λ, x: T — λ
let a = id::<i32>(42);                    // ::<i32> — это [Int]

Правило вычисления для новой конструкции ровно одно и оно точная копия бета-редукции, только на уровне типов:

(Λα. M) [τ]  →  M[α := τ]        типовая бета-редукция

Подстановка типа в терм — та же механика, что подстановка терма в терм, с той же опасностью захвата имён и тем же лечением альфа-переименованием (https://courses.digitable.life/post/lambda-calculus/02-variables-and-substitution/). Ничего нового, кроме уровня.

Два новых правила типизации

К трём правилам λ→ (VAR, ABS, APP) добавляются два:

        Γ, α ⊢ M : τ                        Γ ⊢ M : ∀α. τ
TABS  ───────────────────           TAPP  ────────────────────
      Γ ⊢ Λα. M : ∀α. τ                   Γ ⊢ M [σ] : τ[α := σ]

TABS: если M типизируется в контексте, где α — просто неизвестный тип (про который ничего нельзя предполагать), то Λα. M имеет тип ∀α. τ. TAPP: если у терма полиморфный тип, его можно инстанцировать любым конкретным типом, подставив его вместо связанной типовой переменной.

Разберём вывод для ID [Bool] true полностью, снизу вверх:

1. x : α ⊢ x : α                                  VAR
2. α ⊢ λx:α. x : α → α                            ABS  (по правилу 1)
3. ⊢ Λα. λx:α. x : ∀α. α → α                      TABS (по правилу 2)
4. ⊢ (Λα. λx:α. x) [Bool] : (α → α)[α := Bool]
                          = Bool → Bool           TAPP (по правилу 3)
5. ⊢ (Λα. λx:α. x) [Bool] true : Bool             APP  (правило 4 + true : Bool)

Обратите внимание на шаг 1: в контексте α — абстрактный тип, о котором ничего не известно. Ни методов, ни конструкторов, ни возможности сравнить. Это ограничение — не досадное упущение, а главный источник силы системы; к нему вернёмся в разделе про параметричность.

Тайпчекер System F на Python

Расширим тайпчекер λ→ из https://courses.digitable.life/post/lambda-calculus/09-typed-lambda/ двумя конструкциями. Типы: ('tvar', 'a'), ('arrow', A, B), ('forall', 'a', T).

def TV(a):     return ('tvar', a)
def Arr(a, b): return ('arrow', a, b)
def All(a, t): return ('forall', a, t)

def show_t(t):
    if t[0] == 'tvar':
        return t[1]
    if t[0] == 'arrow':
        left = show_t(t[1])
        if t[1][0] in ('arrow', 'forall'):
            left = '(' + left + ')'
        return f'{left} -> {show_t(t[2])}'
    return f'∀{t[1]}. {show_t(t[2])}'

def ftv(t):                            # свободные типовые переменные
    if t[0] == 'tvar':
        return {t[1]}
    if t[0] == 'arrow':
        return ftv(t[1]) | ftv(t[2])
    return ftv(t[2]) - {t[1]}

_c = [0]
def fresh(a):
    _c[0] += 1
    return f'{a}{_c[0]}'

def subst_t(t, a, s):
    """t[a := s] — подстановка типа в тип, с защитой от захвата."""
    if t[0] == 'tvar':
        return s if t[1] == a else t
    if t[0] == 'arrow':
        return Arr(subst_t(t[1], a, s), subst_t(t[2], a, s))
    if t[1] == a:                      # ∀a. … — внутренняя a затеняет внешнюю
        return t
    if t[1] in ftv(s):                 # захват: переименовываем связанную
        b = fresh(t[1])
        return All(b, subst_t(subst_t(t[2], t[1], TV(b)), a, s))
    return All(t[1], subst_t(t[2], a, s))

Термы: ('var', x), ('lam', x, T, M), ('app', M, N), ('tlam', a, M), ('tapp', M, T). Вывод типа — пять случаев по числу конструкций:

def V(x):         return ('var', x)
def Lam(x, t, m): return ('lam', x, t, m)
def App(m, n):    return ('app', m, n)
def TLam(a, m):   return ('tlam', a, m)     # Λa. M
def TApp(m, t):   return ('tapp', m, t)     # M [t]

class TypeErr(Exception):
    pass

def infer(term, env=None, tvars=None):
    env, tvars = env or {}, tvars or set()
    kind = term[0]
    if kind == 'var':
        if term[1] not in env:
            raise TypeErr(f'свободная переменная {term[1]}')
        return env[term[1]]
    if kind == 'lam':                              # ABS
        x, tx, body = term[1], term[2], term[3]
        unknown = ftv(tx) - tvars
        if unknown:
            raise TypeErr(f'неизвестная типовая переменная {sorted(unknown)}')
        return Arr(tx, infer(body, {**env, x: tx}, tvars))
    if kind == 'app':                              # APP
        tf, ta = infer(term[1], env, tvars), infer(term[2], env, tvars)
        if tf[0] != 'arrow':
            raise TypeErr(f'применяем не функцию, а значение типа {show_t(tf)}')
        if tf[1] != ta:
            raise TypeErr(f'ожидался аргумент {show_t(tf[1])}, получен {show_t(ta)}')
        return tf[2]
    if kind == 'tlam':                             # TABS: Λa. M : ∀a. T
        return All(term[1], infer(term[2], env, tvars | {term[1]}))
    if kind == 'tapp':                             # TAPP: M [S] : T[a := S]
        tm = infer(term[1], env, tvars)
        if tm[0] != 'forall':
            raise TypeErr(f'типовое применение к неполиморфному {show_t(tm)}')
        return subst_t(tm[2], tm[1], term[2])
    raise TypeErr(f'неизвестный терм {term}')

Проверка tvars в случае lam — не формальность: она ловит попытку написать λx:α. x там, где α нигде не связана. Без неё тайпчекер молча принимал бы бессмысленные термы.

Сложность. Один обход терма, O(n) вызовов; каждая подстановка типа — O(размер типа). Проверка типов в System F дешёвая. Дорог, как увидим ниже, вывод типов — настолько, что его вообще нет.

Числа Чёрча наконец получают честный тип

Помните проблему из https://courses.digitable.life/post/lambda-calculus/09-typed-lambda/: в λ→ число Чёрча λf. λx. f (f x) можно типизировать только для одного конкретного α, и «два для Int» с «двумя для String» — разные значения. В System F числа становятся одним полиморфным термом:

Nat = ∀α. (α → α) → α → α

TWO  = Λα. λf:α→α. λx:α. f (f x)                                     : Nat
SUCC = λn:Nat. Λα. λf:α→α. λx:α. f (n [α] f x)                       : Nat → Nat
PLUS = λn:Nat. λm:Nat. Λα. λf:α→α. λx:α. n [α] f (m [α] f x)         : Nat → Nat → Nat

Прогоняем через тайпчекер:

Λa. λx:a. x                        : ∀a. a -> a
two = Λa. λf:a->a. λx:a. f (f x)   : ∀a. (a -> a) -> a -> a
SUCC                               : (∀a. (a -> a) -> a -> a) -> ∀a. (a -> a) -> a -> a
SUCC two                           : ∀a. (a -> a) -> a -> a
PLUS two two                       : ∀a. (a -> a) -> a -> a

Всё сходится: SUCC two снова Nat. Обратите внимание на n [α] f x в определении SUCC — прежде чем применить число к функции, его надо инстанцировать типом. В System F типовое применение пишется руками; в реальном языке компилятор проставляет его сам, и именно поэтому вы не видите [α] в своём коде.

То же самое работает для любой структуры данных: пара кодируется как ∀ρ. (α → β → ρ) → ρ, список — как своя собственная свёртка. Это кодирование Бёма-Берардуччи, о котором шла речь в https://courses.digitable.life/post/lambda-calculus/06-pairs-and-lists/: в бестиповом исчислении оно было трюком, в System F оно типизируется и становится теоремой — любой алгебраический тип данных представим как полиморфный тип его свёртки.

PAIR = TLam('A', TLam('B', Lam('x', TV('A'), Lam('y', TV('B'),
        TLam('r', Lam('f', Arr(TV('A'), Arr(TV('B'), TV('r'))),
             App(App(V('f'), V('x')), V('y'))))))))
# PAIR : ∀A. ∀B. A -> B -> ∀r. (A -> B -> r) -> r

Что мы приобрели и чем заплатили

Приобрели — выразительность. System F сильно нормализуема (Жирар, 1972): любой терм завершается, Y и Ω по-прежнему невыразимы (https://courses.digitable.life/post/lambda-calculus/07-recursion-and-y/). Но при этом класс представимых функций гигантский: это в точности функции, тотальность которых доказуема в арифметике второго порядка. Проще говоря — всё, что вы когда-либо напишете и сможете доказать, что оно завершается. Для сравнения: в λ→ представимы только элементарные расширенные полиномы. Разница — как между калькулятором и языком программирования.

Заплатили — выводимостью типов. Вот терм, который в λ→ невозможен, а в System F типизируется:

SELF = Lam('x', All('a', Arr(TV('a'), TV('a'))),
           App(TApp(V('x'), All('a', Arr(TV('a'), TV('a')))), V('x')))
# λx:∀a.a->a. x [∀a.a->a] x   :   (∀a. a -> a) -> ∀a. a -> a

Это самоприменение — то самое x x, которое ломало λ→. Здесь оно проходит: мы инстанцируем полиморфный x типом ∀a. a → a и применяем к самому себе. Возможность подставлять вместо α типы, содержащие ∀ (включая тот же самый), называется импредикативностью, и именно она делает систему такой сильной — и такой недружелюбной к выводу типов.

Дж. Б. Уэллс в 1994 году доказал: вывод типов в System F неразрешим. Не «медленный», не «экспоненциальный» — алгоритма не существует (Typability and type checking in System F are equivalent and undecidable, APAL, 1999). Значит, язык с полноценным System F обязан требовать аннотации от программиста.

Хиндли-Милнер: полезный кусок System F

Реальные языки берут не всю систему, а фрагмент, в котором вывод остаётся разрешимым. Ограничение называется ранг 1 (или префиксный полиморфизм): все кванторы ∀ стоят снаружи, слева, и никогда — в позиции аргумента функции.

∀α. α → α                          ранг 1 — можно вывести автоматически
∀α. (α → α) → Int                  тоже ранг 1
(∀α. α → α) → Int                  ранг 2 — квантор слева от стрелки, нужны аннотации

Разница ровно в том, кто выбирает тип. В ранге 1 тип выбирает вызывающий: он инстанцирует ∀ в момент вызова. В ранге 2 функция получает аргумент, который сама должна инстанцировать разными типами — а значит, вызывающий обязан передать по-настоящему полиморфное значение, и вывести это невозможно.

Система с рангом 1 плюс обобщение в let — это Хиндли-Милнер, основа ML, OCaml, Haskell, Elm, F# и (в упрощённом виде) вывода типов почти везде. Алгоритм W и унификация подробно разобраны в https://courses.digitable.life/post/compilers/05-type-checking/; здесь важно другое — где у HM границы, потому что в них вы упираетесь на практике.

Граница 1: обобщение только в let. Классика, которую видел каждый, кто трогал Haskell или OCaml:

-- работает: id обобщается при связывании, потом инстанцируется дважды
ok = let f = \x -> x in (f 1, f "строка")

-- не работает: параметр лямбды монотипен, ранг 2 не выводится
bad = (\f -> (f 1, f "строка")) (\x -> x)

Первый вариант компилируется, второй — нет, хотя вычисляет то же самое. Чтобы заработал второй, нужен явный ранг 2 и расширение языка:

{-# LANGUAGE RankNTypes #-}
good :: (forall a. a -> a) -> (Int, String)
good f = (f 1, f "строка")     -- теперь f честно полиморфна внутри тела

TypeScript умеет то же самое и синтаксически даже симпатичнее — тип параметра может быть полиморфной функцией:

// ранг 2: f полиморфна ВНУТРИ функции, а не инстанцируется на входе
function pairUp(f: <T>(x: T) => T): [number, string] {
  return [f(1), f("строка")];
}
pairUp(x => x);   // ok

Граница 2: value restriction. Если разрешить обобщать что попало, система типов ломается. Каноническая дыра из ранней истории ML:

(* если бы r получил тип ∀a. a list ref … *)
let r = ref []          (* ∀a. a list ref  — ОПАСНО *)
r := [1];               (* инстанцируем a := int *)
List.hd !r ^ "строка"   (* инстанцируем a := string — и падаем в рантайме *)

Лечение (Эндрю Райт, 1995): обобщать только синтаксические значения — лямбды, константы, конструкторы, — но не результаты вызовов. Отсюда правило OCaml/SML про «слабые типовые переменные» ('_weak1), которое регулярно ставит новичков в тупик; теперь понятно, что оно охраняет.

Граница 3: у Хиндли-Милнера тоже есть худший случай. Вывод типов в HM DEXPTIME-полон: тип может расти экспоненциально по размеру выражения. На практике вы видите это как «TypeScript думает 40 секунд на одном выражении» (https://courses.digitable.life/post/typescript/12-migration-and-compiler-performance/).

Параметричность: теоремы задаром

Теперь — самая практичная часть. Вернёмся к наблюдению из вывода типов: в теле Λα. … о типе α ничего не известно. Нельзя проверить, что это, нельзя сравнить два значения, нельзя создать значение из воздуха. Единственное, что можно, — перекладывать полученные значения с места на место.

Рейнольдс формализовал это в 1983-м как параметричность: полиморфная функция обязана вести себя «одинаково» на всех типах, причём «одинаково» формулируется через отношения. Уодлер в 1989-м перевёл это на язык, понятный программисту, в статье с говорящим названием Theorems for Free!: из одной только сигнатуры механически выводится теорема о поведении.

Пример 1. f : ∀α. α → α — это обязательно тождество.

Параметричность даёт: для любых типов A, B, любой функции g : A → B и любого x : A верно

f_B (g x) = g (f_A x)

Возьмём A = Unit (тип с единственным значением ()), x = (), а g : Unit → B пусть возвращает произвольное b. Тогда:

f_B b = f_B (g ()) = g (f_Unit ()) = g () = b

f_B b = b для произвольных B и b. Значит, f — тождество, и других реализаций не существует. Мы это доказали, ни разу не заглянув в код функции.

Пример 2. f : ∀α. [α] → [α] коммутирует с map.

map g (f xs) = f (map g xs)      для любой g

Практический смысл: такая функция может переставлять, дублировать и выбрасывать элементы — но только по позиции, не глядя на значения. reverse, tail, take 3 — да. «Отсортировать» — нет: для сортировки нужно сравнивать элементы, а значит, нужен дополнительный аргумент-компаратор или ограничение Ord a. Именно поэтому в Haskell тип sort :: Ord a => [a] -> [a], а не [a] -> [a]: словарь Ord — это как раз то, что возвращает функции право смотреть на элементы.

Пример 3. Сколько всего обитателей у типа?

Число обитателей типа — это число различных доказательств соответствующего утверждения (https://courses.digitable.life/post/lambda-calculus/09-typed-lambda/). Практически это лучший инструмент проектирования API из всех, что даёт теория типов: чем полиморфнее сигнатура, тем меньше у функции возможностей соврать. Если ваша функция принимает <T>(items: T[]) => T[], читателю не нужно проверять, не логирует ли она содержимое, — она физически не может его прочитать.

Где параметричность ломается

Она держится ровно до тех пор, пока язык честен. Каждое из перечисленного пробивает в ней дыру:

• Рефлексия и проверки типа в рантайме. instanceof в Java, reflect.TypeOf в Go, typeof x === "string" внутри дженерика в TypeScript. Функция начинает смотреть на тип — теорема «задаром» больше не действует.
• Приведения типов. unsafeCoerce в Haskell, as any в TypeScript, unsafe в Rust.
• Незавершаемость и исключения. Функция типа ∀α. α → α может не вернуть ничего вовсе, зациклившись или бросив исключение. В Haskell это учитывают отдельной оговоркой (⊥ — bottom); статья Fast and Loose Reasoning is Morally Correct (Danielsson et al., POPL 2006) объясняет, почему рассуждать «как будто ⊥ нет» всё-таки допустимо.
• Побочные эффекты. Функция <T>(x: T) => T в JavaScript может записать x в глобальную переменную, отправить в сеть и подождать. Тип этого не запрещает.

Полезное правило: параметричность — это не «свойство сигнатуры», а «свойство сигнатуры в честном языке». В Haskell на неё можно опираться при рефакторинге, в TypeScript — только как на сильную эвристику.

Три судьбы большой лямбды

Осталась самая инженерная часть: Λα — конструкция уровня типов, а процессору типы не нужны. Что делать с типовой абстракцией при компиляции? Есть ровно три ответа, и все три реализованы в промышленных языках.

Стирание (type erasure). Λα и M [τ] просто выбрасываются: раз параметричность гарантирует, что программа не может ничего узнать о типе, хранить его незачем. Так делают Java, TypeScript, Haskell, OCaml. Цена — типа нет в рантайме: new T[] в Java невозможен, List<String> и List<Integer> в рантайме один и тот же класс (https://courses.digitable.life/post/java/04-collections-and-generics/).

Мономорфизация. Λα вычисляется на этапе компиляции: для каждого использованного типа генерируется своя копия кода. Так делают Rust (https://courses.digitable.life/post/rust/05-types-and-traits/) и шаблоны C++. Цена — время компиляции и размер бинарника; выигрыш — отсутствие косвенных вызовов и полная свобода инлайнинга.

Реификация. Λα остаётся честным вызовом в рантайме: тип передаётся как значение. Так делает .NET (https://courses.digitable.life/post/csharp/09-types-and-abstractions/): List<int> и List<string> — разные типы во время выполнения, typeof(T) работает, JIT специализирует код по значимым типам. Цена — параметричность больше не гарантирована: имея typeof(T), функция может ветвиться по типу.

Go в версии 1.18 выбрал гибрид — стенсилинг по GC-форме: одна копия кода на каждую «форму представления» (все указатели делят одну копию, каждый значимый тип получает свою), плюс словарь с метаданными, передаваемый неявным аргументом. Это буквально попытка усидеть на двух стульях между стиранием и мономорфизацией (https://courses.digitable.life/post/golang/10-generics-and-iterators/).

∃ вместо ∀: интерфейсы — это тоже полиморфизм

У квантора «для любого» есть двойник — «существует». Экзистенциальный тип ∃α. τ читается как «есть какой-то тип α, и значение типа τ, но какой именно α — снаружи не видно».

В System F отдельная конструкция не нужна: ∃ кодируется через ∀ (двойственность, как у де Моргана в логике):

∃α. τ   =   ∀ρ. (∀α. (τ → ρ)) → ρ

Читается так: «дай мне функцию, которая умеет работать с любым α, — и я применю её к своему спрятанному типу и верну результат». Единственный способ что-то сделать с экзистенциальным значением — передать полиморфного потребителя. Митчелл и Плоткин показали в Abstract Types Have Existential Type (1988), что это в точности семантика абстрактных типов данных и модулей.

А в вашем коде это выглядит так:

// ∀: вызывающий выбирает тип
function first<T>(xs: T[]): T { return xs[0]; }

// ∃: реализация выбирает тип, вызывающий видит только интерфейс
interface Counter { inc(): void; value(): number; }
function makeCounter(): Counter {          // внутри может быть number, может — BigInt
  let n = 0;
  return { inc: () => { n += 1; }, value: () => n };
}

Интерфейс в Java и Go, dyn Trait в Rust, модуль в OCaml, объект с приватным полем в JavaScript — всё это экзистенциальные типы. Отсюда полезная формулировка разницы: дженерик — это «тип выбирает вызывающий», интерфейс — это «тип выбирает реализация». Стоит один раз это увидеть, и вопрос «дженерик или интерфейс» перестаёт быть делом вкуса.

Типичные ошибки и заблуждения

«Дженерики — это шаблоны C++». Разные вещи. Дженерик проверяется на типы один раз, при объявлении, — поэтому ошибка в теле дженерика ловится сразу. Шаблон C++ проверяется при инстанцировании, поэтому и знаменитые километровые ошибки. System F описывает первое; второе — это скорее макросы с типизацией постфактум.

«<T> — это как Object, только красивее». Наоборот. Object разрешает узнать тип и привести его; T запрещает. Именно запрет и даёт параметричность, а вместе с ней — гарантии.

«Раз стирание, значит дженерики — это косметика». Косметика на уровне рантайма, теорема на уровне компиляции. Стирание корректно потому что параметричность: программа не может зависеть от того, чего ей не разрешено узнать.

«В System F можно вывести любой тип, просто компиляторы ленятся». Вывод в System F неразрешим (Уэллс, 1994). Требование аннотаций к RankNTypes — не лень, а следствие теоремы.

«Полиморфизм подтипов (наследование) и параметрический полиморфизм — одно и то же». Нет: <T extends Animal> — это ограниченная квантификация (System F<:), и параметричность в ней ослаблена: зная границу, функция уже кое-что умеет с T. Чем сильнее ограничение — тем больше возможностей и тем меньше гарантий.

«Если функция полиморфна, она точно не делает ничего лишнего». Только в честном языке. В JavaScript, Java или Go полиморфная сигнатура — сильный намёк, а не доказательство: рефлексия, эффекты и исключения никуда не делись.

Упражнения

1. Выведите тип терма Λα. Λβ. λx:α. λy:β. x. Какому логическому утверждению он соответствует?
2. Что вернёт ID [∀α. α → α] ID? Выпишите тип и объясните, почему в λ→ это невозможно.
3. Напишите в System F функцию COMPOSE : ∀α.∀β.∀γ. (β → γ) → (α → β) → α → γ и выведите её тип по правилам.
4. Сколько существует тотальных функций типа ∀α.∀β. (α → β) → α → β? А типа ∀α. (α → α) → α → α?
5. Почему map :: ∀α.∀β. (α → β) → [α] → [β] не может изменить длину списка? Сформулируйте свободную теорему.
6. Дан тип (∀α. α → α) → Int. Какого он ранга и почему его нельзя вывести автоматически?
7. Java-код ниже не компилируется. Какая из трёх стратегий компиляции дженериков это объясняет и как обойти?

static <T> T[] makeArray(int n) {
    return new T[n];      // ошибка компиляции
}

Ответы

1. Тип ∀α. ∀β. α → β → α. Вывод: x : α в контексте с обеими типовыми переменными, ABS дважды даёт α → β → α, затем TABS дважды навешивает кванторы. Это комбинатор K (https://courses.digitable.life/post/lambda-calculus/11-combinatory-logic/), а логически — «из A следует, что из B следует A», первая аксиома импликационного фрагмента.

2. ID [∀α. α → α] имеет тип (∀α. α → α) → (∀α. α → α), применяем к ID — получаем ID обратно, тип ∀α. α → α. В λ→ это невозможно, потому что там нет типа ∀α. α → α: тождество существует только для конкретного типа, а инстанцировать «самим собой» нечего. Это тот самый импредикативный шаг, из-за которого вывод типов становится неразрешимым.

3.

COMPOSE = Λα. Λβ. Λγ. λf:(β→γ). λg:(α→β). λx:α. f (g x)

Вывод снизу вверх: x : α, g x : β по APP, f (g x) : γ по APP, три раза ABS дают (β→γ) → (α→β) → α → γ, три раза TABS навешивают кванторы. Это комбинатор B из https://courses.digitable.life/post/lambda-calculus/11-combinatory-logic/, он же (.) в Haskell.

4. Для ∀α.∀β. (α → β) → α → β — ровно одна: Λα.Λβ.λf.λx. f x. Ничего другого сделать нельзя: значение типа β можно получить только применением f, а значение типа α есть только одно. Для ∀α. (α → α) → α → α — счётно много: f можно применить n раз при любом n ≥ 0. Это ровно числа Чёрча, и тип Nat их и описывает.

5. Свободная теорема для map: для любых g : α → α', h : β → β' и f : α → β, если h ∘ f = f' ∘ g, то map h ∘ map f = map f' ∘ map g. Проще говоря, map обязана применить функцию к каждому элементу, сохранив позиции: она не знает про элементы ничего и не может решить, что какой-то из них нужно выбросить, ведь критерия у неё нет. Длина результата определена типом, а не кодом.

6. Ранг 2: квантор ∀ стоит слева от стрелки, в позиции аргумента. Вывести нельзя, потому что вызывающий обязан передать функцию, полиморфную внутри тела — а вывод типов ранга 1 умеет только инстанцировать ∀ на границе вызова. В Haskell понадобится {-# LANGUAGE RankNTypes #-} и явная сигнатура, в TypeScript — явный тип параметра f: <T>(x: T) => T.

7. Это следствие стирания: в рантайме T не существует, а new T[n] требует знать тип элементов в момент создания массива (JVM хранит его в заголовке). Обходы: передать Class<T> явно и звать Array.newInstance(cls, n) (то есть вручную реифицировать тип) или работать с List<T>, где стирание не мешает. В C# с реификацией new T[n] компилируется без проблем — ровно потому, что там Λ дожила до рантайма.

Мини-итог

• System F добавляет к типизированному лямбда-исчислению две конструкции: типовую абстракцию Λα. M и типовое применение M [τ], а к типам — квантор ∀α. τ.
• Дженерики в Java, C#, Rust, Go, TypeScript, Haskell и Scala — это System F с разной степенью ограничений и разными стратегиями компиляции.
• Система сильно нормализуема и при этом чудовищно выразительна; числа Чёрча и любые алгебраические типы получают в ней честные полиморфные типы (кодирование Бёма-Берардуччи).
• Вывод типов в полной System F неразрешим (Уэллс, 1994), поэтому языки берут фрагмент ранга 1 — Хиндли-Милнер, — а за ранг 2 и выше просят аннотации.
• Параметричность: полиморфная функция ничего не может узнать о типе, поэтому из сигнатуры выводятся теоремы о поведении. ∀α. α → α — обязательно тождество, и это доказывается без чтения кода.
• Параметричность ломают рефлексия, приведения типов, эффекты и незавершаемость — то есть в честном языке это гарантия, а в мейнстримном — сильная эвристика.
• Λα при компиляции либо стирается (Java, TS, Haskell), либо вычисляется заранее (Rust, C++), либо доживает до рантайма (C#). Отсюда все практические различия дженериков между языками.
• Двойственный квантор ∃ — это интерфейсы, модули и абстрактные типы данных: «тип выбирает реализация», а не вызывающий.

Источники

• Jean-Yves Girard. Interprétation fonctionnelle et élimination des coupures, 1972 — оригинал System F и доказательство сильной нормализации.
• John Reynolds. Towards a Theory of Type Structure, 1974 — springer.
• John Reynolds. Types, Abstraction and Parametric Polymorphism, IFIP 1983 — исходная формулировка параметричности.
• Philip Wadler. Theorems for Free!, FPCA 1989 — PDF.
• Robin Milner. A Theory of Type Polymorphism in Programming, JCSS, 1978 — исток Хиндли-Милнера.
• J. B. Wells. Typability and type checking in System F are equivalent and undecidable, APAL, 1999 — sciencedirect.
• Andrew Wright. Simple Imperative Polymorphism, LASC, 1995 — про value restriction.
• John Mitchell, Gordon Plotkin. Abstract Types Have Existential Type, TOPLAS 1988 — dl.acm.org.
• Benjamin Pierce. Types and Programming Languages, главы 23–25 — сайт книги.
• Go Blog, An Introduction To Generics и дизайн-документ по стенсилингу — go.dev/blog/intro-generics.

Что дальше

Трек закончен: от трёх правил синтаксиса мы дошли до систем, на которых стоят компиляторы и пруф-ассистенты. Дальше расходятся три дороги.

Практика. Всё, что мы кодировали в лямбдах, в рабочем коде выглядит как функции высшего порядка, композиция и типы данных. Идите в трек функционального программирования: обзор, композиция и каррирование, ФП в мейнстрим-языках и архитектура на ФП.

Теория. Лямбда-исчисление — одна из трёх эквивалентных моделей вычислимости, а типы — это логика. Смотрите вычислимость, логику и доказательства, основы теории категорий и теорию категорий в программировании.

Инструменты. Если захотелось строить языки, а не только на них писать — трек компиляторов: проверка и вывод типов, промежуточное представление, виртуальные машины. А как функциональный стиль соотносится с остальными — в треке парадигм: функциональная парадигма и как выбирать и смешивать.

Не знаете, что брать следующим, — загляните в дорожную карту портала: там треки выстроены в порядке, в котором они друг друга поддерживают.