Опыт использования Coq на практике, или Как я сам себя отпетушил COQОКОКОКО
Есть время собирать опыт.
Есть время разбрасывать на вентилятор.
Уже довольно давно система типизации в окамле кажется мне слегка недостаточной.
Изменения, привнесённые версией 3.12, кое-как сглаживают этот факт, но, всё равно, этого мало.
Для сугубо практических целей я кое-где использовал "динамическую типизацию" -- а именно, подход, позволяющий иметь "свидетеля" с типом ti 'a, позволяющего закатывать и выкатывать значения между типизированным и нетипизированным:
value ubox : ti 'a -> 'a -> ubox;
value uget_exn : ti 'a -> ubox -> 'a;
Конечно же, с рантайм-ошибкой "не тот тип", если для типа a внезапно есть два разных значения с типом ti a, но на практике у меня было такое только при начальных тестах, а в рабочем коде такого не встречалось.
Более того, я в каждом ti 'a храню ещё разные нужные методы -- сравнение, равенство, хеширование, человекочитаемый вывод, произвольный набор [де]сериализаций, структурную [де]композицию значений (позволяющую немало вышеперечисленного выводить автоматически, хоть и не так эффективно, как в случае честных функций).
Однако, такая типизация -- это не модно, это не гламурно. Скатился в неё только из-за необходимости сделать быстро и рабоче (и, да, оно хорошо работает). Но, думал я, для будущего -- это не дело.
И вот, решил попробовать на практике язык с зависимыми и вообще гламурными типами. Вот это -- модно! Кроме того, меня весьма привлекла возможность подоказывать что-то про код. Учитывая, что хотел использовать это в проекте совместно с кучей другого окамловского кода, разумный выбор был только один: coq.
WIN
После недолгого изучения coq и возможностей экстракции открылась ещё одна хорошая возможность: контролируемо инлайнить вызовы функций. (в одном из предыдущих постов показывал.)
FACTS
В coq есть типы, и каждый тип принадлежит kind'у (виду типа, что ли). Практически полезны два kind'а: Type для типов и значений, и Prop для доказательств (логических утверждений).
Крутые посоны говорят, что Prop является impredicative, однако на практике я что-то не заметил, чтобы это сколько-нибудь мешало для доказательств. А для экстракции кода это помешать не может принципиально, потому что:
WIN
Все значения, имеющие вид Prop, стираются при экстракции. Подобно тому, как в некоторых компиляторах при компиляции стираются типы.
То есть, любые доказательства, любые ограничения на структуры данных, любые хитрости типизации -- всё это обычно в Prop, и стираемость очень радует. Код, который экстрактится в окамл, часто напоминает рукописный код в плане эффективности, либо его можно к таковому приблизить директивами экстракции. И всё, что касается доказательств, работает только в coq.
FACTS
Но есть куча различных мнений про то, как правильно использовать зависимые типы, а как -- неправильно и вообще FFUUUU.
Зависимые типы вызывают необходимость что-то доказывать про код, работающий с этими типам. Как я понимаю, это нормальное явление. А как именно доказывать?
Посоны говорят, что тактики -- это говно для лохов, а риальные посоны выписывают пруф-термы вручную (и вообще, используют agda, где из тактик только аналог coq'овского auto, а, значит, тактики не нужны). Для меня, как для незнакомого с обоими вопросами, потребовались время и ресурсы для того, чтобы разобраться в этом.
Для тех, кто не знает, что такое тактики, я расскажу. Тактики -- это такие директивы, которые пользователь даёт coq'у, находящемуся в "режиме доказательства", для того, чтобы в конце концов осуществить это доказательство. Каждая тактика может видеть контекст, где её применяют, и она осуществляет дописывание текущей цели доказательства каким-то своим кодом (считаем, что каждая цель доказательства -- определённого вида "дырка", куда можно присунуть код, изменив им гипотезы, доказываемый факт, закрыв текущую "дырку" либо породив вместо неё ещё несколько). Потом, по окончании доказательства, проверяется именно код, сгенерированный тактиками, то есть, само по себе использование тактик идёт не на уровне ядра, а является скорее чем-то вроде применения умных макросов, сгенерированный которыми код уже проверяется по всей строгости.
Есть куча различных тактик, есть базовые/примитивные, есть весьма непростые, есть тактики, осуществляющие автоматический поиск термов по определённым правилам ("hint databases"), есть специализированные тактики (например, подходящие для доказательств фактов на целых/действительных числах).
И вот, когда есть доказательство какого-либо непростого факта, доказательство через тактики является вполне таки write-only текстом, что вообще печально. Хотя общую идею доказательства уловить можно. Но это доказательство всегда можно присунуть в coqtop/coqide/proofgeneral и посмотреть, что же на самом деле автор имел ввиду. При использовании чужого кода практической нужды в этом почти нет -- если наличествует модульность, доказательства не нужно изучать, достаточно просто использовать их.
В предыдущих постах кто-то мог заметить, как я строю пруф-терм вручную. Проанализировав готовые построения, свернув мозг в йенг мускусной утки, найдя функции, нужные для построения пруф-терма, у меня всё получилось. "Но постоянно так жить не собираюсь".
Впрочем, избавление от навязчивой идеи "строить пруф-термы вручную" пришло откуда не ждали. А именно, я стал дальше изучать coq и читать литературу по нему.
FAIL
Литература по coq в большинстве случаев касается только доказательств. То ли все исключительно умные и без сопливых разберутся, как использовать coq для программирования, то ли этому вопросу не уделяли достаточно времени. Оказалось, второе. Но нашёлся один человек и уделил таки.
WIN
Adam Chlipala -- "Certified Programming with Dependent Types".
Это -- нечто. Начинается мягко и нежно, засасывает плотно. И вот, избавление от дурацкой идеи о ручном построении пруф-термов пришло из неё. В книге показано, как вести масштабируемую разработку на coq, такую, которая не потребует на каждое изменение типов/логики переписывать руками все доказательства, касающиеся этих типов и этой логики. Достаточно в одном месте переписать тактику, возможно какие-то мелочи подправить, и всё. И весьма многое в книге решено именно тактиками. Особенно там, где речь идёт о серьёзных зависимых типах.
FACTS
Тактики -- мощный инструмент. Плохо в нём то, что его можно случайно использовать во вред. А именно, очень не рекомендуют строить тактиками так называемые "computational terms" -- выражения, которые будут вычисляться. То есть, конечно, можно, если представляете себе, что к чему.
А причина тут в том, что тактики могут сгенерировать неправильный код. Например,
Definition add1 (a b : nat) : nat.
auto.
Defined.
Extraction add1.
(** val add1 : nat -> nat -> nat **)
let add1 a b =
b
Definition add2 (a b : nat) : nat.
exact 0.
Defined.
Extraction add2.
(** val add2 : nat -> nat -> nat **)
let add2 a b =
O
Ну а чо, по типам сходится -- вот и ок.
Тем не менее, тактики очень полезны для следующих вещей:
- работа с Prop (с доказательствами). Обычно доказательства пишутся так, что если хоть какой-нибудь способ сконструировать доказательство есть, то факт считается доказанным. Тут ещё рядом proof irrelevance.
- примитивные случаи вида exists значение -- "дать значение и затем доказать, что оно удовлетворяет данному sigma-типу".
- decide equality: тактика, которая структурно разбирает два значения с целью родить функцию с типом forall (x y : A), {x = y} + {x <> y} (подробнее про decide equality -- ниже).
- тактика refine, берущая скелет кода/доказательства, опционально содержащий "дырки". Данный скелет будет протипизирован, типы будут протащены как надо, а дырки превратятся в очередные цели доказательства. Обычно это имеет смысл, когда в теле refine указано всё, что касается вычислений, а дырки соответствуют доказательствам, требуемым для того, чтобы всё "сошлось". Очень хорошая тактика для написания кода, когда есть как computational terms, так и proof terms.
- простые вещи, в которых ограничений по типам достаточно для того, чтобы вывести терм гарантированно правильно.
Ну, это -- теория. Теперь -- практика.
Проект мой касался генерации примитивных sql-запросов из dsl. На вход подавалась структура данных (разобранная из json over http, и разбор на окамле сделать было чуть разумнее из-за причин, выходящих за рамки этого поста), и на её основании нужно было сгенерить запрос, учитывающий описанную в coq схему базы данных (ту её часть, которая необходима для генерации запроса). В том числе, там были поля с автоматической группировкой и необходимость создавать вложенные sql-запросы, со всякими там алиасами столбцов и их использованием во внешнем запросе.
FAIL
Мне нужны нативные окамловские int, int64, string. А в coq их нет штатным образом. Пришлось описывать их аксиоматически, пригодным для экстракции способом -- "поверьте мне, что есть такой-то тип, и есть такие-то функции над значениями этого типа", и описывать как тип, так и операции над ним в виде обычных строк окамловского кода.
Хоть это и геморно, и местами некрасиво, но вполне реализуемо.
FAIL
Следующая проблема в другом: в coq невозможно создать значение "аксиоматического" типа так, чтобы при экстракции оно было в виде литерала. Например, строковые константы экстрактились в (ocaml_string_of_coq_string ['a' :: ['b' :: ['c' :: ...]]]) (хорошо, что хоть в coq этого говна не надо было, "abc" вполне достаточно для создания этого списка).
Аналогичные проблемы с числами, но там хоть побыстрее: coq умеет представление чисел в виде дерева, содержащего биты числа, и его преобразование в нативное число было всего лишь кучкой логических операций ("или", "сдвиг").
FAIL
Отвратительная работа с записями (records): невозможность объявления взаимно-рекурсивных индуктивного типа данных и типа записи. (обход есть, но тоже отвратительный: представлять запись как Myconstructor : t1 -> t2 -> .. -> myrecord и руками прописывать проекции полей.)
FAIL
Ещё к отвратительному относится отсутствие окамловского { (record) with f1 = v1, f2 = v2, ...} -- копирования записи с изменением некоторых полей.
Ещё плохо, что нет штатной и легковесной возможности для подтипизации записей, но без этого худо-бедно, да можно жить.
FACTS
Зная это, я начал писать код.
Все объявления типов, с которыми хочу осмысленно работать в coq, я должен описать в нём же. Не проблема, но вылилось в типы, параметризуемые другими типами совершенно некрасивым образом. Ну ладно, алиасы типов нам на что.. И явные приписывания типов тоже.
FAIL
Надо как-то собирать проект, внезапно. Тот механизм, который предлагается штатно, coq_makefile, не умеет работать совместно с oasis/ocamlbuild. В топку, значит.
А экстракция в моём случае -- не просто %.v -> %.ml %.mli, а ещё и вытаскивание используемых кусков из coq stdlib, то есть, где-то под 40 дополнительно требуемых ml/mli.
Продолбавшись дня три с плагином для ocamlbuild, выяснил в рассылке, что такие хитрые зависимости ocamlbuild не умеет, а если брать так, как он умеет, то он то ли не пересобирает что-то, то ли ещё какая-то хрень была. Давно было дело, забыл детали.
В общем, решение этой проблемы -- шелл-скрипт, умеющий смотреть, не изменилось ли что, перекомпилировать, экстрактить всю эту срань в определённую директорию в пределах дерева исходников (ни в коем случае не в _build -- ocamlbuild их там не видит, о слепец!). Ну, строчка в .hgignore, строчка в _tags, строчка в _oasis, и проблема решена. Элегантность -- на высшем уровне. Зато скрипт внезапно научился запускать coqide на скомпилированных исходниках, без ручной перекомпиляции зависимостей (.v -> .vo).
FACTS
В моей практической задаче далеко не все запросы являются валидными, это надо проверять в coq-коде, так как именно там описана схема базы данных. Значит нужен способ работы с ошибками.
Есть исключения checked, есть unchecked. Классика в манатках -- checked, где тип манатки включает в себя тип ошибок. Но это плохо сочетается с модульностью -- на границе модулей необходимо перекидывать исключения между разными типами, либо заворачивать/разворачивать.
FAIL
Средствами coq можно только через большую глубокую жопу сделать unchecked exceptions. В #coq мне накодили решение, но оно настолько ональное, что я уж забил на это и решил: хрен с тобой, петушара, будут тебе checked exceptions.
FACTS
Так как coq чисто-функциональный, логичным решением было бы использовать манатки. Error всякий там. А ещё можно было бы использовать тайпклассы, гламурно же!11
Кроме того, при преобразовании запроса нужно следить за генерируемыми идентификаторами, что добавляет манатку State.
А ещё, учитывая необходимость использовать манатки совместно друг с другом, лучше сразу сделать ErrorT и StateT.
Вот что мне тут понравилось -- возможность строго доказать законы манаток и их трансформеров. Сладкое такое дрочево. Ну я же пацан -- я и доказал. Правда вот, использовал "functional extensionality", но для этого кода -- можно. (а в coq 8.4 появляется штатная аксиома про eta-expansion, которой вроде бы хватило для доказательства тут.)
Но я не хотел использовать подход из х-я, где каждая манатка и каждый трансформер заворачиваются в конструктор индуктивного типа данных. Есть предположение (50/50), что это меня и погубило, потому что:
FAIL
Coq слишком умный. Он выводит инстансы тайпклассов весьма хитрыми способами, по непростым критериям, и в некоторых случаях (при минимальном изменении кода) либо не выводит их вообще (не может протипизировать код), либо требует ручного указания "всего, что движется," в типе.
Неделя долботни, и я внезапно понял, что это гнилое дело. В жопу тайпклассы для манаток в coq. Да и lift этот весьма задалбывает.
FACTS
Но тайпклассы для целочисленной арифметики я таки сделал/оставил -- там вполне красиво вышло, и экстрактится/инлайнится в код, компилируемый одинаково с рукописным кодом.
Но, выкинув манатки/трансформеры, задача "иметь ошибки и состояния" осталась при мне. Ещё добавилась задача "быстро склеивать куски текста" (окамловский Buffer), и ещё что-то в том же духе, типа очередей (окамловский Queue, чтобы не чесать себе окасаку).
Задолбавшись с MATAHOM, я решил сделать тупо и цинично. "Мировая манатка". В coq представлена как Wm.w {e} a (ошибки -- e -- implicit argument, значение -- a), окамле значение представлено как type w 'a 'e = unit -> 'a.
Можете спросить, почему 'e является "фантомным типом". А дело в том, что я решил экстрактить throw/catch (и вообще ошибки) в окамловские исключения. А чо, быстро. И вот, с помощью Obj и какой-то матери у меня получилось сделать throw/catch, кидающие/ловящие исключение Coqexn of Obj.t. Корректность использования Obj гарантируется типами в coq-коде. Кроме того, сделал также функцию wm_run : w 'a 'e -> [= `Ok of 'a | `Error of 'e ], и, на удивление, всё работает уже долгие месяцы, несмотря на потенциальную небезопасность подхода.
bind и return "мировой манатки" -- инлайнящиеся куски кода. Например, return : forall a e, a -> @w e a экстрактится примерно в (fun x -> fun () -> x).
bind -- похожим образом, вполне очевидным, только посложнее, и, заметим, никакой обработки исключений в bind, ни в coq-коде, ни в результатах экстракции -- её берёт на себя окамл и его рантайм.
По слухам, ocaml >=4.0 умеет бета-редукцию при компиляции, поэтому этот код будет работать весьма шустро.
Далее, для удобства и для проверки возможностей coq (а именно, notations) я налепил do-нотацию для этой манатки. Если х-ь тыкали х-м, знаете, что это такое. И вот, получилось вполне прилично, как императивщина почти.
Для императивных кусков кода проблема написания их на coq решена.
FAIL
А доказать какие-либо свойства этих императивных кусков -- трудно.
Но это всегда так. Не думаю, что с честными манатками было бы сильно лучше (точнее, было бы лучше, но не сильно). Но пичалька. А библиотеки типа "Ynot" -- не в тему тут вообще никак, замучаешься прикручивать, да и слишком хардкор. Но ещё давно были идеи, как доказать, да трудно и не нужно. То есть, доказательства типа-императивного кода -- вообще мутный вопрос, с функциональщиной тут всяко проще (хотя и там бывает всякое...).
То есть, банальный, но скучный вывод: всё, что требует доказательств (будь то глазами, будь то формальными средствами) -- выносить в функциональный код. Либо помочь мне с идейками про доказуху императивщины в "мировой манатке", как будет желание. Но сомневаюсь в особом смысле этого.
Примерно на этом этапе я решил: буду писать на coq как на чистом ml, при необходимости пользуясь крутыми типами. Вот, так оно и получилось -- места, где есть суровые зависимые типы либо доказательства, не часты в коде данного проекта.
Для некоторых кусков кода мне понадобилось иметь отображение ключа на значение, типа окамловского Map (AVL tree).
FAIL
То дерево, которое поставляют в coq stdlib, хрен используешь. Проблема в непонятных старых/новых версиях реализации этого avl tree, в непонятках, как сделать модуль, приемлемый для функтора, создающего дерево. Там же, как понимаете, необходимо предоставить не только
type t;
value compare : t -> t -> int;
, но и доказательства того, что тот compare является отношением порядка на значениях данного типа.
Для строк подобное было ещё сложнее (сконструировать и доказать), поэтому забросил, только поняв, что предстоит.
В рассылке coq-club был рецепт использования этих деревьев, но уже после того, как я с ними помучился и забил на них. А вместо них я сделал простые ассоциативные списки с гарантией уникальности ключа, вытащенной в тип. Хотя тоже помучился, но весьма мило. Плохо, что до сих пор одно из доказательств ищется единицы секунд при каждой компиляции, но менять тут что-то -- уже сил нет. Может, как отдохну, разве что.
Далее, для ассоциативного списка не обязательно отношение порядка, достаточно отношения равенства (и, разумеется, будет полный проход по списку в общем случае). А как равенство в coq делается?
WIN
Классически -- через функции с типом forall x y : A, {x = y} + {x <> y}. То есть, для двух значений с типом A возвращается сумма возможностей, находящаяся в Type, где каждая из возможностей находится в Prop. Что имеем: если подобная функция вернула значение, его анализ происходит в рантайме, но в coq в каждой из веток (x = y и x <> y) имеем не только факт того, равны ли два значения или нет, но и доказательство их равенства/неравенства. Это было очень полезным для поддержания compile-time инварианта уникальности ассоциативного списка.
А экстрактится это в bool. Как и обещано -- Prop убрали, после стирания остался индуктивный тип данных с двумя конструкторами, не несущими никаких значений.
Я на радостях даже тайпкласс налепил, который предоставлял eq_dec-функции нужным типам. Вполне удобно.
Но проблемы не закончились: учитывая взаимно-рекурсивные определения типов и необходимость их беспорядочной параметризации друг другом, eq_dec-функции (от "decidable equality") должны повторять тот же шаблон параметризации: например, если тип A передаётся как параметр в тип B для реального использования, то eq_dec над A тоже должно передаваться как параметр в eq_dec над B. Но и это ещё не всё.
В coq весьма строгое обращение с завершимостью функций.
FAIL
Для доказательства завершимости функции, в которую передают другую функцию, если эти функции являются рекурсивными, необходима дополнительная проверка того, что результат применения будет завершимым. Минус несколько дней рабочего времени на это. Оказалось, если есть Fixpoint me param recarg := … me param anotherarg …, и param тоже рекурсивная функция, и она передаётся при обращении к func, то это в теории может вызвать проблемы.
Вроде, в coq 8.4 это слегка расслабили.
Но мне приходилось писать что-то вроде
Definition func param : recargtype -> restype :=
(fix self recarg := ... self anotherarg ...)
, чтобы в рекурсивных вызовах участвовал только recarg и его структурно-меньшее порождение anotherarg, тогда как param там не участвовал.
Особенно мучило это в случаях, когда та самая рекурсивная функция -- это eq_dec-подобная функция для определения того, равны ли два значения определённого типа данных, параметризованного другим типом данных с имеющейся своей eq_dec-функцией.
Не уроборос, но близко.
Но coq позволял себе раздумья на десятки минут из-за неаккуратного использования eq_dec-функций, передающихся в другие eq_dec-функции, перед тем, как выдать ошибку. Это плохо.
Однако, теперь я знаю, как правильно это делается.
FACTS
Но есть и ещё подходы к равенству в coq. Например, можно объявить нужные отношения (равенство, эквивалентность, конгруэнтность), и с помощью тайпкласса Equivalence, доказав, что они удовлетворяют рефлексивности, симметричности и транзитивности, использовать эти отношения вместо равенства. Это -- гибче, чем сводить любые сравниваемые элементы до уровня синтаксического равенства или около того. С другой же стороны, полагаясь на эквивалентность, не имеем гарантий именно равенства значений, что иногда бывает полезным.
В качестве развлечения набросал штуку, из отношения классического равенства выводящую инстанс Equivalence. То есть, ничего сложного в целом нет.
(осталось ещё разобраться с дебильным интерфейсом аналога Map и сделать как-нибудь по-нормальному, тоже на подобных тайпклассах, только для другого отношения.)
Есть ещё один подход, касающийся доказательства {равенство} + {неизвестночто} (где "неизвестночто" -- не неравенство, но логически к нему приравнено. Однако, судя по coq-club, пользы не очень много.
И есть ещё вариант: объявить окамловские функции с типом 'a -> 'a -> bool (да хоть структурное равенство, Pervasives.( (=) )), а в типах coq описать сигнатуру именно eq_dec-функции. Таким образом, этот хак позволит родить доказательство равенства/неравенства "из воздуха", но в рантайме это будет всё тот же анализ булевого значения. Но я такое не использовал, некрасиво, да и не везде структурное равенство работает (и не везде оно приемлемо).
А помните моё желание уйти от "значения-свидетеля" и динамической типизации в окамле? Так вот, в coq подобное решается не менее трудоёмко: для каждого типа, будь желание иметь его структурную [де]композицию, необходимо таким же образом описывать либо все конструкторы индуктивного типа данных, либо все поля/компоненты туплов и записей. Разве что, чем хорошо, можно будет статически проверить обратимость композиции и декомпозиции.
FAIL
Ещё хотел сделать кое-что с итератами, которые являются функтором на IO-монадой, и, опять же, придирчивость coq, гарантирующая завершимость, должна была проверить, что в тип данных IO.m 'a параметр 'a входит "строго положительно", а в сигнатуре модуля coq невозможно указать эту "положительность". Ситуация слегка напоминает ко/контра-вариантность в окамле, но там таки есть +'a и -'a.
ВЫВОДЫ
Что стоит писать на coq?
А хрен знает. По крайней мере, уж точно, есть смысл писать куски чисто-функционального кода, для которых неплохо бы иметь зависимые типы и/или доказательства каких-либо фактов об этом коде.
Имея "мировую манатку", я могу писать на coq вещи и побольше.
Что точно пока не буду делать -- использовать библиотеки с развесистым апи. Каждый тип и каждое значение описывать аксиомами -- надорваться можно.
Думал про штуку, которой можно было бы обработать окамловские исходники (видимо, camlp4) и сгенерить нужные аксиомы. Хотя бы по-тупому, без модных типов, но с возможностью дописать эти типы где надо. Было бы круто. Но там не только это надо, ещё надо заворачивать функции с сайд-эффектами в "мировую манатку", делать мрачные извращения с обработкой исключений.
Может, будет интересно, в чём же собственно петушня.
1. Тонны лишнего гемора, времени, ресурсов. Без coq, на окамле, всё было бы сделано гораздо проще.
2. Учитывая излишние затраты времени, оказалось так, что я продолбался с coq в то время, когда были доступны для работы верстальщик, вроде даже js-кодер, и потом, по завершении работы, мне пришлось самому заниматься этим говнищем.
Но и польза от этого тоже есть.
1. Подтянул письменный английский, затратив в сумме сотню часов на быструю формулировку тонн вопросов в #coq irc, несколько писем в coq-club и в их багтрекер.
2. Разобрался с кучей интересных и в будущем полезных вещей.
3. Понял многое про академоту.
4. Появились некоторые планы на будущее относительно coq.
5. Сделал, на худой конец, проект. Всё работает.
По итогу -- впечатления смешанные.