Глава 5. Компилятор как доказательство

Глава 5. Компилятор как доказательство

Что вообще доказывает «компилируется»

Вот функция работы с заказом. Ничего хитрого, обычный код.

function firstSku(order: Order): string {
  const item = order.items[0];
  return item.sku;
}

Отдайте её одному моему коллеге — он скажет, что всё в порядке, и tsc у него промолчит. Отдайте другому — tsc подчеркнёт item.sku и сообщит:

const item = order.items[0];
return item.sku;
//     ~~~~ 'item' is possibly 'undefined'.

Исходник побайтово один и тот же. Разные у них не руки, не версия компилятора и не операционная система. Разный — tsconfig.json. У второго включён флаг noUncheckedIndexedAccess, у первого нет. Под одной настройкой обращение к order.items[0] даёт { sku: string; qty: number }, под другой — { sku: string; qty: number } | undefined, и .sku на возможном undefined уже не проходит.

Остановитесь на этом, потому что вещь неуютная. Валидность кода оказалась не свойством кода. Один и тот же текст одновременно корректен и некорректен — смотря какой конфиг лежит рядом. «Компилируется» перестало быть высказыванием о программе и стало высказыванием о паре «программа плюс настройки».

Для пришедшего из мира, где валидность определяет спецификация языка, это сбивает с ног. Там вопрос «компилируется ли это» имеет один ответ на всю планету: либо текст соответствует грамматике и правилам типизации языка, либо нет, и никакой файл рядом этого не меняет. Здесь ответ зависит от ручки, которую кто-то когда-то повернул. И тогда встаёт вопрос, на который держится вся эта глава: если сама проверка настраивается, то что вообще означает её прохождение? Что доказывает зелёная сборка, если силу проверки задал не язык, а вы?

Компиляция — это проверка доказательства

Чтобы ответить, надо вернуться к тому, что компилятор делает на самом деле. В главе 1 мы разделили две его работы — проверку и стирание — и условились, что они независимы. Сейчас нас интересует только первая, и к ней нужен более точный язык.

Соблазнительно думать про tsc как про переводчик: взял .ts, выдал .js. Но перевод — это работа стирания, второй фазы, и она ничего не утверждает о правильности. Первая фаза занята другим. Она берёт ваш код вместе со всеми аннотациями и проверяет, не противоречат ли они друг другу. Не переводит — проверяет. На вход ей идёт утверждение, на выходе — вердикт: утверждение состоятельно или нет.

Аннотация : string на возврате firstSku — это утверждение: «что бы ни вернула эта функция, это будет строка». Проверяющий не верит на слово. Он прослеживает все пути через тело функции и смотрит, во всех ли случаях возвращается строка. Если находит путь, где возвращается что-то ещё или где item мог оказаться undefined, — утверждение не доказано, и он сообщает об этом. Зелёный результат означает не «я перевёл», а «я проверил твоё утверждение и не нашёл, чем его опровергнуть».

Это и есть точная модель: проверяющий типов — ассистент доказательств (proof assistant). Вы пишете теорему — сигнатуры, аннотации, формы — и пишете доказательство — тело программы. Компилятор механически проверяет, что доказательство закрывает теорему. Не придумывает за вас, не исполняет, а именно проверяет: сходится ли заявленное с написанным.

И вот тут возвращается тот неуютный конфиг. Если компиляция — проверка доказательства, то у проверки есть строгость. Можно требовать, чтобы доказательство закрывало все случаи, а можно сквозь пальцы смотреть на пропущенные. Флаги в tsconfig — это и есть регулятор строгости. Они решают, какие пробелы в доказательстве считать дырами, а какие пропускать. Под слабой настройкой firstSku доказана как «вернёт строку, если массив непуст, а пустоту мы решили не рассматривать». Под строгой — теорема честнее: «массив может быть пуст, докажи возврат и в этом случае». Один и тот же код закрывает разные теоремы. Отсюда и два вердикта.

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

strict — это набор

«Включи strict» — первый совет, который слышит любой новичок, и почти всегда без объяснения, что за ним стоит. А стоит за ним не один флаг, а семейство. strict: true — это переключатель, который разом поднимает примерно десяток отдельных проверок. Разберём несущих участников: что каждый покупает и чем за это платит.

noImplicitAny. Без него компилятор, не сумев вывести тип, молча ставит any и идёт дальше. Параметр без аннотации, к которому неоткуда вывести тип, становится any — и проверка этого аргумента тихо отключается.

function totalWithTax(order) {  // без strict: order неявно any
  return order.total * 1.2;     // order.total — any, проверки нет
}
totalWithTax("не заказ");        // молчит, рантайм разберётся

