От зависимых типов к гомотопической теории типов на Scala + Shapeless + ProvingGround

Всем привет. Хочу поделиться своим опытом использования библиотеки ProvingGround, написанной на Скале с использованием Shapeless. У библиотеки имеется документация, правда, не очень обширная. Автор библиотеки — Сиддхартха Гаджил из Indian Institute of Science. Библиотека экспериментальная. Сам Сиддхартха говорит, что это пока не библиотека, а «work in progress». Глобальная цель библиотеки — брать статью живого математика, парсить текст, переводить естественный язык с формулами в формальные доказательства, которые мог бы чекать компилятор. Понятно, что до этого еще очень далеко. Пока что в библиотеке можно работать с зависимыми типами и основами гомотопической теории типов (HoTT), (полу-) автоматически доказывать теоремы. Началось все с того, что мне захотелось записать вводный курс по зависимым типам на Скале для конкурса Степика. Не хотелось повторяться, на Идрисе недавно появился хороший курс. Скала была выбрана как один из самых популярных функциональных языков. Погуглил по гитхабу по словам «Скала», «зависимые типы», «HoTT» и наиболее многообещающе выглядела ProvingGround. Сразу дисклеймер — я не утверждаю, что те или иные языки или библиотеки наиболее подходят для программирования с зависимыми типами, автоматического доказательства теорем, работы с HoTT. Можно было взять другие языки или библиотеки — был бы другой курс.

Как известно, Скала — язык с ограниченной поддержкой зависимых типов. Зависимые типы имплементируются в ней (другая точка зрения — эмулируются) с помощью path-dependent типов, type-level значений и имплицитов. Объяснять зависимые типы на голой Скале или Скале плюс Shapeless и погрязнуть в технических деталях типа отличия type members от type parameters (дженериков), имплицитов, path-dependent типов, «Aux» паттерна, type-level вычислений и т.д. не очень хотелось. Поэтому часть курса была на голой Скале, но бОльшая часть практики — на ProvingGround.

Термы и типы

Для задания переменных, термов, типов, функций и т.д. ProvingGround предоставляет свой DSL . Так можно объявить тип A и переменную a этого типа:

т.е. типичное объявление выглядит как

Напечатать терм «красиво» можно с помощью метода .fansi , вывести его тип — с помощью .typ :

Можно задать переменную детальнее:

Здесь A — это тип в библиотеке ProvingGround, т.е. HoTT -тип, а Term — это тип в Скале.

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

То, что эта строчка компилируется, означает, что тип указан правильно.

Зависимые типы

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

Так можно задать зависимый тип Ba , который зависит от значений типа A , и переменную этого типа:

Функции

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

Часть проверки типов осуществляется в рантайме, но часть информации о типах видит и компилятор Скалы:

Здесь зависимый функциональный тип из ProvingGround/HoTT компилятор Скалы видит как обычную функцию в Скале.

Индуктивные типы

Можно задавать индуктивные типы. Например, булев тип с конструкторами «истина» и «ложь»:

то есть типичное задание индуктивного типа выглядит как

где конструкторы значений этого типа отделены |: .

Еще пример — тип натуральных чисел с конструкторами «ноль» и «следующее число за натуральным n »:

Тип целых чисел с конструкторами «плюс натуральное n » и «минус натуральное n минус 1» использует уже определенный тип натуральных чисел:

Тип списка значений типа A имеет конструкторы «пустой список» и «список с головой типа A и хвостом типа ListA »:

У типа бинарного дерева (для простоты без значений некоторого типа в узлах) есть конструкторы «лист» и «вилка» (второй принимает пару поддеревьев):

Альтернативно конструктор «вилка» могла бы принимать функцию, которая переводит ложь в одно поддерево, истину в другое:

Зависимые индуктивные типы

Если тип зависимый (indexed inductive type), например вектор Vec или тип-равенство Id , то надо использовать =:: вместо =: , стрелку с тильдой и ссылаться на тип внутри конструкторов (Имя_типа -> Имя_типа(n)) в возвращаемом типе, (Имя_типа :> Имя_типа(n)) в принимаемом типе, а не просто Имя_типа(n) . Например, тип вектора длины n :

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

Действительно, нет способа сконструировать значение типа Fin(zero) . Есть ровно одно значение типа Fin(one) :

Есть ровно два значения типа Fin(two) :

Есть ровно три значения типа Fin(three) :

Семейства индуктивных типов

