Все мы знаем, что языки делятся на динамические и статические: Python или JS позволяют молниеносно прототипировать, но расплачиваться нестабильностью в продакшене приходится потом, тогда как C++, Java или C# требуют прописывать типы сразу, оплачивая монументальную надежность замедлением разработки.

В 2006 году Джереми Сиек предложил разрешить этот конфликт концепцией постепенной типизации в работе «Gradual Typing for Functional Languages»: язык остается динамическим по умолчанию, однако разработчик может аннотировать типами отдельные модули или функции, не покрывая ими всю кодовую базу, а типизированный и нетипизированный код взаимодействуют через специальный динамический тип Dyn. Звучит как сказка — быстрое прототипирование с постепенным наращиванием стабильности. Однако при детальной проработке вскрылись фундаментальные нюансы: в серии последующих работ Сиек, Таха, Вадлер и другие показали, что стыковка типизированного и нетипизированного кода требует операции приведения типа (cast), а дизайн этого каста упирается в противоречие между тремя желаемыми свойствами — надёжностью системы типов (soundness), собственно постепенностью (gradual typing) и отсутствием рантайм-обёрток на границах (no wrappers).

Позднее сообщество, и я в том числе, переосмыслило третью вершину: no wrappers — это забота о производительности и прозрачности рантайма, безусловно важная, но с позиции программиста, а не математика-оптимизатора, правильнее говорить о удобстве разработчика (developer-friendly). Это свойство вбирает в себя no wrappers как частный случай, добавляя понятные сообщения об ошибках, низкий порог входа и отсутствие многослойных типовых аннотаций, ведь если ради производительности приходится городить бесконечные теоремы типов, такая система едва ли приживётся на суровом рынке опенсорса.

Так родилась трилемма Святого Грааля системы типов: выбрать можно любые два свойства, а третье неизбежно пострадает, и в этой статье мы разберём, как создатели языков пытались достичь всех трёх и на какие компромиссы шли.

❯ Три свойства, 3 пути

Давайте разберем сразу, на каких трех свойствах стоит трилемма, и почему чаще всего удается соблюсти только 2 свойства, принеся в жертву третье свойство.

Soundness — созвучность, непротиворечивость

Soundness как свойство означает, что система типов не противоречит: если компилятор принял код без ошибок типов, то в рантайме не будет ошибок типов. Ценность свойства заключается в твердых гарантиях что баги, связанные с несоответствием типом, исключены из продакшена.

Самый простой пример — typescript и python с Any-типом.

from typing import Any

name: Any = "Hello"
name = name.is_integer()

Компилятор типов MyPy не покажет никаких ошибок, хотя в рантайме мы встретим AttributeError: 'str' object has no attribute 'is_integer'.

Теперь посмотрим, с чем soundness вступает в конфликт.

Путь 1 — Soundness + Developer-Friendly — теряем Gradual Typing. Если мы хотим, чтобы система была и непротиворечивой, и удобной, проще всего потребовать полной типизации. Никаких Any, никаких Dyn. Весь код аннотирован и компилятор все проверяет. Ошибки точны и понятны, потому что у компилятора есть вся информация о типах. Но увы, нельзя начать с динамического прототипа и плавно типизировать его.

Путь 2: Soundness + Gradual Typing — теряем Developer-Friendly. Это сложный путь, чтобы система типов была и постепенной, и непротиворечивой, система обязана вставлять рантайм проверки на каждой границе между типизированным и нетипизированным кодом, или строить сложные аннотации типов. Для простых типов (Dyn → Int) это приемлемо: просто проверяем, что пришло число. Но для сложных — функций, дженериков, вложенных структур — системе приходится создавать обёртки (wrappers), которые проверяют типы при каждом вызове. Эти обёртки замедляют выполнение, загрязняют стек-трейсы и нарушают структурное равенство: две идентичные функции могут перестать быть равны из-за разного количества обёрток.

С сообщениями об ошибках — отдельная муторная история. Когда обёртка ловит несоответствие типов, непонятно, кого винить: статический код, который ждал Int, или динамический, который передал String? Сиек и Вадлер разработали Blame Calculus — формализм, который отслеживает происхождение каста и в случае ошибки указывает, на какой стороне границы допущена ошибка, это мы рассмотрим чуть ниже. Таким путем идет мало кто, приходит на ум только Hack: гарантии есть, постепенность есть, но пользоваться системой типов сложно.