С noImplicitAny этот код не пройдёт: «Parameter ‘order’ implicitly has an ‘any’ type». Флаг покупает отсутствие тихих дыр — каждое попадание в any теперь либо ваше осознанное решение (написали : any руками), либо ошибка. Платите вы аннотациями: код, опиравшийся на молчаливый any, придётся типизировать.

strictNullChecks. Главный из всех. Без него null и undefined — члены каждого типа: переменная : string спокойно принимает null, и .toUpperCase() на ней проходит проверку, а в рантайме падает. Флаг вынимает null и undefined из всех типов и делает их отдельными, которые надо учитывать явно.

function findOrder(id: OrderId): Order | undefined {
  return orders.get(id);
}

const order = findOrder("A-1");
order.total;
// ~~~~~ 'order' is possibly 'undefined'.

Без флага возврат был бы просто Order, undefined молча прятался бы внутри, и order.total прошёл бы — до первого ненайденного заказа в продакшене. С флагом тип честно говорит Order | undefined, и компилятор требует разобрать случай отсутствия, прежде чем трогать .total. Это настолько существенный сдвиг, что ему отведена отдельная глава (Глава 10); здесь достаточно знать, что без strictNullChecks остальная строгость почти бессмысленна — самый частый рантайм-сбой остаётся непойманным.

strictFunctionTypes. Делает присваивание функций состоятельным по параметрам. Без него можно подсунуть туда, где ждут обработчик более общего типа, обработчик более узкого — и получить рантайм-несовпадение, которое проверка пропустила. Флаг закрывает эту дыру для функций, объявленных как функции (на методы, по совместимым с остальным языком причинам, он не распространяется — это острый край, к которому мы ещё вернёмся в главе про функции).

strictPropertyInitialization. Требует, чтобы поле класса было инициализировано — в объявлении или в конструкторе, — либо честно помечено как способное быть undefined.

class OrderService {
  private cache: Map<OrderId, Order>;
  // ~~~~~ Property 'cache' has no initializer
  //       and is not definitely assigned in the constructor.
}

Без флага поле было бы Map, по факту — undefined до первого присваивания, и первое же обращение упало бы. Флаг покупает гарантию, что объявленное поле к концу конструктора действительно того типа, что обещано. Работает в паре со strictNullChecks — без него ему не на что опереться.

useUnknownInCatchVariables. Прямое продолжение разговора из главы 1 про то, почему catch не типизируется. Брошено может быть что угодно — не только Error, а строка, число, undefined. Без флага переменная в catch имеет тип any, и вы беспрепятственно зовёте на ней любой метод.

try {
  pay(order);
} catch (e) {       // с флагом: e имеет тип unknown
  console.log(e.message);
  //          ~ 'e' is of type 'unknown'.
}

Флаг даёт переменной catch тип unknown вместо any — то есть заставляет проверить, что вы вообще поймали, прежде чем обращаться к .message. Это честно: язык не может пообещать, что в catch прилетит Error, и теперь не делает вид, что может. Платите вы проверкой формы на входе в обработчик — ровно той дисциплиной на границе, которой посвящена пятая часть книги.

Общая логика набора видна. Каждый флаг закрывает один класс тихих дыр и берёт за это плату аннотациями или явным разбором случаев. strict — это решение закрыть их все разом. Не магия, не «режим качества», а конкретный список конкретных проверок, каждую из которых можно назвать и объяснить.

За пределами strict

Естественно решить, что strict: true — это потолок, дальше некуда. Это не так. Есть проверки, ловящие настоящие баги, которых в strict нет вовсе. С одной из них глава началась.

noUncheckedIndexedAccess. Доступ по индексу — arr[i], map[key] — в обычном TypeScript возвращает тип элемента, как будто промах невозможен.

const order = ordersById["A-404"]; // тип: Order
order.total;                        // проходит. в рантайме: undefined

Но обращение по несуществующему ключу даёт undefined, и тип об этом молчит. Флаг добавляет | undefined к результату любого индексного доступа:

const order = ordersById["A-404"]; // тип: Order | undefined
order.total;
// ~~~~~ 'order' is possibly 'undefined'.

Теперь компилятор требует разобрать промах. Это та самая проверка, что превратила безобидный firstSku в начале главы в ошибку.

exactOptionalPropertyTypes. Уточняет, что значит необязательное поле. Без флага status?: "paid" принимает и отсутствие ключа, и явное status: undefined — а это разные вещи: «поля нет» и «поле есть, и оно пустое».

type Patch = { status?: Order["status"] };
const p: Patch = { status: undefined }; // без флага — ок
// с флагом: Type '{ status: undefined; }' is not assignable to type
//           'Patch' with 'exactOptionalPropertyTypes: true'. Consider
//           adding 'undefined' to the types of the target's properties.

