Covalue

Hewer, Hutton, [2024] "Quotient Haskell: lightweight quotient types for all"

Мой порт секций 2+3 на Cubical Agda: source

У субтипов есть дуальная редко используемая, но полезная конструкция - фактор-типы. Для субтипа мы доказываем выполнение предиката при конструировании, а для фактор-типа - при элиминации. Классический пример программистской фактор-конструкции - мультимножества (bags), т.е. списки, факторизованные по перестановке элементов. При работе с такой конструкцией для каждой функции, принимающей bag аргументом, нужно доказывать, что её результат не зависит от перестановок нижележащего списка. Эти пруф-обязательства можно автоматизировать, ограничив логику до SMT-разрешимой. Так мы получаем систему рефайнмент-типов, например автоматизация для субтипов широко используется в LiquidHaskell. Однако, автоматизация для фактор-типов менее изучена, каковой пробел и восполняет статья, вводя расширение LH - QuotientHaskell. Основная идея состоит в переводе эквациональных законов, требуемых функциями на фактор-типах, в предикаты refinement логики. Класс поддерживаемых фактор-типов - quotient inductive types (QIT), где конструкторы индуктивного типа определяются одновременно с уравнениями для данных. Первая часть статьи посвящена трем мотивирующим примерам.

Первый пример - "мобили", бинарные деревья с данными в нодах, факторизованные по зеркальному отражению ветвей (Node l a r == Node r a l). Для создания фактор-типа нужно добавить "высший" конструктор нужного равенства (в гомотопической терминологии - "пути"). В логике QH эти конструкторы становятся обычными равенствами; ключевой момент - терм в левой части уравения должен иметь каноническую (конструкторную) форму. Фактор-определения технически создают новый тип, а не являются рефайнментом старого.

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

Следующий пример - "бум-иерархия": деревья с (опциональными) данными в листьях -> списки -> (конечные) мультимножества -> множества.

* Чтобы получить списка из дерева, нужно факторизовать его по законам моноида (где "сложение" это конструктор ноды). Конкатенация такого фактор-списка имеет константную сложность, т.к. мы просто добавляем новую ноду, не пересчитывая нормальную форму списка - это может быть полезно, когда у нас много подобных операций, а линейное представление списка используется редко. На факторизованных списках работают древесные операции, сохраняющие структуру моноида - sum, map, filter.
* Мультимножества получаются повторной факторизацией по коммутативности "сложения", аналогично мобилям. Это отсекает функции, учитывающие порядок элементов, например, toList.
* Множества получаются окончательной факторизацией по идемпотентности, что запрещающает различать разные вхождения одного и того же элемента. Мы по-прежнему можем использовать функции типа contains, но уже не имеем права подсчитывать количество вхождений.

www.group-telegram.com/us/covalue.com/80

1.0K viewsFeb 10, 2024 at 09:01

Hewer, Hutton, [2024] "Quotient Haskell: lightweight quotient types for all"

Мой порт секций 2+3 на Cubical Agda: source

У субтипов есть дуальная редко используемая, но полезная конструкция - фактор-типы. Для субтипа мы доказываем выполнение предиката при конструировании, а для фактор-типа - при элиминации. Классический пример программистской фактор-конструкции - мультимножества (bags), т.е. списки, факторизованные по перестановке элементов. При работе с такой конструкцией для каждой функции, принимающей bag аргументом, нужно доказывать, что её результат не зависит от перестановок нижележащего списка. Эти пруф-обязательства можно автоматизировать, ограничив логику до SMT-разрешимой. Так мы получаем систему рефайнмент-типов, например автоматизация для субтипов широко используется в LiquidHaskell. Однако, автоматизация для фактор-типов менее изучена, каковой пробел и восполняет статья, вводя расширение LH - QuotientHaskell. Основная идея состоит в переводе эквациональных законов, требуемых функциями на фактор-типах, в предикаты refinement логики. Класс поддерживаемых фактор-типов - quotient inductive types (QIT), где конструкторы индуктивного типа определяются одновременно с уравнениями для данных. Первая часть статьи посвящена трем мотивирующим примерам.

Первый пример - "мобили", бинарные деревья с данными в нодах, факторизованные по зеркальному отражению ветвей (Node l a r == Node r a l). Для создания фактор-типа нужно добавить "высший" конструктор нужного равенства (в гомотопической терминологии - "пути"). В логике QH эти конструкторы становятся обычными равенствами; ключевой момент - терм в левой части уравения должен иметь каноническую (конструкторную) форму. Фактор-определения технически создают новый тип, а не являются рефайнментом старого.

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

Следующий пример - "бум-иерархия": деревья с (опциональными) данными в листьях -> списки -> (конечные) мультимножества -> множества.

* Чтобы получить списка из дерева, нужно факторизовать его по законам моноида (где "сложение" это конструктор ноды). Конкатенация такого фактор-списка имеет константную сложность, т.к. мы просто добавляем новую ноду, не пересчитывая нормальную форму списка - это может быть полезно, когда у нас много подобных операций, а линейное представление списка используется редко. На факторизованных списках работают древесные операции, сохраняющие структуру моноида - sum, map, filter.
* Мультимножества получаются повторной факторизацией по коммутативности "сложения", аналогично мобилям. Это отсекает функции, учитывающие порядок элементов, например, toList.
* Множества получаются окончательной факторизацией по идемпотентности, что запрещающает различать разные вхождения одного и того же элемента. Мы по-прежнему можем использовать функции типа contains, но уже не имеем права подсчитывать количество вхождений.

BY Covalue