Gradual Typing — постепенная типизация

Постепенная типизация — это возможность смешивать типизированный и нетипизированный код в одном проекте и переходить от одного к другому плавно, как я писал выше.

Путь 1: Gradual Typing + Developer-Friendly — теряем Soundness. Это самый популярный компромисс в нашем мире. Мы разрешаем разработчику использовать динамические типы, или не определять аннотации вообще. Компилятор доверяет программисту и не вставляет проверок на границах, и взаимодействие между этими двумя мирами происходит без накладных расходов. Правда взамен этого удобства и скорости теряется непротиворечивость, динамический тип становится квази-типом, прокси между типом и значением. Этот путь исповедуют такие языки как Python с MyPy и TypeScript (который вообще позиционируется как «синтаксический сахар над JavaScript»).

А путь Gradual Typing + Soundness с потерей Developer-Friendly мы уже обсуждали.

Developer Friendly — удобство для разработчика

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

В оригинальной трилемме эту вершину занимало свойство No Wrappers — отсутствие рантайм-обёрток на границах между типизированным и динамическим кодом, но я решил обобщить это удобством для разработчика, включив туда No Wrappers.

Оба пути мы обсудили, либо гарантии и полная типизация, либо свобода и удобство без гарантий.

Но, увы, одно из свойств всегда страдает. Любые два свойства тянут систему в определённом направлении, а третье оказывается несовместимым с этим движением, как лебедь, рак и щука.

Хотите гарантий (Soundness) и удобства без накладных расходов (Developer-Friendly)? Система должна знать всё о типах заранее — Gradual Typing невозможен.

Хотите удобства без накладных расходов (Developer-Friendly) и постепенности (Gradual Typing)? Система должна доверять разработчику и не мешать ему проверками — Soundness невозможна.

Хотите гарантий (Soundness) и постепенности (Gradual Typing)? Система должна проверять всё на границах и создавать обёртки — Developer-Friendly невозможен.

❯ Истоки: каст как источник и решение всех проблем

В 2006 году Джереми Сиек опубликовал диссертацию и статью «Gradual Typing for Functional Languages», где конкретизировал идею постепенной типизации. Он сделал центральным понятием работы динамический тип Dyn - прокси-тип между типизированным и нетипизированным кодом. Переменная типа Dyn может содержать значение любого типа, и компилятор не проверяет операции над ней. Но когда Dyn пересекает границу и попадает в типизированную функцию, системе нужна операция каста — приведения Dyn к конкретному типу, например Int.

Именно дизайн каста и порождает трилемму. Давайте возьмем псевдокод:

function add(x: Int, y: Int): Int {
    return x + y;
}

let a: Dyn = 42;
let b: Dyn = "hello";

add(a, b);

У компилятора есть три варианта, и каждый из них жертвует одним свойством:

1. Игнорировать и ничего не проверять. Скомпилировать как есть, считать что Dyn совместим с любым типом. Быстро, удобно и никаких расходов. Но это пропускает ошибку типов в рантайм, и мы теряем soundness.

2. Вставить проверку на границе, проверяя перед вызовом add что оба аргумента подходят по типу. Soundness соблюден в жертву developer-friendly.

3. Либо потребовать типы сразу. Тут страдает gradual typing.

Третий и первый вариант тривиален (это просто статическая типизация или динамическая с аннотациями типов), а вот второй потребовал отдельной теоретической проработки. Сиек и Вадлер в работе «Threesomes, With and Without Blame» (2010) разработали Blame Calculus — исчисление вины. Идея в том, что каждый каст помечается меткой: положительной (static) и отрицательной (dynamic). Если каст Dyn → Int провалился, система смотрит на метку и определяет источник ошибки: положительная метка означает что виноват статический код, который ожидал Int, а получил не пойми что. А отрицательная метка говорит что виноват динамический код, который передал значение не того типа.

