Суд над null

В конце прошлой главы компилятор Python перевёл "hello" * {} — строку, умноженную на пустой словарь, — в байт-код без единой жалобы, и ошибка всплыла только при запуске. Проверка check в компиляторе Огнива следила лишь за тем, чтобы у каждого имени было значение, а о том, какого вида значения и что с ними можно делать, не заботился никто. Спрячем ту же строчку в ветку, куда программа заходит редко.

Функция определена, два вызова прошли, упал третий — в тот момент, когда в программу пришло имя «Хоар». В рабочей программе это может случиться через день или через год после того, как её написали. А ведь ошибку видно из текста: строку на словарь не умножают ни при каком имени. Нельзя ли поручить машине прочитать программу и найти такие места заранее, не запуская её?

Можно. Но сначала об ошибке, которую такие проверки десятилетиями пропускали и которая, по всей видимости, остаётся самой частой в истории программирования. У неё есть изобретатель, и он сам признал вину.

Дело № 53

Глава устроена как судебный процесс. Подсудимый — null, «пустая ссылка»: значение, которое означает «здесь ничего нет». В Python его зовут None, в C — NULL, в Go, Ruby и Swift — nil, в JavaScript их даже два: null и undefined. Обвинение предъявит падения программ и аппарат, потерянный у Марса, защита ответит удобством и скоростью. Между ними выступят эксперты — они объяснят, что такое тип и как машина находит типы, которых никто не писал, — и свидетели: языки, которые обошлись с подсудимым по-разному.

Вы — присяжный. Выслушав обе стороны, вы вынесете приговор, а потом напишете проверку типов сами — программу, которая находит "hello" * {} до запуска.

Обвинение: признание изобретателя

Чтобы понять, что сломалось, вспомним, что обещает тип. В главе 2 тип значения говорил, что с ним можно делать: строку — склеивать и резать, число — складывать. Ссылка типа «запись о сотруднике» обещает, что по ней лежит запись о сотруднике и у неё можно спросить фамилию. Нулевая ссылка это обещание нарушает. Её разрешено положить в переменную любого ссылочного типа, но фамилии у неё не спросишь: по ней ничего не лежит. В C нулевой указатель — это адрес 0, и, как мы видели в главе 38, страницу с этим адресом нарочно не выдают никому: обращение по нему кончается сигналом segfault. В Java вылетает исключение NullPointerException. А в Python None приходит из мест, где его никто не ждёт.

Четыре разные дороги, и в конце каждой — None, о котором ни имя функции, ни её вызов не предупреждают. Последняя строка падает с ошибкой, которую видел каждый, кто писал на Python больше недели: 'NoneType' object has no attribute 'upper'. Хуже всего, что программа падает в одном месте, а ошибка родилась в другом. None может пройти через десяток функций, прежде чем у него попросят атрибут, и трейсбек покажет, где программа упала, но не где пустота появилась.

В SQL тоже есть NULL, но это другое: отметка «значение неизвестно» в клетке таблицы, и SQL её хотя бы не прячет — любое сравнение с ней даёт «неизвестно». Под судом — ссылка, которая выдаёт себя за что угодно.

Экспертиза: что такое тип

Прежде чем судить, суд выслушивает эксперта. Для нужд проверки тип удобно определить так: это множество значений вместе с операциями, которые над ними разрешены. int — целые числа и всё, что с ними делают: сложение, сравнение, остаток. str — строки, их склейка, поиск, умножение на целое число. Ошибка типа — операция над значением, которого нет в её множестве: умножить строку на словарь, попросить .upper() у None.

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

Для Python такая программа есть — mypy. Её начал писать в 2012 году Юкка Лехтосало, финский аспирант Кембриджского университета. В 2014-м он вместе с Гвидо ван Россумом и Лукашем Лангой написал PEP 484 — соглашение о том, как записывать типы прямо в тексте программы. Тип параметра пишут после двоеточия, тип результата — после стрелки: def greet(name: str) -> str. Такие пометки называют аннотациями типов. Сам Python их не проверяет — PEP прямо обещает, что Python останется языком с динамической типизацией, — их читает mypy. Он установлен в песочнице курса, и из ячейки его вызывают через модуль cs.typecheck: функция mypy(текст) печатает, что он нашёл. Номера строк считаются с первой строки кода в переданном тексте.

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