Несколько слов об отличии семейства индуктивных типов (family of inductive types) от индексированного индуктивного типа (indexed inductive type). Например, List(A) — это семейство, а Vec(A)(n) — это семейство относительно типа A , но индексированный тип относительно натурального индекса n . Индуктивный тип — это тип, конструкторы которого для «следующих» значений могут использовать «предыдущие» значения (как у типов Nat , List и т.д.). Vec(A)(n) при фиксированном A является индуктивным типом, но не является при фиксированном n . В ProvingGround в настоящее время нет семейств индуктивных типов, т.е. нельзя, имея индуктивное определение, например, типа List(A) , легко получить индуктивное определение типов List(B) , List(Nat) , List(Bool) , List(List(A)) и т.д. Но можно эмулировать семейства с помощью индексированных типов:

Можно также определить гетерогенный список ( HList ):

Мы сейчас реализовали собственный HList в библиотеке ProvingGround, которая написана поверх Shapeless, в которой основным строительным элементом является HList .

Алгебраические типы данных

В библиотеке можно эмулировать обобщенные алгебраические типы данных (GADT). Код, который выглядит на Хаскеле

и на чистой Скале

запишется в ProvingGround как

Классы типов

Также можно в библиотеке эмулировать классы типов. Например, функтор:

Можно, например, список объявить экземпляром (instance) функтора:

Можно в класс типов добавить законы:

Типы-равенства

В библиотеке уже есть встроенные сигма-тип (тип зависимой пары), пи-тип (тип зависимой функции, мы его уже видели выше), тип-равенство (identity type):

но можно определить и свой, например, тип-равенство:

Типы-равенства естественно возникают, когда начинается разговор о соответствии Карри-Ховарда. С одной стороны A ->: B — это функции из A в B , с другой — это логическая формула «из утверждения A следует B ». И, с одной стороны, (A ->: B) ->: A ->: B — это тип функции высшего порядка, которая принимает на вход функцию A ->: B и значение типа A и возвращает эту функцию, примененную к этому значению, т.е. значение типа B . С другой стороны, это правило вывода в логике modus ponens — «если верно, что из A следует B , и верно A , то верно B ». С такой точки зрения типы — это утверждения, а значения типов — это доказательства этих утверждений. И утверждение верно, если соответствующий тип населен, т.е. существует значение этого типа. Логическое «и» соответствует произведению типов, логическое «или» — сумме типов, логическое «не» — типу A ->: Zero , т.е. функциям в пустой тип. Так в теории типов возникает логика. Правда, не любая логика, а так называемая интуиционистская или конструктивная, т.е. логика без закона исключения третьего. Действительно, вообще говоря, нельзя сконструировать значение типа PlusTyp(A, A ->: Zero) (если не удалось доказать A , то это еще не значит, что удалось доказать не- A ). Интересно, что справедливо отрицание к отрицанию закона исключения третьего:

Ну так вот, если типы — утверждения, а значения типов — доказательства, то раз равенство двух термов a1 =:= a2 — это утверждение, значит и тип. Тип зависимый, т.к. зависит от значений a1, a2 некоторого типа A . Если a1, a2 разные, то не должно быть способа сконструировать значение этого типа, т.к. утверждение ложно. Если одинаковые, то наоборот должен быть способ сконструировать значение, раз утверждение верно, так что у нашего индуктивного типа единственный конструктор refl(A)(a) !: Id(A)(a)(a) (или a.refl !: (a =:= a) для встроенного типа-равенства).

Еще один полезный тип при доказательстве теорем с неравенствами:

Высшие индуктивные типы

Еще в библиотеке можно работать с высшими индуктивными типами. Например, окружностью

Рекурсия и индукция

Теперь о том, как определять (рекурсивные) функции. Библиотека для каждого индуктивного типа генерирует методы .rec , .induc , т.е. рекурсию (aka рекурсор) и индукцию — элиминаторы в постоянный и зависимый тип соответственно, с помощью которых можно осуществлять сопоставление с образцом (pattern matching), если надо — рекурсивное. Например, можно определить логическое «не»:

Здесь можно считать, что мы сделали сопоставление с образцом:

Проверяем, что всё работает:

Также можно определить логическое «и»:

Здесь можно считать, что мы сделали сопоставление с образцом по первому аргументу:

Можно определить удваивание натурального числа:

Здесь опять можно считать, что мы сделали сопоставление с образцом:

Определим сложение натуральных чисел:

Здесь аналогично можно считать, что мы сделали сопоставление с образцом по первому аргументу:

Определим также конкатенацию векторов:

Здесь мы используем не рекурсию, а индукцию, т.к. нам нужен элиминатор в зависимый тип m

>: (VecA(m) ->: VecA(add(n)(m))) — действительно, этот тип зависит от n из вектора (первый аргумент конкатенации), который мы деконструируем при сопоставлении с образцом:

Покажу еще пример, как теоремы доказываются в ProvingGround. Докажем, что add(n)(n) =:= double(n) .

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

с двумя аксиомами comp_base и comp_loop :

Несколько слов о том, как запускать код на ProvingGround. Есть 3 способа.

📎📎📎📎📎📎📎📎📎📎