Формально Blame Calculus гарантирует, что ошибка будет на какой то одной стороне. Но проблема в том, что когда разработчик видит сообщение об ошибке, оно может ссылаться на каст, а не на строку которую он написал. Вот тут и начинает страдать developer-friendly.

Дальнейшие исследования, например «Exploring the Design Space of Higher-Order Casts» от Сиека и Ко., показали, что для сложных типов (функции высшего порядка, дженерики) проблема обёрток и нечитаемых ошибок только усугубляется. Каст Dyn → (Int → Int) нельзя проверить в момент приведения: функция ещё не вызвана, аргументов нет. Приходится создавать прокси-функцию, которая оборачивает исходную и проверяет типы аргументов и возвращаемого значения при каждом вызове. С каждым вложенным кастом растёт число обёрток и тем усложняется внутреннее представление программы.

❯ А что выбирают разработчики языков программирования?

Наконец-то пора перейти к тому, как реальные языки с динамической типизацией пытаются (или не пытаются) достигнуть святого Грааля.

TypeScript — это самый яркий пример осознанной жертвы Soundness. TypeScript — это синтаксический сахар над JavaScript, так что цель не в том чтобы добавить гарантий, а в том чтобы облегчить разработку без нарушения обратной совместимости.

На первый взгляд Python с MyPy идёт тем же путём. Any в typing ведёт себя так же, как any в TypeScript — отключает проверки. Но есть нюанс. MyPy по умолчанию строже TypeScript в двух отношениях. Во-первых, он требует явного указания Any: если вы не аннотировали переменную и не пользуетесь выводом типов, MyPy может потребовать аннотацию в зависимости от настроек. Во-вторых, mypy можно настроить на строгую проверку, запретить неявное использование Any. TypeScript такого уровня строгости не предоставляет.

Но плата за такою настраиваемость — сложность настройки. Чтобы получить soundness, нужно не просто писать аннотации, но и правильно сконфигурировать сам тайпчекер, разобраться в флагах, интегрировать его в CI, а также может порождать монструозные аннотации типов. Как по мне, overload и дженерики в питоне — это монструозные конструкции. Это смещает баланс в сторону Developer-Friendly страдает, даже если Soundness в теории достижима. Один только typing.overload заставляет меня дрожать в ужасе. Например, в typeshed достаточно долго висят issue связанные с overload, например этот, я сам его пытался решить, но окончательно запутался в куче функций, типов и необходимости писать по несколько overload’ов в определенном порядке.

Команда Elixir в версии 1.20.0 предложила другой взгляд. Вместо того чтобы жертвовать каким нибудь свойством, они решили пойти на компромиссы, чтобы сохранить все три свойства. Dynamic-типы, сужение типов и многое другое, полноценный разбор этого релиза я планирую в отдельной статье, ибо он интересный даже для тех кто никогда не интересовался миром BEAM, а пока можете прочитать оригинальную статью.

❯ Заключение

Трилемма Святого Грааля — не формальная теорема. Никто не доказал математически, что система с тремя свойствами невозможна. Это наблюдаемый на практике фундаментальный конфликт, который воспроизводится в любой попытке скрестить динамику со статикой.

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

Тем не менее, поиски продолжаются. Каждые несколько лет появляются новые подходы — от расширенного вывода типов до множественных представлений (set-theoretic types, которые кстати также изучаются в elixir), которые как раз и пытаются переосмыслить святой Грааль.

Выбирая язык для проекта, вы всегда выбираете сторону треугольника, даже если не формулируете это явно. Быстрый прототип без типов с перспективой роста? Ваша плата — отсутствие гарантий на ранних этапах, и TypeScript или Python с Any здесь — осознанный выбор. Большой проект, где надёжность критична, а скорость разработки вторична? Возможно, вы заплатите удобством и возьмёте Hack или строгую конфигурацию MyPy. Готовы отказаться от постепенности вообще? Rust или Haskell дадут и soundness, и отличные сообщения об ошибках.

И как по мне, интересны сейчас компромиссы, как можно расширить рамки, соблюдая все три свойства одновременно? Тут я поддерживаю авторов Elixir.

Новости, обзоры продуктов и конкурсы от команды Timeweb.Cloud — в нашем Telegram-канале ↩