Презумпция виновности

У суда над программами один принцип противоположен человеческому. Суд над человеком исходит из невиновности: сомнения толкуются в пользу обвиняемого. Проверка типов исходит из обратного. Если она не может доказать, что операция безопасна, она отвергает программу, даже если та работает. Чтобы видеть оба суда сразу, дальше будем звать mypy иначе: строка mypy_cell() в начале ячейки отдаёт ему текст самой ячейки — с теми же номерами строк, что на странице, — печатает его вердикт, а потом ячейка выполняется как обычно.

Запуск показывает, что программа верна: числом x бывает только при истинном verbose, и как раз тогда к нему прибавляют единицу. Но чтобы это понять, надо проследить связь двух развилок, а mypy помнит про x одно: «число или строка», int | str. Сложить такое с единицей нельзя, вернуть как строку тоже, и он выдаёт две ошибки. Угадывать он не будет.

Отвергать невиновных проверка иногда обязана: идеальной проверки, которая про любую программу точно скажет, случится ли в ней ошибка типа, не существует. Это следствие теоремы, которую мы докажем в главе 56. Остаётся выбирать, в какую сторону ошибаться. Систему типов, которая никогда не пропускает виновных, называют корректной; цена корректности — отказы невиновным. Есть и утешение: то, что непонятно проверке, часто непонятно и человеку. Перепишите label так, чтобы каждая ветка сама строила свою строку, — и mypy согласится, а функция станет проще.

Свидетель обвинения: аппарат у Марса

Во втором эпизоде обвинения null не участвует, зато видно то же свойство типов: они обещают меньше, чем нам кажется. Он случился через два года после того, как Pathfinder из главы 39 сел на Марс.

Посмотрим на эту историю глазами системы типов. И у программы Lockheed Martin, и у программы навигаторов импульс — дробное число, float. Тип совпал, проверять нечего. Число, за которым стоят 4,45 ньютон-секунды, и число, за которым стоит одна, для системы типов неразличимы: float знает, что это число, но не знает, чего. Можно ли сделать единицы частью типа? Попробуйте в калькуляторе ниже: в нём каждое число едет вместе со своей единицей.

Калькулятор ловит два разных рода ошибок. Первый — ошибка размерности: метры нельзя сложить с секундами ни в каких единицах, и такую строку он отвергает. Второй род коварнее, и именно его совершил орбитер: размерность верная, импульс складывается с импульсом, но единицы разные. Если число несёт единицу с собой, калькулятор переводит одно в другое, и ошибки нет: 1 lbf*s + 1 N*s — это около 5,45 ньютон-секунды. Беда случается там, где единица теряется: программа печатает в файл голое число, другая программа читает его и приписывает свою единицу. В наборе «орбитер: голые числа» всё сходится по размерностям, а ответ неверен в 4,45 раза.

Единицы в типе

Есть три способа заставить машину следить за единицами. Самый лёгкий даёт mypy: NewType создаёт новый тип из старого. Для Python во время работы NewtonSeconds(10.0) — то же самое число, но mypy считает NewtonSeconds и PoundSeconds разными типами и не даст передать одно туда, где ждут другое.

Первый вызов mypy отверг: фунт-сила-секунды не ньютон-секунды. А при запуске тот же вызов прошёл молча — Python аннотаций не проверяет, — и навигаторы «учли» 12 ньютон-секунд вместо 53,4. Второй вызов прошёл, потому что перевод записан явно: умножили на 4,448 и только потом назвали результат ньютон-секундами. При этом NewType не знает физики и не помешает назвать ньютон-секундами число, которое забыли умножить. Он лишь требует, чтобы каждое превращение одной единицы в другую было записано в тексте, где его увидит читатель.