Флаг разводит эти случаи: ? означает «ключа может не быть», но не «значением может быть undefined». Если вы строите частичное обновление, где { status: undefined } и {} должны вести себя по-разному, разница перестаёт быть невидимой.

Сюда же примыкают проверки на грани с линтером: noImplicitReturns (все пути функции должны возвращать согласованно), noFallthroughCasesInSwitch (запрет на проваливание между case), noUnusedLocals и noUnusedParameters (мёртвый код). Они не про состоятельность типов, а про класс ошибок «забыл», и компилятор способен их ловить заодно.

Резонный вопрос: если эти флаги ловят реальные баги, почему их нет в strict? Ответ — эргономика, а не принцип. noUncheckedIndexedAccess добавляет | undefined к каждому индексному доступу, и в коде, где вы только что проверили длину массива в строке выше, компилятор всё равно потребует разобрать «невозможный» undefined. Цена в шуме высока, выгода зависит от кода, и авторы решили не навязывать её всем по умолчанию. strict собран как разумная база, на которой работает большинство; эти флаги — точечное усиление под конкретную задачу. Включать их стоит, когда вы знаете, какой класс ошибок покупаете, и готовы платить за него многословием.

Флаг — самый дешёвый способ купить гарантию

Сделаем шаг назад и посмотрим, что вообще произошло, когда мы включили noUncheckedIndexedAccess. Одна строка в конфиге — и целый класс ошибок «обращение к несуществующему элементу массива» из невидимого стал невозможным. Не в одном месте. Во всём проекте, на каждом индексном доступе, раз и навсегда.

Сравните это с тем, во что обошлась бы та же гарантия вручную. Найти все обращения по индексу. Возле каждого вспомнить, может ли индекс промахнуться. Где может — дописать проверку на undefined. Не забыть ни одного. Удержать дисциплину на code review. Проследить, чтобы новый код, написанный через полгода другим человеком, тоже её соблюдал. Целый класс ошибок, закрываемый постоянным усилием множества людей, — против одной строки, после которой про этот класс можно забыть, потому что компилятор не даст его допустить.

Вот в чём настоящий рычаг проверяющего как ассистента доказательств. Вы не доказываете отсутствие ошибки в каждой точке кода руками. Вы декларативно заявляете теорему — «в этой кодовой базе индексный доступ всегда учитывает промах» — и автоматический доказатель проверяет её за вас, всюду, на каждой сборке, без устали и без пропусков. Флаг — это не настройка удобства. Это формулировка свойства, которое вы хотите видеть истинным во всей программе, отданная машине на принудительное соблюдение.

Поэтому к tsconfig стоит относиться не как к техническому файлу, который скопировали из шаблона и забыли, а как к списку гарантий, которые вы купили. Каждая строка там — это либо включённая проверка, что-то доказывающая, либо выключенная, что-то пропускающая. Самая дешёвая инженерная сделка из существующих: одна декларация против бесконечной ручной бдительности.

Глазами джависта

В Java вопрос «насколько строго меня проверяют» не имеет смысла. Сила проверки зафиксирована спецификацией языка. javac проверяет ровно то, что предписывает Java Language Specification, — не больше и не меньше, — и ручки, которой это можно ослабить или усилить, не существует. Программа либо well-formed по спецификации, либо нет. Один ответ, одинаковый у всех.

Поэтому идея, что один и тот же исходник валиден под одним конфигом и невалиден под другим, джависту чужда на уровне рефлекса. У него «компилируется» — абсолютное свойство кода, а не относительное к настройкам. Ближайшее, что есть в его мире, — флаги -Xlint и внешние линтеры вроде SpotBugs, но это слой поверх компиляции, предупреждения рядом с ней, а не сам вердикт о валидности. Тип-чек у него один и неподвижен.

Откуда вообще взялся этот градиент строгости в TypeScript? Из задачи, которую Java никогда не решала. Java типизировала свой код с первого дня; типы были там всегда, по умолчанию и без альтернативы. TypeScript пришёл в мир, где уже жили миллионы строк нетипизированного JavaScript, и должен был принять их все — от «просто перестань ругаться и транспилируй мой старый JS как есть» до «докажи про мой новый код всё, что можешь». Эти два требования несовместимы в одном фиксированном уровне строгости. Регулятор — прямое следствие: TypeScript обязан обслуживать оба конца спектра, и потому строгость пришлось сделать настройкой. То, что джависту кажется тревожной зыбкостью, — цена за способность натянуть типы на чужой живой код, которого у Java под ногами просто не было.

Строгость не бесплатна и не монотонна

Теперь честная часть, потому что у регулятора строгости есть цена и есть ловушки, и обойти их молчанием значило бы соврать.

