Приветствую, странники Хабра! Меня зовут Алексей Васильев, я разработчик в команде Инновационных Технологий Страхового Дома ВСК. В погоне за производительностью программ, элегантностью их кода и масштабируемостью систем мы часто забываем о фундаменте: исполняет ли программа именно то, что мы от нее ожидаем? Как долго программа будет работать корректно? Цена ошибки может быть разной — разочарование пользователей, финансовые потери компаний… Печально, но в некоторых случаях это безопасность и жизнь людей.

Но ошибки — не досадные случайности. Это следствие утраты контроля над собственным намерением. Существует невообразимое число различных способов сломать код. И есть разные способы защитить программу от ошибок. Мы всегда заинтересованы в верификации. Пожалуй, самое явное подтверждение этому — обилие всевозможных тестов, которыми в современной разработке принято покрывать системы перед их запуском в использование. И даже не только перед запуском: разработка через тестирование, test‑driven development — сегодня де‑факто стандарт в промышленной разработке. Тестирование — это уже почти верификация. Но возможности тестирования в обеспечении защиты программ от ошибок и гарантии защищенности, которые оно предоставляет, фундаментально ограничены. По определению, любое тестирование — это всегда эмпирическая проверка ограниченного количества случаев. Таким образом мы соглашаемся на то, что не можем проверить все и везде, но что самое главное — не можем дать абсолютной гарантии того, что даже те случаи и тот код, который мы протестировали будут правильно работать всегда. Ведь проверка была эмпирической, а значит, сколько бы мы ни перепроверяли, вероятность того, что при очередном запуске все сломается или внезапно получится другой результат — остается.

Что же делать, если мы хотим большей уверенности в корректности и надежности того, что разрабатываем с таким трудом? На помощь приходит формальная верификация. Но первое слово скрывает необходимость выбора. С одной стороны, это безусловно (мы ожидаем некоторых формальных гарантий) должно привести нас в область высокой уверенности в надежности и корректности нашего ПО (high assurance systems). С другой стороны, это подразумевает, что начать мы должны с формализации наших ожиданий, aka «хотелок». Ведь показать формальную достоверность можно только для чего‑то, что само по себе полностью лишено неоднозначности. Получить абсолютно строгую, формальную постановку задачи — уже нетривиальная задача.

Вообще, область формальной верификации невероятно многогранна и глубока. Цель данной статьи — показать, что этот подход может быть доступен в широкой практике разработки и осветить основные инструменты, которые предоставляет для этого язык программирования Idris 2. А также продемонстрировать особенную красоту программ, корректных по построению. Мы сделаем это на примере всем известной задачи о ФиззБаззе. Материал не предполагает наличия глубокой теоретической подготовки читателя, только базовое знакомство с принципами функционального программирования, ну и… немного любви к математике.

1. Введение в Idris, зависимые типы и процесс Type‑Driven Development

2. Специфицируем задачу

3. Пишем решение. Доказываем корректность логики

4. Вводим альтернативную спецификацию, показываем эквивалентность

5. Строим программу. Верифицируем поведение

Введение в Idris, зависимые типы и процесс Type-Driven Development

Давайте начнем с небольшого знакомства с языком, который мы будем использовать. Idris — это функциональный язык программирования с зависимыми типами первого класса и возможностями системы доказательства теорем. Язык разработан Эдвином Брэди, британским компьютерным ученым, в настоящее время — ведущим научным сотрудником Сент‑Андрусского университета в Шотландии. Язык назван в честь поющего дракона Идриса из британской детской телепередачи «Паровозик Айвор».

Idris реализует наиболее выразительную систему типов по классификации лямбда‑куба Барендрегта — полиморфное лямбда‑исчисление высшего порядка с зависимыми типами (оно же исчисление конструкций, ). Это означает, что в нашем распоряжении присутствуют: параметрический полиморфизм, операторы над типами, и собственно, зависимые типы. Типы в Idris являются конструкциями первого класса. Все это, в некотором смысле, размывает уже саму границу между типом и значением. Вторая версия языка встраивает в систему типов механизмы стирания и линейности, основанные на теории квантитативных типов и аппарате субструктурных интуиционистских логик.

Мы еще посмотрим на все упомянутое выше в действии, однако сначала давайте проясним следующее: зачем нам все это, и почему именно Идрис? Идрис был спроектирован с замыслом продвижения методологии «разработка через типирование», Type‑Driven Development, по иронии судьбы разделившей акроним с популярным подходом, который мы уже упоминали выше. В разработке через типирование (далее в тексте TDD будет обозначать только ее), типы трактуются не просто как синтаксическое средство языка, но выступают как основной инструмент для построения программы. Набор введенных программистом типов рассматривается как своего рода план программы, а компилятор, с его подсистемами проверки и вывода типов, — как полноценный помощник, ассистент программиста, с которым они вместе постепенно строят программу, в соответствии с планом. Чем более выразительным является определенный в начале набор типов, тем больше уверенности в корректности итоговой программы — именно в смысле полноценности, точности реализации программистом своего исходного намерения (а не просто в смысле того, что программист не допустил синтаксических и грамматических ошибок в коде, и поэтому все скомпилировалось).

Цель Idris — сделать передовые подходы в программировании доступными для разработчиков‑практиков. И важная философия, которой придерживается проект, заключается в том, что Idris позволяет программисту использовать сильные методы, основанные на типизации: показывать инварианты данных, формально специфицировать поведение программы и доказывать ее свойства, но не требует этого. При желании, Идрис можно использовать просто как «обыкновенный» функциональный язык с типами первого класса. Также немаловажен приоритет в «официальном» позиционировании инструмента именно как, в первую очередь, языка программирования общего назначения, а не теорем‑прувера (что никак не запрещает использовать Идрис подобным образом, хотя и чувствуя все же некоторые недостатки по отношению к Rocq или Agda). Сам Эдвин Брэди любит характеризовать Идрис как «Pac‑Man‑complete»‑язык: он не только какой‑то там в теории завершенный по Тьюрингу, на Идрисе реально сделать полноценный работающий Pac‑Man!

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

data Vector  : (length : Nat) -> (elementType : Type) -> Type where
        Nil  : Vector Z _
        Cons : (elem : eType) -> (vect : Vector len eType) -> Vector (S len) eType

Это функциональная структура данных, которая описывает некоторое семейство типов, как функцию двух аргументов: натурального числа length и принимаемого типа данных elementType (тип элементов вектора), с результатом в виде некоторого типа, конкретного экземпляра данного семейства. Далее есть два конструктора, которые позволяют создавать эти конкретные экземпляры типов, таким образом как бы разбивая все семейство векторов на два подсемейства. Конструктор Nil позволяет создавать пустые векторы, то есть те, у которых length = Z ( это тип натурального нуля в аксиоматике Пеано: да, в Идрисе, в стиле Бурбакистов, натуральные числа начинаются с нуля). Но самое интересное происходит в Cons: это конструктор, то есть способ получить вектор из другого подсемейства типов, и он сам является функцией, которой нужны два аргумента: элемент некоторого типа eType , и уже имеющийся вектор с элементами именно этого типа eType, c длиной len, и тогда будет построен новый вектор из элементов eType с длиной ровно на единицу больше len (снова в соответствии с принципами Пеано,  — это конструктор типа натурального числа, которое следует за некоторым другим натуральным:

• 

• 

• 

  и т. д.).

То есть, обратите внимание, результирующие типы конструкторов Nil и Cons — это частные случаи Vector: когда его длина, по своей структуре, есть , и когда длина, по структуре, есть . Таким образом, сам в итоге — это алгебраический тип данных (то есть тип‑сумма из типов‑произведений: в Nil и в Cons).

Вот тип функции‑конструктора Cons это и есть зависимый тип! Или, точнее, один из видов зависимых типов: зависимая функция. Действительно: какой именно тип Vector получится в результате применения функции Cons, зависит от того, какие конкретно значения elem и vect она получила в качестве аргументов (а сами значения elem и vect — это типы, частные случаи и соответственно. Вы уже перестали различать типы и значения?.. Хорошо!). Сам тип Vector тоже зависимый: это зависимая функция, чья область значений определяется значениями ее аргументов, что и показывают конструкторы, как специальные имена для подобластей значений Vector. Мы можем сказать, что зависимый АТД проиндексирован типом и параметризован типом (тип второго аргумента). Можно использовать более короткую запись:

data Vector  : Nat -> Type -> Type where
        Nil  : Vector Z _
        Cons : e -> Vector l e -> Vector (S l) e

Какая польза от зависимых типов? Вся суть в том, что при декларации сущности Vector мы в конструкторах ясно описали структурные зависимости (результата от необходимых для его получения посылок). И в награду за эту точность и ясность при описании того, что есть Vector и как он может возникнуть, тайпчекер будет далее нам помогать: защищать от возможностей совершить ошибки при определении функций, которые работают с данной сущностью. И даже более того, он будет помогать нам их определять!

БАЗА

Тут пришло время немного подробнее остановиться на самом методе TDD. Его формула выглядит как последовательность инструкций для программиста:

1. Type : описываем тип

2. Define = даем определение

3. Refine : уточняем описание (переходим на шаг 1)

Давайте, используя этот подход, реализуем несколько полезных функций на векторах, которые мы специфицировали выше. Например, функция безопасного взятия первого элемента, головы вектора. Как говорит TDD, сперва мы должны описать ее тип:

safeVectHead : Vector (S l') eType -> eType

Здесь сразу приходит на ум объявить тип аргумента, как вектор, где длина имеет структуру length = S l'. Таким образом, мы просто не сможем передать в функцию пустой вектор: длина у вектора‑аргумента должна быть последователем некоторого натурального числа (сам l' может быть равен Z, но S l' — никак). Если где‑то в коде мы все‑таки попытаемся передать в safeVectHead аргумент типа Vector Z Type, компилятор выдаст ошибку. Если бы мы написали в типе просто Vector k eType, то тогда мы были бы недостаточно точны в выражении своего намерения. Компилятор понял бы нас так: в функцию позволяется передавать вектор любой длины с типом , в том числе нуль: k = Z. А написав наш первый вариант, мы ясно выразили, что принимаемый вектор не может быть пустым. Второй важный момент: мы прямо говорим, что вернуть функция должна некоторое значение ровно того же типа, что и элемент(ы) в принятом векторе. Итак, первый шаг: «Type», описание типа — самый важный. На нем мы договариваемся с компилятором о своих намерениях.

Реализация же, в данном случае, становится тривиальной:

safeVectHead : Vector (S l') eType -> eType
safeVectHead (Cons head tail) = head

Как и во многих современных функциональных языках, в Идрисе мы используем структурное сопоставление с образцом, чтобы написать определение функции. То есть мы буквально разбираем все возможные случаи входных параметров по их структуре. А какие виды векторов у нас бывают? Nil и Cons. Но Nil нет необходимости рассматривать, потому что он просто не пересекается с областью значений типа . Это кодомен Cons, который, в свою очередь «разбирается» на свои аргументы head и tail — элемент и вектор, как мы описывали выше. При этом компилятор может вывести тип tail: это , где (т.е. Z или S Nat). И здесь у нас просто не остается вариантов, кроме правильного: вернуть head. Мы не сможем, например, так просто «умудриться» вернуть здесь safeVectHead tail (типа зачем‑то рекурсивно вызвать функцию на хвосте списка) — этот вариант не пройдет структурную унификацию параметров: опять же, safeVectHead ожидает аргумент с длиной вида , а длина в tail — это просто какой‑то Nat, в том числе это может быть нуль (т. е. tail может быть Nil). То есть, в данном случае, правильное определение функции буквально автоматически выводится из ее типа.

Нет необходимости в проверках времени выполнения: что принятый вектор не оказался пустым, или что мы не выбрали для возврата что‑то не то — все решено на этапе компиляции. И компилятор также может проверить, что наша функция покрывающая (определена на всех входах) или даже тотальная (завершается на всех входах) — зависит от режима, устанавливаемого директивой %default (в Idris 2 по умолчанию %default covering). Почему все оказалось так удобно и легко? На самом деле, благодаря нашей удачной спецификации для вектора, а именно конструкторам Nil и Cons. Когда мы описывали вектор, мы декларировали, что есть два способа его построить: Nil «по первому слову» создаст пустой вектор, а Cons потребует предоставить ему элемент и уже существующий вектор, а последний мог быть построен снова либо с помощью Nil, либо с помощью Cons. Все это приводит нас в итоге к тому, что любой вектор, по нашей спецификации — либо пустой, либо прямое произведение элемента и вектора, и вот тут и сокрыт секрет удобства реализации safeVectHead. Скажем, если в рамках данной спецификации мы захотим реализовать функцию взятия последнего элемента в векторе, нам придется постараться немного больше (стать чуть более многословными в определении функции; вы можете увидеть этот вариант в репозитории туториала на ГитХабе). Или же — изменить спецификацию (вот он, третий шаг «Refine»). Как именно, подумайте сами (это совсем несложно, все подсказки мы уже предоставили выше в тексте; ну или ответ всегда можно найти в стандартной библиотеке Идриса).

Другой пример — соединение двух векторов. Опять же, на первом шаге определимся с намерением:

join2Vectors : Vector m e -> Vector n e -> Vector (m + n) e

Все уже максимально прозрачно: мы ожидаем два вектора с элементами одного типа и некоторыми длинами , а вернем вектор из элементов такого же типа длины ровно . Переходим к определению:

join2Vectors : Vector m e -> Vector n e -> Vector (m + n) e
join2Vectors Nil                    v2 = v2
join2Vectors (Cons v1_head v1_tail) v2 = Cons v1_head (join2Vectors v1_tail v2)

Это стандартный подход с разбором случаев по некоторому аргументу и рекурсией. Обратите внимание вот на что: благодаря структуре зависимостей в результирующем типе функции, а также спецификации Vector, программисту не получится по ошибке написать, например, такой рекурсивный вызов: join2Vectors v2 v1_tail («случайно» перепутали стороны при соединении).

Мы уже научились брать первый и последний элементы из вектора, давайте реализуем функцию взятия элемента по произвольному индексу (тоже типобезопасную, разумеется). И вот тут, на первом шаге «Type», мы задумаемся. А как нам специфицировать, чтобы индекс не мог выйти за пределы размера вектора? Без всяких проверок времени выполнения. На помощь спешит математика. Давайте подумаем, векторы у нас проиндексированы типом , область значений которого не ограничена сверху, т. е. элементы . Взять элемент по индексу можно только из непустого вектора, но если это конкретный вектор, то число элементов в нем конечно (т. к. длина есть конкретный Nat). Но это значит, что индекс элемента вектора должен принадлежать конечному множеству элементов (а не открытому справа Nat). Значит, для индекса нам нужно объяснить Идрису, что такое конечное множество. Аналогично спецификации вектора, введем тип для конечного множества:

data Finite  : (cardinality : Nat) -> Type where
        Zero : Finite (S _)
        Next : Finite n -> Finite (S n)

Это АТД, который также проиндексирован типом , и также имеет два конструктора: Zero, для взятия (или «указания на») нулевого элемента из конечного множества ненулевой мощности, и Next, для взятия следующего элемента из конечного множества ненулевой мощности, если был уже взят предыдущий элемент. То есть Finite здесь можно читать как «выбери из конечного множества», или «ты можешь выбрать конечное число раз». Что можно выбрать? Произвольный нулевой элемент и произвольный элемент, следующий за кем‑то (в порядке конкретного множества). То есть Zero, это на самом деле «возьми первый раз». А Next это «возьми еще». Но обратите внимание, ни один конструктор не захватывает в свой кодомен Finite Z. Это значит, что выбрать элемент из пустого множества мы не сможем никак (даже если где‑то мы объявим тип , населить этот тип нет способов). И также это значит, что если мы объявили некоторый тип , то конструкторы Zero и Next позволят нам выбирать элементы из Finite k максимум раз. Первый раз будет с помощью Zero, а далее Next вплоть до , то есть не превысит .

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

getElementAt : (index : Finite n) -> (vector : Vector n eType) -> eType

Длина вектора-аргумента зависит от мощности множества его индексов. То есть компилятор на этом месте понимает: функция объявлена для любого индекса из конечного множества и вектора с длиной, равной мощности этого множества. Определим функцию:

getElementAt : (index : Finite n) -> (vector : Vector n eType) -> eType
getElementAt Zero     (Cons head tail) = head
getElementAt (Next i) (Cons head tail) = getElementAt i tail

Снова заметим, что рассматривать пустые вектора здесь нет смысла. Это невозможно, так как не может существовать свидетельств (построенных значений) типа . Компилятор Идриса в данном случае может это понять сам, но если очень хочется, можно такие случаи прописать явно, с помощью ключевого слова impossible:

getElementAt _ Nil impossible	-- в определении getElementAt
safeVectHead Nil impossible		-- в определении safeVectHead

Забегая вперед, можно сказать, что вся суть программ, корректных по построению — в использовании алгебраических зависимых типов для моделирования задачи и в следовании стратагеме «make illegal states unrepresentable». Мы отказываемся от идеи валидации данных. Вместо этого мы моделируем предметную область так, чтобы все возможные высказывания в ней имели смысл. Поскольку Идрис позволяет производить вычисления внутри объявлений типов, мы можем специфицировать сколь угодно нетривиальные свойства и поведение наших программ. Единственный потолок здесь — воображение и навык разработчика.

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

Специфицируем задачу

Давайте начнем с постановки задачи. Вот классическая формулировка:

Напишите программу, которая выводит на экран числа от  до  включительно. Но вместо чисел, которые делятся на три, выведите «Fizz», а вместо чисел, которые делятся на пять — «Buzz». Если число делится и на три, и на пять, выведите вместо него «FizzBuzz».

Исходно это такая детская игра‑считалка, цель которой — обучение детей правилам деления. Вот и мы, в своем подходе к реализации программной логики, будем, в некотором роде, именно обучать программу понимать (а на самом деле прояснять для себя вопрос), что такое делимость и как именно ее правильно использовать для решения поставленной задачи. Именно ясное и строгое выражение понятий будет фундаментом, на котором мы построим реализацию, цель которой — доказательная корректность. Вот этот момент очень важно осознать заранее, перед тем, как начать разработку. Давайте посмотрим на следующий пример реализации на Python:

for i in range(1, 101): print('Fizz' * (i % 3 == 0) + 'Buzz' * (i % 5 == 0) or i)

Это правильно работающий ФиззБазз. Вернее, один пример из бесчисленного множества реализаций правильно работающих ФиззБаззов. В данном случае мы видим, что программист явно ценит лаконичность, простоту и изящество кода: действительно, это без лишних слов перевод исходной формулировки задачи с естественного языка на язык Питона. Но положительные стороны данного примера обязаны его конкретности. Если мы захотим обобщать данное решение: вводить новые правила вывода слов в зависимости от делимости чисел, расширять диапазон работы программы и т. п., при этом с условиями проверяемости результата на правильность и наличия некоторой систематизированности в коде — нам потребуется вводить абстракции. Пример движения в этом направлении (не выходя за рамки Python) можно увидеть, например, здесь. Объем решения, по сравнению с однострочником, приведенным выше, увеличивается примерно в 200 раз (как внушительно могут выглядеть цифры, правда?), но примерно ¾ кода — (property‑based) тестирование. Решение стало расширяемым (мы легко можем добавить новое правило в игру), но показательно, что необходимость убедиться в том, что решение осталось правильным, растет быстрее, чем основная система.

Гибкость — не единственное, за что приходится «платить» доверием. Вот пример развития решения в совершенно другом направлении. За поражающую воображение производительность приходится платить еще больше: ~400 строк кода самого решения и ~800 строк — весь пост целиком! Да, это текст поста вместе с кодом решения, но мы будем считать пост — документацией к системе, и код в ней приводить просто необходимо, т. к. комментарии идут по тексту реализации, и если убрать код, станет просто не понятно, о каком конкретно хитром битовом сдвиге или другом хакерском трюке идет речь в данный момент (и наоборот, если убрать сопровождающие комментарии, то в том, какую вообще задачу решает этот код, не сразу разберется даже опытный программист).

Что объединяет все решения, приведенные выше (лаконичный, гибкий, ультраоптимизированный подходы)? Без тени иронии или критики — это прекрасные инженерные решения и отличные примеры развития в разных парадигмах разработки. Каждое из трех имеет свои сильные стороны, которые сложно превзойти. Но есть и одна совершенно общая слабость, которой они поражены — хрупкость доверия к системе. Вот ее анамнез:

1. Программист на 90% верит, что штуки вроде 'Fizz' * (i % 3 == 0) правильно делают свою работу: действительно проверяют делимость на 3 и вернут «Fizz» в правильном случае (как‑то умножив строку на логическое значение, или оно будет приведено к целому, перегрузка операторов… что вообще здесь на самом деле происходит понимает только высококвалифицированный заклинатель змей). И мы так же абсолютно верим программисту, что сложная битовая маска в примере ультрапроизводительной реализации вычислена верно, что программист вообще правильно понял задачу, которая держится на словесной спецификации (и легко расходится с кодом при малейших изменениях). Вероятность ошибки программиста есть всегда, и с ростом кодовой базы она растет (супер)экспоненциально.

2. Когда мы осознаем, насколько велика вероятность ошибки, мы понимаем необходимость скрупулезного тестирования именно корректности реализации. Включается «доверяй, но проверяй». Поскольку нет строгих способов «запретить» создать программу, которая может выдать «Bazz» вместо «Buzz» для n = 5 (или вообще программист перепутает 5 и 15 в проверке делимости), мы можем лишь проверять результат и констатировать факт — правильно получилось или нет. Но тесты могут быть неполными, могут содержать ошибки сами, и всегда могут лишь среагировать на баг после его появления (а система/обновление уже неделю как живут на проде..). Строго говоря, тесты все‑таки валидируют (проверяют результат процесса), а не верифицируют (гарантируют сам процесс) корректность.

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

Мы постараемся решить именно эту проблему: не сделать очередную правильно работающую реализацию с помощью очередного набора инструментов, а построить систему, в которой состояния с неверной логикой ФиззБазза принципиально невозможны и отвергаются на этапе сборки исполняемого кода из исходного.

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

data Divisible : (numer : Nat) -> (denom : Nat) -> Type where
        SelfDivisible : Divisible (S x') (S x')
        NextDivisible : Divisible (S n') (S d') -> Divisible (S n' + S d') (S d')

Как мы уже видели во введении, это достаточно общий паттерн для определения типов: мы описываем некоторый тривиальный случай, который строится «Ex nihilo», и способы построения «менее очевидных» вариантов. В данном случае, мы говорим, что само на себя число делится тривиально, для этого не нужно каких‑то доказательств, это аксиома. Но выполняется такое свойство, очевидно, только для отношений, в которых делимое и делитель равны. А в качестве нетривиального случая мы можем ввести понятие «следующей делимости», с посылкой вида «если делится на » и выводом «значит делится на ». Обратите внимание, в результатах типов конструкторов мы везде представляем и делимое и делитель как последователей некоторого натурального числа. Вводя такую структуру мы сразу «уберегаем» наш домен делимости от любых отношений с нулем, как в числителе, так и в знаменателе. В том смысле, что они могут быть описаны формально, как типы:

divOfZero : Divisible 0 1
divByZero : Divisible 1 0
undefined : Divisible 0 0

, но населить такие типы реальными значениям возможности нет. Это важный прием: мы не только абстрактно моделируем делимость (формулируем свойство), мы сразу думаем о конкретной предметной области — да, ноль делим на ноль, но конкретно такого частного в нашем ФиззБаззе не будет (конкретное частное не определено математически, а логически использование предикатов делимости с нулем неявно превращает доказательства в математические софизмы; в конце концов, нам такое просто не нужно в домене).

Имея фундаментальное понятие делимости, мы сразу можем описать тип, отвечающий за возможные состояния нашей программы:

data GameState : (number : Nat) -> Type where
        Number   : Not (Divisible n 3) -> Not (Divisible n 5) -> GameState n
        Fizz     : Divisible n 3       -> Not (Divisible n 5) -> GameState n
        Buzz     : Divisible n 5       -> Not (Divisible n 3) -> GameState n
        FizzBuzz : Divisible n 3       -> Divisible n 5       -> GameState n

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

Not : Type -> Type
Not x = x -> Void

То есть мы могли бы все то же самое записать и так:

Number : ((Divisible n 3) -> Void) -> ((Divisible n 5) -> Void) -> GameState n

, очевидно, что с Not нагляднее. Конструкция же сама по себе означает, что наличие терма типа приводит к противоречию. это встроенный пустой тип, который не имеет конструкторов. Вообще. Таким образом, в любой функции, результирующим типом которой является , хотя бы один аргумент обязательно тоже должен быть (иначе нам просто нечего вернуть, а сам по себе Void никак не построить). Функции, результирующие в пустой тип, таким образом, можно использовать для доказательств от противного, т. к. Void также описывает тип тривиально ложного высказывания. Мы еще увидим, как это работает на практике.

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

{n : _} -> Show (GameState n) where
        show (Number   _ _) = show n
        show (Fizz     _ _) = "Fizz"
        show (Buzz     _ _) = "Buzz"
        show (FizzBuzz _ _) = "FizzBuzz"

это тип, проиндексированный натуральным параметром , а интерфейс Show связывает его значения со строками, определяя конкретные методы для каждого состояния игры. Для всех состояний, кроме Number, мы возвращаем конкретные заданные строки, а в случае Number вызываем show на аргументе параметра состояния n (поэтому мы должны описать его как неявный параметр вначале, чтобы он попал в контекст методов show), который есть натуральное число, а для них интерфейс определен в стандартной библиотеке. То есть, по сути мы перегружаем один метод интерфейса («класса» или «категории» типов, в которую мы добавляем GameState) в зависимости от конкретных областей значений его аргумента. Параметры доказательств состояния нас не интересуют в контексте методов интерфейса Show, поэтому мы их описываем пропусками (а могли бы интересовать, если бы нам было важно, например, какая именно это делимость: тривиальная или «последующая»). Мы перевели исходную словесную постановку задачи на формальный язык типов в нашей программе.

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

-- логика вычисления игрового мира
gameLogic : (number : Nat) -> GameState number

-- пока оставим такой очень грубый набросок, очевидно,
-- в этой спецификации не до конца выражено желаемое устройство процесса
-- (first : Nat) -> (last : Nat) -> ... -> IO ()
playFizzBuzz : (first : Nat) -> (last : Nat) -> IO ()

-- запуск игры
main : IO ()
main = playFizzBuzz 1 100

Пока, конечно, это не окончательный план построения программы, в playFizzBuzz мы лишь грубо обозначили идею, как мы хотим видеть игровой процесс. Вероятно, на самом деле мы должны будем получить некоторое множество состояний GameState и перевести их в вывод IO (для чего у нас уже есть интерфейс), и, разумеется, мы должны будем отразить это в спецификации (то есть явно описать всю логику, согласно которой формируется итоговый вывод программы на экране). Иначе в итоге снова получим процесс, который держится на доверии, что из чисел каким‑то магическим образом получаются правильные выводы. Но, спокойствие, до этого мы обязательно дойдем.

На самом деле, мы только что сделали самый важный шаг. Мы смоделировали (пусть и пока размыто относительно конечного бизнес‑процесса), предметную область в системе типов. Далее, в рамках этой спецификации, возможны только корректные состояния и непротиворечивые высказывания. Программисту для реализации потребуется всего лишь показать, как именно возможны правильные высказывания. Здесь важно остановиться, чтобы понять — если спецификация размыта, как сейчас, то и множество «корректных» высказываний будет больше того, что мы на самом деле желаем. А мы ведь хотели, чтобы реализовать что‑то заведомо непозволительное, типа признать неделимое делимым или напечатать «Fizz» для состояния Buzz не было принципиальной возможности. Пока очевидная дыра в нашей спецификации заключается в том, что она в программе позволит получать выводы на экран, минуя всю нашу прекрасно смоделированную логику. То есть сейчас мы в общих чертах представляем, как внутри должен быть устроен мир нашего ФиззБазза, но пока не видим, как гарантировать корректность процесса взаимодействия с ним.

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

Пишем решение. Доказываем корректность логики

Настало время разрешить ФиззБазз! Обо всем по порядку, давайте сначала построим реализацию игровой логики:

gameLogic : (number : Nat) -> GameState number
gameLogic n with (decideDivisible3 n, decideDivisible5 n)
      _ | (No  proofNotFizz, No  proofNotBuzz) = Number   proofNotFizz proofNotBuzz
      _ | (Yes proofFizz,    No  proofNotBuzz) = Fizz     proofFizz    proofNotBuzz
      _ | (No  proofNotFizz, Yes proofBuzz)    = Buzz     proofBuzz    proofNotFizz
      _ | (Yes proofFizz,    Yes proofBuzz)    = FizzBuzz proofFizz    proofBuzz

Вообще здесь реально нет вариантов сделать неправильно. GameState number требует, согласно спецификации, пары доказательств для своего аргумента, относительно возможности его делимости на  и на . Иначе состояние просто не построить. Давайте представим, что у нас есть процедуры для осуществления подобных выводов:

decideDivisible3 : (input : Nat) -> Dec (Divisible input 3)
decideDivisible5 : (input : Nat) -> Dec (Divisible input 5)

Паттерн Dec — фундаментальный инструмент для построения разрешающих процедур:

data Dec : Type -> Type where
        Yes : (proof_ : prop)     -> Dec prop
        No  : (contr_ : Not prop) -> Dec prop

Технически это очень простой тип‑обертка, который позволяет сказать о выполнении некоторого свойства  либо «Да», требуя явно предоставить свидетельство этого свойства, либо «Нет», с требованием явного свидетельства того, что свойство неверно: . То есть это как «строгий Maybe», только Maybe мы используем, когда хотим гибкости в рассуждениях, а когда хотим надежности, нам нужно не «может быть» а строго «да/нет». Это ровно та форма заключений, которую требует наш GameState, и в gameLogic мы с помощью паттерн‑матчинга просто анализируем полученные заключения, и строим соответствующие состояния.

Мы движемся к самому ядру логики нашего ФиззБазза, теперь нам требуется реализовать автоматические процедуры разрешимости делимости на 3 и на 5 для произвольного аргумента. Технически, для этого нам нужно автоматически генерировать термы типов , и т. д. Как это сделать? Спецификация позволяет нам утверждать делимость двумя способами: SelfDivisible и NextDivisible. Значит, мы должны утверждать или отрицать делимость на основании этих двух предикатов. Но как быть для произвольного аргумента? Вспомним, что у нас вообще есть две базовые техники доказать что‑то:

1. прямо рассмотреть все возможные ситуации и сделать выводы, либо

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

Очевидно, в данном случае, мы должны рассуждать вторым образом, то есть по индукции. В качестве ее базы мы можем взять набор утверждений относительно тривиальных случаев, то есть отношений, в которых делимое меньше или равно делителю. Благо что делители у нас небольшие, значит и набор утверждений для базы индукции разрешающих процедур описать не составит большого труда. А потом потребуется сделать вспомогательные процедуры для перехода от утверждения о (не)делимости с некоторым аргументом к утверждению относительно следующей (не)делимости (у нас «следующая» это

).

Мы понимаем, что из всех базовых случаев свойство делимости будет утверждаться только в последнем, то есть когда делимое и делитель равны (и для этого нам не потребуется каких‑то дополнительных функций, т. к. есть явный конструктор свойства делимости для таких отношений). Так что мы распишем доказательства неделимости базовых отношений, где делимое меньше делителя. Давайте так и напишем все это — от частного к общему, от деталей к идее. Вот наши тривиальные случаи неделимости:

-- база индукции для делителя 3
proof0NotDivBy3 : Not (Divisible 0 3)
proof0NotDivBy3 _ impossible

proof1NotDivBy3 : Not (Divisible 1 3)
proof1NotDivBy3 SelfDivisible                         impossible
proof1NotDivBy3 ({n', d' : Nat} -> (NextDivisible _)) impossible

proof2NotDivBy3 : Not (Divisible 2 3)
proof2NotDivBy3 SelfDivisible                         impossible
proof2NotDivBy3 ({n', d' : Nat} -> (NextDivisible _)) impossible

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

Стоит также добавить, что impossible это не какой‑то unsafe cast вроде believe_me, это вполне легитимное указание компилятору проверить невозможность паттерна. Если тайпчекер (на этапе унификации параметров) не сможет найти невозможную комбинацию, он вернет ошибку:

twoPlusTwoNotFive : Not (2 + 2 = 5)
twoPlusTwoNotFive Refl impossible			-- верно

twoPlusTwoIsFour : (x = 2) -> (x + x = 4)
twoPlusTwoIsFour Refl impossible			-- ошибка, аргумент Refl возможен
twoPlusTwoIsFour Refl = Refl			    -- верно

Проще говоря, все заявленные программистом impossible проверяются компилятором. Однако метод консервативен (поскольку это именно проверка тайпчекером паттернов на стадии унификации параметров, не более), поэтому не стоит ожидать от него слишком много:

thereIsA : a -> Not (Not a)
thereIsA _ _ impossible	    -- ошибка, чисто с точки зрения унификатора все ok,
thereIsA a notA = notA a	-- хотя в действительности, конечно, невозможно иметь
					        -- предикат и его отрицание одновременно

data Equal : forall a, b . a -> b -> Type where
     [search a b]
     Refl : {0 x : a} -> Equal x x

Повторим те же базовые доказательства для нашего второго делителя, пяти:

-- база индукции для делителя 5
proof0NotDivBy5 : Not (Divisible 0 5)
proof0NotDivBy5 _ impossible

proof1NotDivBy5 : Not (Divisible 1 5)
proof1NotDivBy5 SelfDivisible                         impossible
proof1NotDivBy5 ({n', d' : Nat} -> (NextDivisible _)) impossible
 
proof2NotDivBy5 : Not (Divisible 2 5)
proof2NotDivBy5 SelfDivisible                         impossible
proof2NotDivBy5 ({n', d' : Nat} -> (NextDivisible _)) impossible

proof3NotDivBy5 : Not (Divisible 3 5)
proof3NotDivBy5 SelfDivisible                         impossible
proof3NotDivBy5 ({n', d' : Nat} -> (NextDivisible _)) impossible

proof4NotDivBy5 : Not (Divisible 4 5)
proof4NotDivBy5 SelfDivisible                         impossible
proof4NotDivBy5 ({n', d' : Nat} -> (NextDivisible _)) impossible

Обратите внимание, что в случаях, где делимое есть нуль, мы можем обобщить оба случая конструкторов в одно определение. Просто приятное удобство, тайпчекер Идриса с этим справляется. Для отличного от нуля делимого нам приходится быть немного более многословными.

Далее, для случаев, когда делимое и делитель равны, мы в разрешающих процедурах, очевидно, сможем просто утверждать делимость с помощью SelfDivisible. Теперь нам нужен тот самый логический переход, когда мы понимаем неделимость некоторого данного отношения и хотим рассуждать о свойстве следующего отношения. То есть:

proofNextNotDivBy3 : Not (Divisible (S n') 3) -> Not (Divisible (S n' + 3) 3)
proofNextNotDivBy5 : Not (Divisible (S n') 5) -> Not (Divisible (S n' + 5) 5)

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

decideDivisible3 : (input : Nat) -> Dec (Divisible input 3)
decideDivisible3 Z                  = No  proof0NotDivBy3
decideDivisible3 (S Z)              = No  proof1NotDivBy3
decideDivisible3 (S (S Z))          = No  proof2NotDivBy3
decideDivisible3 (S (S (S Z)))      = Yes SelfDivisible
decideDivisible3 (S (S (S (S x')))) with (decideDivisible3 (S x'))
      _ | Yes proof_ = rewrite proofCongPlus3 x' in Yes (NextDivisible      proof_)
      _ | No  contr_ = rewrite proofCongPlus3 x' in No  (proofNextNotDivBy3 contr_)

decideDivisible5 : (input : Nat) -> Dec (Divisible input 5)
decideDivisible5 Z                          = No  proof0NotDivBy5
decideDivisible5 (S Z)                      = No  proof1NotDivBy5
decideDivisible5 (S (S Z))                  = No  proof2NotDivBy5
decideDivisible5 (S (S (S Z)))              = No  proof3NotDivBy5
decideDivisible5 (S (S (S (S Z))))          = No  proof4NotDivBy5
decideDivisible5 (S (S (S (S (S Z)))))      = Yes SelfDivisible
decideDivisible5 (S (S (S (S (S (S x')))))) with (decideDivisible5 (S x'))
      _ | Yes proof_ = rewrite proofCongPlus5 x' in Yes (NextDivisible      proof_)
      _ | No  contr_ = rewrite proofCongPlus5 x' in No  (proofNextNotDivBy5 contr_)

Все в целом очевидно, как объясняли выше, строим индукцию на базе тривиальных доказательств. Когда рассмотрели все конкретные тривиальные случаи, описываем один обобщенный нетривиальный случай: количество конструкторов в образце аргумента делимого равно . На новом ядре делаем рекурсивный вызов (прямо в сопоставлении с образцом, круто?!) разрешающей процедуры и оцениваем результат. Если относительно предыдущей делимости мы получили утвердительный ответ, тогда строим следующую прямо по спецификации, иначе используем наш логический переход (щас распишем его, щас..) чтобы показать следствие неделимости следующего отношения на основе неделимости данного. А что за rewrite здесь появились?

rewrite это указание произвести в терме подстановку согласно некоторому равенству с явным предикатом (есть еще синтаксис replace с неявным выводом свойства). Эти средства реализуют принцип «неразличимости тождественных»: если два терма равны, то они имеют одинаковые свойства (подробнее). Нам это нужно, чтобы успокоить разволновавшийся тайпчекер, заявляющий:

While processing right hand side of with block in decideDivisible3. Can't solve constraint between: plus x' 3 and S (S (S x')).

While processing right hand side of with block in decideDivisible5. Can't solve constraint between: plus x' 5 and S (S (S (S (S x')))).

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

proofCongPlus3 : (x : Nat) -> S (S (S x)) = x + 3
proofCongPlus3 Z     = Refl
proofCongPlus3 (S k) = cong S (proofCongPlus3 k)

proofCongPlus5 : (x : Nat) -> S (S (S (S (S x)))) = x + 5
proofCongPlus5 Z     = Refl
proofCongPlus5 (S k) = cong S (proofCongPlus5 k)

cong доказывает эквивалентность результатов применения функции на эквивалентных аргументах:

cong : (0 f : t -> u) -> (0 p : a = b) -> f a = f b
cong f Refl = Refl

Так, там осталась одна формальность, переходы proofNextNotDivBy3 и proofNextNotDivBy5. Для SelfDivisible, очевидно, невозможная комбинация сразу, а для NextDivisible просто получаем противоречие из «наличия» одновременно термов делимости (следующее «типа делится», но значит был аргумент для конструктора NextDivisible) и неделимости (только что выше делали такое в примерчике thereIsA), так что все предельно просто:

proofNextNotDivBy3 : Not (Divisible (S n') 3) -> Not (Divisible (S n' + 3) 3)
proofNextNotDivBy3 contr_curr proof_next = ?whatNow

Заглянув в дыру ?whatNow видим простую задачу:

 0 n' : Nat
   proof_next : Divisible (S (plus n' 3)) 3
   contr_curr : Divisible (S n') 3 -> Void
 ------------------------------
 whatNow : Void 

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

proofNextNotDivBy3 : Not (Divisible (S n') 3) -> Not (Divisible (S n' + 3) 3)
proofNextNotDivBy3 contr_curr (SelfDivisible _) impossible
proofNextNotDivBy3 contr_curr (NextDivisible curr) = contr_curr curr

Аналогично для… Так, стоп. Что за..

While processing left hand side of proofNextNotDivBy3. Can't solve constraint between: ?n' [no locals in scope] and ?_ [no locals in scope].

Нужно обозначить неявные параметры? Не вопрос, распишем все явно:

proofNextNotDivBy3 : (Divisible (S n') 3 -> Void) -> Divisible (S n' + 3) 3 -> Void
proofNextNotDivBy3 contr_curr (SelfDivisible _) impossible
proofNextNotDivBy3 contr_curr (NextDivisible {n'} {d' = 2} curr) = contr_curr curr

Хм.. Неявный параметр конструктора Идрис увидел, но с параметром контекста его не получается унифицировать:

While processing left hand side of proofNextNotDivBy3. Can't solve constraint between: ?n' [no locals in scope] and ?n' [no locals in scope].

Сделать еще более явно..?! Ну ok, давайте прямо покажем весь путь n':

proofNextNotDivBy3 : {n' : Nat} -> (Divisible (S n') 3 -> Void) -> Divisible (S n' + 3) 3 -> Void
proofNextNotDivBy3 {n'} contr_curr (SelfDivisible _) impossible
proofNextNotDivBy3 {n'} contr_curr (NextDivisible {n'} {d' = 2} curr) = (contr_curr curr)

Ага, параметры связались. Но теперь мы сломали паттерн‑матчинг:

While processing left hand side of proofNextNotDivBy3. Can't match on ?n' [no locals in scope] (Non linear pattern variable).

Очевидно что простое изменение имени параметра в контексте (с n' на что‑нибудь другое) ситуацию с нелинейностью не спасет. Ошибка в левой части определения функции... У меня плохое предчувствие, но ok, раз унификатор в сопоставлении с образцом не справляется, давайте «перенесем задачу» в правую часть определения:

proofNextNotDivBy3 : Not (Divisible (S n') 3) -> Not (Divisible (S n' + 3) 3)
proofNextNotDivBy3 contr_curr proof_next = case proof_next of
                                                (SelfDivisible _) impossible
                                                (NextDivisible curr) => contr_curr curr

Да твою дивизибл! Это еще что должно значить:

While processing right hand side of proofNextNotDivBy3. When unifying:

Divisible (S n') 3

and:

Divisible (S n') 3

Mismatch between: n' (implicitly bound at...) and n'.

После долгих попыток максимально ясно донести до компилятора свою мысль, мы вынуждены признать, что проблема, увы, глубока... Ее корни уходят в работу тайпчекера Идриса с АТД при зависимом паттерн‑матчинге. Все это выглядит как проблема экзистенциализации в GADT. Дело в том, что у нашего типа сложный индекс, вернее, мы делаем его сложным при объявлении типов функций proofNextNotDivBy, когда получаем в них выражения вроде . Тайпчекеру приходится решать уравнения между выражениями индексов разных Divisible, чтобы унифицировать их, и constraint solver в процессе не справляется с этой задачей. Как я ни пытался, никакими сложными replace и rewrite, вынесением вспомогательных лемм, оборачиванием аргументов в лямбды и т. п., ничто не помогало избавиться от экзистенциализации типа индекса Divisible (которая в итоге приводит к неспособности унифицировать термы и получению загадочного Mismatch between: n' and n'). Только превращало код в plumbing, в котором терялся всякий смысл исходного намерения.

Вводим альтернативную спецификацию, показываем эквивалентность

В подобной ситуации программисты на Idris обычно делятся на два типа: тех, кто просто тихо матерится, и тех, у кого по лбу пробегает холодный пот. Но это если вы «нормальный программист» или пишете для работы. Если же вы как и я всей душой любите по ночам отлаживать абстрактный нонсенс, то бинго! Добро пожаловать в удивительный мир систем алгебраических уравнений на типах.

Но подождите! Мы же хотели сделать что‑то весьма простое. Почему мы вообще влезли в проблемы элиминации экзистенциалов GADT?! Или мы что‑то принципиально неправильно делаем?.. Давайте проверим нашу гипотезу. Если мы думаем, что проблема действительно именно в высокой сложности зависимого паттерн‑матчинга на наших Divisible, и возникает она из‑за получения сложных выражений в его индексах… Давайте сделаем вот что: наши делители в Divisible, т. е. знаменатели отношений, делимость которых мы моделируем, всегда остаются предельно просты — 3 или 5 — в них никогда не возникает каких‑то сложных выражений, так давайте на место индексов Divisible поставим их. То есть объявим Divisible как:

data Divisible : (denom : Nat) -> (numer : Nat) -> Type where

, чтобы в итоге получать функции вроде:

proofNextNotDivBy3 : Not (Divisible 3 (S n')) -> Not (Divisible 3 (3 + S n'))

Перепишем быстренько спецификацию и необходимые части нашего ФизБазза и увидим, что… оно работает. ?‍♂️

Какую пользу мы можем извлечь из этого приключения? Важно понять следующее: с использовании инструментария настолько мощного, как теорем‑пруверы или языки программирования на зависимых типах, важность сохранения осмысленности в коде выходит на новый уровень. Как мы говорили выше, теперь наши процедуры — это не просто какие‑то штуки для получения на экране компьютера желаемых эффектов малопонятным до конца образом (чаще всего наш инструментарий используют для программ, которые вообще не имеют ни ввода ни вывода). Это подлинные знания о чем‑то, об устройстве предмета нашего изучения. И чем более осмысленно (что вовсе не обязательно значит «просто»; но сложность кода, если она возникает, должна быть полезной — нетривиальные композиционные паттерны это одно, а тупой plumbing в попытках состыковать квадратное с круглым — совсем другое) устройство наших функций, тем большую ценность представляет код решения. Поэтому, очевидно, что в данном конкретном случае (для этого ФиззБазза) наиболее правильным решением было бы просто переписать спецификацию. Можно было вообще не упоминать все это приключение с proofNextNotDivBy в туториале, но после некоторых размышлений я решил оставить и его, и обе спецификации Divisible в коде. Зачем? Потому что это отличный повод продемонстрировать методы, которые можно применять для решения подобных проблем в более сложных проектах.

То есть давайте представим следующее: мы можем оказаться в ситуации, когда нам важно сохранить спецификацию (или ее часть) в определенном виде. Не просто по техническим причинам, а потому что именно эта ее форма имеет больше всего смысла для предметной области. И вот у нас возникает одновременно две проблемы:

1. нужно чисто технически согласовать разные спецификации между собой;

2. более фундаментальная проблема консистентности общей модели, состоящей из разных спецификаций.

В общем, если мы не хотим превратить наши доказательства в поток такого:

или, еще хуже, скатиться до использования believe_me в попытках с тайпчекером делать выводы через нерефлексивные эквиваленции (? Аристотель завещал в Идрисе использовать только самотождественность через Refl! Хотите, хм, более тонких эгалитарностей? Покупайте Книгу), или, наконец, получить корректную реализацию непонятно чего (из‑за неконсистентности в модели теории домена) — тогда придется включать голову.

Итак, мы хотим строгих формальных доказательств без unsafe постулатов, при этом чтобы они оперировали не abstract nonsense, а «нормальными» понятиями из теории домена, и при этом мы не хотим с нуля все переписывать на новую спецификацию… На помощь спешит (generalized abstract nonsense) теория категорий!

Что мы можем сказать о двух вариантах спецификации делимости, к которым мы пришли? Обе несут одинаковый смысл — что одно число нацело делится на другое, но выражение этого свойства у них несколько различается. В своем исходном виде Divisible говорит, что «numer делится denom'ом нацело», а после изменения — что «denom делит нацело numer». Суть отношения, очевидно, сохраняется. Но меняется некоторое направление действия, которым связаны объекты.

Чтобы убедиться, что мы нигде сами себе не противоречим и можем в разных частях модели (при переходах между доказательствами) использовать наиболее предпочтительное выражение Divisible, мы можем показать формальную эквивалентность данных спецификаций. В идеале — показать их изоморфизм. Но в строгом смысле это должно означать полную синтаксическую эквивалентность термов после применения композиции преобразований, то есть:

Настолько строго у нас здесь не получится. Ключевое различие между типами спецификаций — в валентности (ковариантности/контрвариантности) их индексов относительно конструкторов данных. Это напрямую влияет на то, как будет происходить индукция в доказательствах, использующих эти типы. И выше мы наблюдали ситуацию, в которой не самая удачная стратегия вывода может создать неудобства или проблемы. Поэтому в нашем случае, нам вполне достаточно будет семантической и пропозициональной эквивалентности, то есть чтобы наши спецификации обладали равной вычислительной силой и позволяли делать заключения об одних и тех же свойствах. Можно понимать это как слабый изоморфизм, или просто некоторую формальную гарантию того, что мы в доказательствах сможем оперировать композициями преобразований при переходах от одной спецификации к другой. Все это есть формализация теории предметной области (в нашем случае, делимости), на более сложных задачах и спецификациях это может быть необходимо осуществлять, чтобы иметь возможность работать со сложными моделями.

Попробуем заглянуть внутрь наших понятий. Если рассматривать наши типы как расслоения единого пространства , то в исходном Divisible мы получим , а морфизмы NextDivisible будут: , а в новом типе: Введем категорию , в которой объектами являются предикаты делимости, а морфизмами — отношения порядка между ними на структуре слоя... Так, стоп, стоп! Уже слишком поздно, и у нас вообще-то практический туториал. Короче, нет времени объяснять: диаграммы категорий наверное коммутируют, значит, мы сможем показать эквивалентность.

Итак, альтернативная спецификация будет иметь вид:

data Divisible_Op : (denom : Nat) -> (numer : Nat) -> Type where
        SelfDivisible_Op : {x'     : Nat} -> Divisible_Op (S x') (S x')
        NextDivisible_Op : {d', n' : Nat} -> Divisible_Op (S d') (S n') -> Divisible_Op (S d') (S d' + S n')

Используя ее, мы, наконец можем построить необходимые логические переходы:

proofNextNotDivBy3_Op : Not (Divisible_Op 3 (S n')) -> Not (Divisible_Op 3 (3 + S n'))
proofNextNotDivBy3_Op contr_curr proof_next with (proof_next)
     _ | SelfDivisible_Op impossible
     _ | (NextDivisible_Op curr) = contr_curr curr

proofNextNotDivBy5_Op : Not (Divisible_Op 5 (S n')) -> Not (Divisible_Op 5 (5 + S n'))
proofNextNotDivBy5_Op contr_curr proof_next with (proof_next)
     _ | SelfDivisible_Op impossible
     _ | (NextDivisible_Op curr) = contr_curr curr

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

forwardEqDivisible : Divisible n d -> Divisible_Op d n
forwardEqDivisible SelfDivisible                   = SelfDivisible_Op
forwardEqDivisible (NextDivisible {n'} {d'} p)     =
   rewrite plusCommutative (S n') (S d') in NextDivisible_Op (forwardEqDivisible p)

backwardEqDivisible : Divisible_Op d n -> Divisible n d
backwardEqDivisible SelfDivisible_Op               = SelfDivisible
backwardEqDivisible (NextDivisible_Op {d'} {n'} p) =
   rewrite plusCommutative (S d') (S n') in NextDivisible (backwardEqDivisible p)

Можно было бы далее объединить спецификации единым интерфейсом, так как, по сути, они представляют собой различные представления (view). Но мы ограничимся тем, что реализуем логические переходы по исходной спецификации (которые используются в разрешающих процедурах) с помощью композиций преобразований, и на этом реализация логического модуля ФиззБазза будет завершена:

proofNextNotDivBy3 : Not (Divisible (S n') 3) -> Not (Divisible (S n' + 3) 3)
proofNextNotDivBy3 contr_curr proof_next =
     proofNextNotDivBy3_Op (contr_curr . backwardEqDivisible) proof_next_op where
          proof_next_op : Divisible_Op 3 (3 + S n')
          proof_next_op =
              rewrite (plusCommutative 3 (S n')) in (forwardEqDivisible proof_next)

proofNextNotDivBy5 : Not (Divisible (S n') 5) -> Not (Divisible (S n' + 5) 5)
proofNextNotDivBy5 contr_curr proof_next =
     proofNextNotDivBy5_Op (contr_curr . backwardEqDivisible) proof_next_op where
          proof_next_op : Divisible_Op 5 (5 + S n')
          proof_next_op =
              rewrite (plusCommutative 5 (S n')) in (forwardEqDivisible proof_next)

Строим программу. Верифицируем поведение

Итак, с основной логикой мы разобрались. Теперь напишем, собственно, саму игру. Давайте посмотрим на спецификацию процедуры игрового процесса:

playFizzBuzz : (first : Nat) -> (last : Nat) -> IO ()

Мы уже говорили, что это слишком размытая спецификация, она, по сути, никак не контролирует возможное устройство процесса. А какие гарантии мы хотели бы обеспечить для нашего ФиззБазза? Для начала, неплохо бы понимать, что наш процесс в принципе завершится. По условию задачи, мы должны пройти по некоторому диапазону чисел в определенном направлении. Чтобы процедура была завершимой, нам нужно гарантировать в этом движении конечное число шагов, то есть границы и направление должны быть определены корректно. Поэтому, если мы собираемся идти от начального числа до конечного по возрастанию, очевидно, мы должны потребовать, чтобы начальное число было меньше конечного или равно ему (тогда будем считать, что в игре мы должны сделать ровно один шаг):

playFizzBuzz : (first : Nat) -> (last : Nat) -> {auto p : LTE first last} -> IO ()

Мы вводим неявный параметр — терм типа , то есть доказательство свойства . Ключевое слово auto на неявном параметре — просьба компилятору Идриса попробовать найти значение аргумента самостоятельно. У такого поиска в Idris есть своя специфика и настраиваемые параметры (см. описание в документации), не будем в это сейчас подробно углубляться, скажем только, что мы здесь делаем это лишь для удобства: если Идрис сам найдет или построит необходимое доказательство — отлично, если у него не получится — ничего страшного, программист просто должен будет сам предоставить требуемый терм. С таким условием мы теперь можем попробовать построить процедуру игры. Покажем один из возможных вариантов, с использованием рекурсии:

playFizzBuzz : (first : Nat) -> (last : Nat) -> {auto p : LTE first last} -> IO ()
playFizzBuzz n last with (decEq n last)
     _ | Yes _       = do displayResult n; pure ()
     _ | No  notLast = do displayResult n;
                          playFizzBuzz (S n) last {p = proofNextLTELast} where
                          proofNextLTELast = case isLT n last of
                               Yes proofLT => proofLT
                               No  contrLT => let
                                              proofGTE = notLTImpliesGTE contrLT
                                              isLast   = antisymmetric p proofGTE
                                              in absurd (notLast isLast)

Здесь мы используем разрешимое сравнение decEq, чтобы проверить, должны ли мы идти вглубь рекурсии, или данный шаг игры будет последним. Сам паттерн процедуры достаточно простой, интереснее посмотреть на то, как мы строим доказательство, что мы не оказываемся за границами допустимого диапазона. Процедура изначально может быть запущена только с наличием терма , а при рекурсивном вызове на шаге мы должны предоставить новый . Мы делаем это следующим образом: из результата decEq мы уже имеем терм , который утверждает, что n не равен last. Тогда мы осуществляем проверку isLT n last, которая разрешается либо в терм , который утверждает, что n строго меньше last, тогда из этого мы получаем исходно требуемое утверждение . Либо мы рассматриваем случай, что (после проверки isLT) n «вдруг оказался» больше или равен last (это следствие из ответа No нам показывает notLTImpliesGTE). Но тогда мы одновременно имеем два терма: изначальный утверждает, что , а  утверждает, что .

Антисимметричность этих свойств дает нам утверждение, что n равен last. Мы пришли к противоречию с термом , с которого начинали рассуждение в данной ветви, что означает невозможность ситуации, которую мы рассматриваем. Технически, требуемый терм типа мы здесь получаем согласно принципу «Ex falso quodlibet», что реализует функция absurd: она требует терм ненаселяемого типа, а выдает все, что пожелаешь. Это как бы такой функциональный аналог impossible, только impossible снимает необходимость самого определения, а absurd освобождает от необходимости завершить доказательство, когда мы уже находимся в процессе определения.

Выглядит как вполне корректная, всегда завершающаяся процедура. Однако, чтобы убедиться в этом, включим в самом начале нашей программы директиву %default total, и Идрис нам отвечает, что…

playFizzBuzz is not total, possibly not terminating due to call to Main.with block in playFizzBuzz;

with block in playFizzBuzz is not total, possibly not terminating due to recursive path Main.playFizzBuzz → Main.with block in playFizzBuzz → Main.playFizzBuzz → Main.with block in playFizzBuzz

В рамках установленных правил, Идрис не признает функцию тотальной, так как по ходу рекурсивных вызовов у нас не уменьшается ни один аргумент, и вся цепочка не сводится явно к некоторой базе с нулем, иначе говоря, наша рекурсия не well‑founded. Очевидно, что это дело техники — переписать процедуру так, чтобы структурно получить определения для случаев и по параметру рекурсии. Попробуйте самостоятельно сделать это каким‑нибудь способом, который вам больше нравится (но сохранив спецификацию в виде границ first и last, и с условием прохождения проверки тотальности). Мы же сейчас пойдем дальше, и усилим спецификацию игровой процедуры в целом.

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

calcFizzBuzz : (first : Nat) ->
               (last  : Nat) ->
               {auto 0 p : LTE first last} ->
               Vect (S (last `minus` first)) (n ** GameState n)

Теперь это процедура, которая только вычисляет игру. Она возвращает вектор, содержащий необходимое количество шагов считалки, которые представляются типом n ** GameState n. До этого в туториале мы видели множество примеров одного вида зависимых типов — зависимых функций. Тип элементов вектора‑результата calcFizzBuzz — это другой вид зависимых типов: зависимая пара. Это так называемый «сигма‑тип», который выражает квантор существования: в зависимой паре тип ее второго элемента зависит от значения первого, что в предикатной логике соответствует утверждению «существует такое значение [первый элемент пары], что некоторое свойство [второй элемент] истинно». Для нас это означает, что мы построим вектор, состоящий из пар число‑вопрос ** ответ считалки. Это позволит нам показывать определенные свойства процесса игры, который мы строим.

Вот определение:

calcFizzBuzz : (first : Nat) ->
               (last  : Nat) ->
               {auto 0 p : LTE first last} ->
               Vect (S (last `minus` first)) (n ** GameState n)
calcFizzBuzz first last = map (\n => (n ** gameLogic n)) (vectNatFromTo first last)

То есть мы строим вектор чисел‑вопросов и отображаем на него функцию, связывающую числа с вычисляемыми на них ответами ФиззБазза. Такой вид результата позволит доказать, что все необходимые числа были посчитаны. Также возможно будет доказать корректный порядок ответов. Но эти доказательства мы оставим за рамками данного туториала.

Сама же функция vectNatFromTo и представляет собой процесс прохода по считалке:

vectNatFromTo : (start : Nat) ->
                (end   : Nat) ->
                {auto 0 p : LTE start end} ->
                Vect (S (end `minus` start)) Nat
vectNatFromTo start end = go start (end `minus` start) where
                          go : (cur : Nat) -> (steps : Nat) -> Vect (S steps) Nat
                          go cur Z     = [cur]
                          go cur (S k) = cur :: go (S cur) k

В целях оптимизации, можно было бы сделать этот процесс прохода ленивым (поскольку calcFizzBuzz — просто отображение логики игры на этот процесс). Вот теперь мы получили осмысленную модель процесса: строим процесс ходов в игре и отображаем на него игровую логику. Обе функции проходят проверку тотальности.

Что же, осталось явить наш ФиззБазз миру:

writeFizzBuzz : Vect (S l) (n ** GameState n) -> String
writeFizzBuzz Nil impossible
writeFizzBuzz states = foldr writer "" states where
                             writer : (n ** GameState n) -> String -> String
                             writer (num ** state) next = let line = 
                               [padLeft 5 ' ' (show num), " => ", show state, "\n"]
                                                          in joinBy "" line ++ next

Это одна из возможных реализаций. Добавим только, что, при желании, ее тоже можно верифицировать (специфицировать вывод и доказать соответствие ему получаемых результатов), оптимизировать, и более гибко настроить! Главное, что мы сейчас показали — четкое разделение всей программы на:

• игровую логику

• игровой процесс (проход по считалке + вычисление ответов)

• формирование результата

• наконец, передача результата во «внешний мир» (вместе со сборкой всех этапов в единое целое)

Последний шаг выглядит следующим образом:

main : IO ()
main = putStrLn (writeFizzBuzz (calcFizzBuzz 1 100))

Попробуйте запустить игру в неправильном направлении:

main = putStrLn (writeFizzBuzz (calcFizzBuzz 100 1))

Компилятор такое не пропустит:

While processing right hand side of main. Can't find an implementation for LTE 100 1.

Если захотите исследовать далекие состояния считалки, рекомендуется явно передавать терм доказательства, чтобы не мучить компилятор:

main = putStrLn (writeFizzBuzz (calcFizzBuzz 1090901 1091001
                               {p = lteReflectsLTE 1090901 1091001 Refl}))

Подведем небольшие итоги. Мы добились того, что наша программа:

1. строго специфицирует задачу (и позволяет настраивать эту спецификацию)

2. гарантирует отсутствие состояний с неверной логикой игры

3. гарантирует завершающийся процесс и некоторые его свойства (правильные границы игры и направление прохода по ней; как уже было сказано, эту часть можно усилить, показав необходимые инварианты относительно чисел-вопросов и результатов-ответов)

Необходимо упомянуть о некоторых ограничениях, которые пока присутствуют в Idris 2 (помимо уже упомянутой выше проблемы с totality checker):

1. rewrite не работает на зависимых типах. Это объясняет, почему у нас не получалось помочь тайпчекеру унифицировать термы при реализации процедур proofNextNotDivBy

2. в настоящий момент система типов Idris 2 не реализует принцип кумулятивности. Да, мы все это время работали в системе, в которой . Что кагбэ намекаэ...

Звучит как ФиззБазз. Если вы дочитали этот пост до конца, поздравляю, вы прошли посвящение в Орден Оверинжиниринга Программ! Да-да, именно про него, равно как и про ФиззБазз и TDD (вы знаете, которое), обязательно спрашивают в наше время на любом собеседовании в программисты.

А если серьезно, то в завершение хотелось бы сказать следующее. Производительность? Простота, читаемость? Расширяемость? Безусловно, важны. Но есть ли во всем этом смысл, если программа делает не то, что нужно? Современная разработка нуждается в сдвиге парадигмы: на первое место должна выйти доказуемая корректность программного обеспечения — способность гарантировать, что наш код исполняет именно то, что мы от него ожидаем. И речь идет о самой широкой практике, а не о каких-то особенных специальных областях «где это необходимо». Сколько можно гадать, когда настанет тот день, где мы вместо ожидаемого вывода увидим окошко с красным крестом, или того хуже, белую эпитафию на синем экране? Зачем нужны тысячи приложений с разным дизайном, если среди них нет ни одного абсолютно надежного? Перестаньте доверять и проверять. Начните доказывать.

Всех с днем программиста! Интересной и осмысленной вам разработки. Спасибо за внимание, Хабр, удачи и до новых встреч!

Код туториала на ГитХаб: https://github.com/knight-of-calculus/total_fizzbuzz.git