Второй способ — носить единицу вместе с числом во время работы: объект хранит значение и размерность, а сложение и умножение проверяют и пересчитывают её. Так устроен калькулятор выше и библиотеки вроде pint; такой класс вы напишете в задаче «Единицы под контролем». Ошибка обнаружится уже во время работы, при первом же вычислении, зато обнаружится всегда. Третий способ — встроить единицы в саму систему типов. Так сделано в языке F#: единицы измерения появились в нём в версии 2.0 в 2010 году, их проектировал Эндрю Кеннеди. Там 100.0<m> / 5.0<s> имеет тип float<m/s>, сложить метры с секундами не даст компилятор, а во время работы от единиц не остаётся и следа — они ничего не стоят.

Но у всех трёх способов одна граница, и орбитер прошёл как раз по ней. Две программы жили в разных организациях и обменивались файлом. Тип живёт внутри программы; в файле лежат цифры, и между программами следить за единицами может только спецификация интерфейса — а её читают люди. Спецификация у орбитера была, и в ней были правильные единицы. Рабочих правил из этой истории два. Записывайте единицу прямо в данные: поле impulse_newton_s труднее прочитать неправильно, чем impulse. И проверяйте стыки: прогоняйте реальные данные через обе программы сразу, как советовала комиссия по «Ариан-5» в главе 11.

Слово защите

Обвинение высказалось. Защита просит суд выслушать четыре довода.

Первый: пустота нужна. Ключа в словаре может не быть. Поиск может ничего не найти. Значение может быть ещё не вычислено, файл — не открыт, у человека может не быть отчества. Любому языку нужен способ сказать «здесь ничего нет», и None — самый короткий. Уберите его, и программисты начнут изобретать заменители: −1 вместо номера, пустую строку вместо имени, нулевую дату. Заменитель хуже оригинала: −1 можно по ошибке сложить с другим номером, и программа даже не упадёт.

Второй: это бесплатно. Нулевая ссылка — просто ноль в указателе. Она не занимает лишней памяти, а проверка p == NULL стоит одного сравнения. Любая обёртка вроде «значение или ничего» потребует места под признак и времени на его проверку. Для C, ядра системы или прошивки ракеты, где на счету каждый такт, такие расходы заметны.

Третий: свобода. На Python без аннотаций программу пишут за вечер, не объясняя машине того, что и так понятно. Утиная типизация из главы 12 работает с любым объектом, который умеет нужное. Аннотации стоят времени, а проверка, как мы видели, иногда отвергает правильные программы. Не случайно авторы PEP 484 пообещали, что аннотации в Python никогда не станут обязательными.

Четвёртый: типы ловят не всё. Программа «Ариан-5» из главы 11 была написана на Аде — языке со строгой статической типизацией. Перевод 64-битного дробного числа в 16-битное целое был с точки зрения типов законен; не поместилось само значение. Ошибку орбитера типы тоже пропустили: float сошёлся с float. Неверную формулу, перепутанные местами аргументы одного типа, забытую ветку логики проверка типов не видит. Тесты нужны всё равно.

Обвинение отвечает. На первый довод: пустота нужна, но из этого не следует, что пустым может быть всё. Хоар жалел о том, что пустота пролезла в каждый тип; достаточно отличать «строку» от «строки или ничего», и проверка будет следить, чтобы второе не путали с первым. На второй: в Rust тип Option<&T> — «ссылка или ничего» — по гарантии языка занимает столько же памяти, сколько ссылка, и «ничего» в нём записано тем же нулём. Машинный код тот же, что в C; разница только в том, что компилятор не даст забыть проверку. На третий: постепенная типизация уже оставила свободу — аннотации добавляют там и тогда, где они окупаются. Четвёртый довод обвинение принимает: типы ловят не всё. Но то, что ловят, они ловят во всех запусках, а тест — только в тех, которые вы придумали.

Взвешивать доводы будем в конце. Защита жаловалась, что типы приходится писать руками, и суд вызывает второго эксперта, чтобы это проверить.

Экспертиза: типы, которых никто не писал

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

Первым это строго сделал логик Роджер Хиндли: в 1969 году он доказал, что для выражений комбинаторной логики самый общий тип, если он вообще есть, всегда находится алгоритмом. В 1978 году Робин Милнер в Эдинбурге, не зная о работе Хиндли, придумал тот же метод для языка ML, на котором писал систему доказательства теорем, — его алгоритм W. В той же статье есть фраза, которую с тех пор повторяют все, кто занимается типами: правильно типизированные программы не могут пойти вразнос. В 1982 году Луис Дамас доказал, что алгоритм Милнера находит самый общий тип всегда, когда он существует. Метод называют выводом типов Хиндли — Милнера, и на нём стоят ML, OCaml, Haskell, F#; Rust и Swift пользуются его родственниками.