Первое и самое коварное — валидность зависит от конфигурации, а конфигурация не одна на проект. Сторонняя библиотека, чьи типы лежат в .d.ts, написана и проверена под её собственным tsconfig. Вы подключаете её под своим, более строгим. Её типы прошли проверку у автора, но утверждения в них слабее, чем требует ваш конфиг, — и вы получаете либо | undefined, всплывающий из чужого индексного доступа, либо тип, который под вашим strictNullChecks оказывается дырявее, чем выглядел у автора. Граница между вашим кодом и чужими .d.ts — это граница между двумя теоремами разной силы, и стыкуются они не всегда гладко.

Второе — слабые конфиги дают ложную уверенность, и это опаснее открытой ошибки. Зелёная сборка под слабой теоремой ощущается так же успокаивающе, как под сильной, — то же слово «компилируется», тот же зелёный цвет. Но доказано под ней мало. Команда, унаследовавшая проект без strictNullChecks, живёт с ощущением типобезопасности, которой у неё нет: компилятор молчит не потому, что всё верно, а потому, что его не просили проверять самое важное. Тишина слабого конфига и тишина строгого выглядят одинаково и означают противоположное.

Третье — строгость способна завалить вас работой не по делу. noUncheckedIndexedAccess честен, но неизбирателен: он добавит | undefined и там, где вы строкой выше проверили длину, и там, где индекс — заведомо валидная константа. Компилятор не настолько умён, чтобы доказать вашу правоту в этих случаях, и потребует разобрать «невозможный» undefined. Иногда это спасает; иногда — это шум, который заставляет либо городить лишние проверки, либо тянуться к ! и as, проделывая в той же строгости дыру.

Четвёртое — набор strict не зафиксирован навечно. Со временем в него добавляют новые проверки. Это значит, что апгрейд версии TypeScript может, ничего не меняя в вашем коде, добавить в него ошибки: код, валидный вчера, перестаёт компилироваться сегодня, потому что теорема под именем strict стала сильнее. Для языка это здоровое движение, для вашего CI в день обновления — внезапная красная сборка на ровном месте.

И пятое, помельче, но реальное: флаги взаимозависимы. strictPropertyInitialization без strictNullChecks бессмыслен. useUnknownInCatchVariables опирается на наличие strictNullChecks, чтобы unknown имел вес. Включать строгость по одному флагу, не понимая связей, — способ получить странные половинчатые результаты. Набор называется набором не случайно.

Ничто из этого не довод против строгости. Это её настоящая цена, и платить её осознанно лучше, чем обнаружить постфактум.

Читай tsconfig как аксиомы своего доказательства

Вот сдвиг, ради которого вся глава.

Перестаньте видеть в зелёной сборке самостоятельное свидетельство правильности. «Компилируется» — это всегда сокращение от «компилируется под этой конфигурацией», и без второй половины первая ничего не утверждает. Прежде чем поверить вердикту, посмотрите, какую теорему вы заказали. Открыть tsconfig и прочитать его как список аксиом доказательства — strictNullChecks есть? noUncheckedIndexedAccess? что выключено и почему? — это не педантизм, а единственный способ узнать, чего стоит зелёный цвет в этом конкретном проекте.

Из этого следует рабочее правило по умолчанию. Берите максимальную доказуемую строгость как точку старта. Не потому, что строже значит добродетельнее, а потому, что сильная теорема — это больше пойманных ошибок за ту же цену сборки, и отказываться от них без причины расточительно. Ослабление — допустимо, но только осознанно и точечно: вот эта конкретная граница с нетипизированной библиотекой, вот этот участок легаси, где строгость обошлась бы дороже, чем приносит. Ослабление с объяснением, привязанное к месту, — инженерное решение. Ослабление по наследству, потому что конфиг достался от кого-то и его не стали трогать, — это принятая вслепую слабая теорема, про которую вы даже не знаете, что именно она перестала доказывать.

Зрелый выбор — не «строго везде» и не «как привыкли», а осознанная карта строгости по границам проекта: где доказываем всё, где сознательно отступаем и почему. Этим — строгостью как спектром, который выбирают на каждой границе отдельно, — мы займёмся подробно в главе 31. Пока достаточно одного: конфиг — это ваши аксиомы, и читать чужой код, не прочитав его аксиом, значит не знать, что в нём вообще доказано.

Итог

Проверяющий типов доказывает ровно ту теорему, которую вы задали ему конфигом, — не больше; «компилируется» без знания tsconfig не утверждает ничего. На этом часть I собрана: в одном файле живут две программы, связанные стиранием; они говорят формами значений, а не ярлыками классов; типы в них выводятся, а не диктуются; и проверяются они с той силой, которую вы выбрали сами.