Идея укладывается в три шага. Каждому неизвестному типу даём имя-неизвестную: t1, t2, … Каждое использование даёт уравнение: если f применяют к x, то f — функция, и её аргумент того же типа, что x. Систему уравнений решаем, подставляя найденное в остальные, — это называется унификацией, её придумал Джон Алан Робинсон в 1965 году для автоматического доказательства теорем. Неизвестная, которая так и осталась неизвестной, означает «любой тип»; их печатают как 'a, 'b. Ниже вывод типов для однострочных функций Python — lambda из главы 10. Текст разбирает модуль ast из главы 50, а язык совсем маленький: целые и логические значения, сложение, сравнение, вызов и условное выражение.

Прочтите третий пример. f(x) даёт уравнение «f — функция из типа x во что-то»; f(f(x)) — ещё одно: «результат f тоже годится ей в аргумент». Унификация сводит их к тому, что аргумент и результат f одного типа, а какого — неважно. Ответ ('a -> 'a) -> 'a -> 'a: функция берёт функцию из чего угодно в то же самое, потом значение того же типа и возвращает такое же. Ни одного типа в тексте нет, и всё же вывод дал точное описание, которое годится и для чисел, и для строк. Четвёртый пример выводу не поддался: x служит условием, значит, он bool, а ветки возвращают то 1, то x — целое и логическое сразу быть нельзя. Пятый требует, чтобы тип x был функцией, принимающей саму себя: уравнение t8 = t8 -> t9 решения не имеет, как $x = x + 1$.

mypy устроен скромнее. Тип локальной переменной он выводит сам: после xs = [1, 2] он знает, что xs — list[int]. А тип функции он берёт только из аннотаций: функция без аннотации результата возвращает для него Any. Так задумано: в языке с наследованием, перегрузкой и изменяемыми объектами вывод Хиндли — Милнера в чистом виде не работает, а сигнатура функции, записанная явно, служит документацией, которую проверяет машина.

Свидетели: языки

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

Свидетели разделились на три группы. В первой — C, Java, JavaScript и Python без аннотаций: пустота разрешена в любом месте, и о ней узнают при запуске. C падает с segfault, а то и хуже: обращение по нулевому указателю — неопределённое поведение, и оптимизирующий компилятор вправе считать, что его не бывает. Java бросает NullPointerException, JavaScript — TypeError, Python — AttributeError.

Во второй группе — Kotlin, Swift, TypeScript со строгим режимом, C# начиная с 2019 года и Python вместе с mypy. Пустота в них осталась, но под надзором: тип String пустым не бывает, а String? — бывает, и прежде чем вызвать метод, нужно доказать проверке, что значение есть. Документация Kotlin прямо называет эту часть языка ответом на ошибку на миллиард долларов. Третья группа — Haskell, OCaml и Rust: пустого значения в обычных типах нет вовсе. «Может быть, ничего» — отдельный тип: Maybe в Haskell, Option в Rust. Достать из него значение можно, только разобрав оба случая.

Вещественное доказательство: Optional

Python с mypy — во второй группе. Тип «строка или ничего» пишется str | None; в старом коде встречается и Optional[str] — это то же самое. Такие типы называют необязательными. Для mypy str и str | None — разные типы: в первом None не бывает никогда, второй нельзя использовать как строку, пока не проверено, что там строка.

mypy нашёл одну ошибку — в shout, где результат поиска сразу просят прокричать, — и запуск подтвердил её знакомым AttributeError. В shout_safely ошибки нет, хотя name объявлено как «строка или ничего». Проверка if name is None: return отрезала случай пустоты, и после неё mypy знает, что name — str. Это называют сужением типа: проверка в программе становится доказательством для mypy. Сужают и if name:, и isinstance, и match.

Площадка ниже — для ваших опытов: правьте ячейку, запускайте её и проверяйте mypy. Интереснее всего случаи, где два вердикта расходятся: mypy нашёл ошибку, а запуск прошёл, или наоборот.

У mypy есть и лазейки, и о них стоит знать, чтобы не верить ему больше, чем он обещает. Тип Any отключает проверку для всего, что через него прошло. assert x is not None сужает тип, но это обещание, которое проверяется только при запуске. typing.cast велит mypy поверить на слово. Без них в больших программах не обойтись, но каждое такое место — расписка: «здесь отвечаю я, а не проверка».

Предложение обвинения: алгебраические типы

Третья группа свидетелей обходится без null совсем: вместо одного типа, в который пролезает пустота, она описывает данные как выбор из нескольких вариантов. В Haskell тип «может быть, ничего» объявлен одной строкой: data Maybe a = Nothing | Just a — либо ничего, либо Just со значением внутри. Вертикальная черта читается «или».

Типы данных собирают из двух операций. Запись — это «и»: точка на экране — это x и y. Если у x 1920 возможных значений, а у y 1080, то возможных точек $1920 \cdot 1080$ — произведение. Вариант — это «или»: фигура — это круг или прямоугольник, и возможных фигур столько, сколько кругов, плюс сколько прямоугольников, — сумма. Типы, собранные из сумм и произведений, называют алгебраическими — как раз за эту арифметику. Maybe a — это «тип a плюс одно значение»: возможностей ровно на одну больше. Эта единица — та же пустота, только записанная в типе: в другие типы ей хода нет.

В Python произведение — это класс с декоратором @dataclass: он сам пишет __init__, __repr__ и __eq__ по списку полей. Сумма — объединение типов через |. А разбирают варианты оператором match, который появился в Python 3.10: он сверяет значение с образцами по очереди и сразу достаёт поля. Это называют сопоставлением с образцом. Самое ценное — что mypy проверяет полноту разбора. Если в последней ветке написать assert_never(s) — «сюда управление не доходит», — mypy убедится, что все варианты разобраны раньше, а если какой-то забыт, назовёт его.

Треугольник добавили в объединение, но забыли в area, и mypy указал на assert_never: сюда может прийти Triangle. При запуске прямоугольник посчитался, а треугольник дошёл до assert_never, и программа упала с AssertionError — та же ошибка, но уже у пользователя. В программе на тысячу файлов такая проверка выручает: добавили новый вариант — и проверка перечислит все места, где его не разобрали. Тем же приёмом описывают неудачи. Функция возвращает либо результат, либо описание ошибки — в Rust этот тип зовут Result, — и вызывающий не может забыть про неудачу: чтобы достать результат, ему придётся разобрать оба варианта. Исключения из главы 11 так не умеют: о них сигнатура функции молчит.

Экспертиза: типы с параметром

Мы уже писали list[str] и dict[str, int]. Сам по себе «список» — заготовка, в которую подставляют тип элементов: list[int] и list[str] — разные типы, и mypy не даст положить строку в список целых. Такие типы называют обобщёнными. Свою обобщённую функцию с Python 3.12 объявляют так: параметр-тип пишут в квадратных скобках после имени.

T — та же неизвестная, что 'a у Хиндли — Милнера: при каждом вызове mypy подставляет вместо неё тип аргумента. reveal_type просит mypy рассказать, какой тип он вывел, — это пояснение, а не ошибка; блок if TYPE_CHECKING читает только проверка, Python его пропускает. Для списка чисел first вернёт «целое или ничего», для списка строк — «строку или ничего». Строку n + 1 mypy отверг, хотя при запуске она напечатала 4: список [3, 1, 2] не пуст. Но mypy судит обо всех запусках сразу, и first([]) в той же строке показывает, что вернулось бы в другой раз.

Высшая инстанция: доказательства

У суда есть инстанции, и у проверки программ тоже. Тест из главы 11 спрашивает программу о нескольких входах, выбранных человеком, и про остальные молчит. Проверка типов говорит обо всех входах сразу, но лишь об одном роде ошибок: операция не получит значение чужого типа. Следующая инстанция — доказать, что программа на любом входе делает то, что написано в её описании. Так уже проверены программы, от которых зависит многое.

В 2009 году группа из австралийского исследовательского центра NICTA закончила доказательство корректности seL4 — ядра операционной системы, написанного на 8700 строках C и 600 строках ассемблера. Доказано, что ядро ведёт себя так, как велит его формальное описание: оно никогда не упадёт, не обратится по нулевому указателю и не зависнет в бесконечном цикле. Доказательство заняло около 200 тысяч строк для программы-доказателя Isabelle/HOL, которая проверяет каждый шаг. Сам код ядра обошёлся примерно в два человеко-года, доказательство — примерно в двадцать.

С 2005 года Ксавье Леруа во французском институте INRIA строит CompCert — компилятор C, про который доказано в системе Coq, что скомпилированная программа ведёт себя так же, как исходная. Проверку устроили суровую. В 2011 году группа из Университета Юты опубликовала итоги трёх лет охоты за ошибками компиляторов программой Csmith, которая генерирует случайные корректные программы на C. Нашли больше 325 ошибок в GCC, LLVM и других компиляторах; каждый проверенный компилятор хотя бы раз упал и хотя бы раз молча выдал неверный код. В CompCert ошибки нашлись только в частях, на которые доказательство не распространялось. Ошибок «среднего слоя», которые нашлись у всех остальных, в нём не оказалось, хотя на поиск потратили около шести процессорных лет.

Но и высшая инстанция судит по закону, который написали люди. Доказательство говорит: программа соответствует описанию. Ошибку в самом описании оно не найдёт — авторы seL4 сами признают, что скептик вправе сказать: доказательство лишь показывает, что в реализации ровно те же ошибки, что в спецификации. Разница в том, что спецификация, записанная в той же нотации, втрое короче кода и проще. Получается лестница: тесты дёшевы и ловят частное, типы ловят один род ошибок во всех запусках, доказательство ловит всё, что противоречит описанию, но у seL4 оно обошлось вдесятеро дороже самой программы.

Приговор

Прения окончены, слово присяжным. Ниже все доводы, прозвучавшие в процессе, — по шесть с каждой стороны. Решите про каждый, убеждает ли он вас, — весы покажут, куда вы склоняетесь. Приговор, который получится, — ваша позиция: правильного ответа суд не знает, и языки, как вы видели, решили по-разному.

История, впрочем, свой приговор уже выносит. Kotlin, Swift и Rust, появившиеся в 2010-х, не пускают пустоту в обычные типы без надзора. C# в 2019 году добавил ссылки, которые не бывают пустыми, а Dart в 2021-м перевёл на это весь язык. Java добавила в 2014 году тип Optional, но null по-прежнему разрешён в любой ссылке, и миллиарды строк старого кода не перепишешь. Python оставил решение вам: аннотации и mypy необязательны.

Каким бы ни был ваш приговор, из процесса следует несколько правил на завтра. Пишите аннотации хотя бы у функций, которыми пользуются другие: сигнатура def find(...) -> User | None предупреждает о пустоте лучше любого комментария, и её проверяет машина. Запускайте mypy так же регулярно, как тесты, — в большой программе он находит забытые проверки на None раньше пользователей. Описывайте варианты объединением типов и разбирайте их через match с assert_never. Держите единицы в именах и типах. И помните четвёртый довод защиты: тесты нужны всё равно.

Задачи

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

Куда дальше

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

mypy доволен, и на этих числах функция отвечает: 97 доходит до единицы за 118 шагов. Но остановится ли она на любом целом n больше нуля? Это гипотеза Коллатца из главы 0, и ответа на этот вопрос не знает никто. Зависшая программа бывает хуже упавшей: упавшую перезапускают, зависшую ждут. Нельзя ли написать проверку посильнее — программу, которая читает любую программу и говорит, остановится ли та?

Чтобы ответить, нужно точно сказать, что такое программа и что такое машина, которая её выполняет. Python, «Искра-8», интерпретатор Лиспа из главы 51 слишком сложны, чтобы рассуждать о них строго. Начнём с простейшей машины. У неё нет ни переменных, ни стека, ни ленты — только конечное число состояний и правила перехода между ними. Умеет она немало: например, проверить, похожа ли строка на дату или адрес почты. А вот понять, правильно ли расставлены скобки, ей не по силам. Об этой машине и о языке, на котором ей отдают приказы, — следующая глава.