Covalue

Hewer, Hutton, [2022] "Subtyping Without Reduction"

https://github.com/brandonhewer/Subtyping

Продолжаем тему субтипизации. Статья выстроена вокруг двух факторизованных кодировок субтипов - 1) сигмы с пропозиционально обрезанным индуктивным семейством и 2) индуктивно-рекурсивной с ограничением на инъективность одновременно определяемой функции; обе кодировки формализованы на кубической Агде. Мотивация - операции на субтипах как правило перевычисляют вшитый предикат, что может сильно замедлять тайпчекинг. В первой половине статьи в качестве рабочего примера берется подтип чётных натуральных чисел и операция сложения на нём.

Суть первой идеи - кодирование предиката, определяющего вхождение в субтип индуктивным типом, с добавлением дорогостоящих операций, замкнутых по предикату (т.е., вышеупомянутого сложения) как "неканонических" конструкторов. Такое добавление выбрасывает семейство из класса prop (т.к. доказательство одного факта теперь можно получить разными термами, например, сложением с нулем), но можно исправить это т.н. prop-обрезанием, т.е. постулированием равенства всех доказательств одного типа высшим конструктором. Для удобства работы можно построить изоморфизм между "каноническим" предикатом четности и факторизованным. Элиминировать из такого предиката назад в natы можно через введение промежуточного сигма-пропа или рекурсией по числам-индексам.

Вторая идея - использовать высшее индуктивно-рекурсивное определение для всего субтипа сразу. Т.е. строим сразу структурно чётные числа со вшитым сложением, одновременно определяя функцию toN для проекции в наты и добавляем высший конструктор для инъективности toN. Тут на словах обрисовывают построение изоморфизма с предыдущим определением, однако доступного кода нет. Пришлось реконструировать его самому на основе последующих разделов (поверх библиотеки cubical-mini): https://gist.github.com/clayrat/7e7e33d72fa2cf19dfe855c90981a41f

Фактически обе техники сводятся к построению DSL для операций на субтипах - блокирование редукции за счет кодирования функций данными и ускоряет тайпчекинг. Далее авторы решают перейти к примеру с конечными упорядоченными множествами Fin, кодируют их как сигму из ната и индуктивного неравенства (с конструкторами 0 < S _ и x < y -> S x < S y), благополучно забывают про первичную мотивацию и дальше работают только с самим типом неравенства - зашивают в него конструкторы для транзитивности и разницы-на-единицу (плюс проп-обрезание), подчеркивают что пруфы над расширенным вариантом сохраняют новые конструкторы, а не "нормализуют" их до двух канонических. Также обещают показать высшеиндуктивно-рекурсивный вариант в коде - но его там тоже нет.

Дальше статья переходит к формализации обобщения первой идеи (IF) через факторизованные (фри)монады над индексированными контейнерами и их морфизмами - это называют "пропозициональной монадой" и строят ее фри-аналог. В качестве очередного примера авторы показывают как построить поверх этой конструкции субтип списков, где элементы попарно связаны заданным пропозициональным отношением. Затем формализуют обобщение второй идеи с высшеиндукцией-рекурсией (IR), называя ее "свободным расширением субтипа", используя файберы на индексированных контейнерах, подробно описывают построение изоморфизма между этой кодировкой и IF, с переносом списочного примера.

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

В качестве родственных подходов статья называет SProp, аннотации стираемости и абстрактные определения. Проблема у первых двух - недостаточная композициональность; у последних - необходимость в дополнительных доказательствах. Как направление для будущей работы указывается задание произвольных равенств между операциями, выработка языка комбинаторов для субтипов и поиск более удобных элиминаторов.

#hott

www.tgoop.com/covalue/75

1.3K viewsAug 25, 2023 at 08:40

Hewer, Hutton, [2022] "Subtyping Without Reduction"

https://github.com/brandonhewer/Subtyping

Продолжаем тему субтипизации. Статья выстроена вокруг двух факторизованных кодировок субтипов - 1) сигмы с пропозиционально обрезанным индуктивным семейством и 2) индуктивно-рекурсивной с ограничением на инъективность одновременно определяемой функции; обе кодировки формализованы на кубической Агде. Мотивация - операции на субтипах как правило перевычисляют вшитый предикат, что может сильно замедлять тайпчекинг. В первой половине статьи в качестве рабочего примера берется подтип чётных натуральных чисел и операция сложения на нём.

Суть первой идеи - кодирование предиката, определяющего вхождение в субтип индуктивным типом, с добавлением дорогостоящих операций, замкнутых по предикату (т.е., вышеупомянутого сложения) как "неканонических" конструкторов. Такое добавление выбрасывает семейство из класса prop (т.к. доказательство одного факта теперь можно получить разными термами, например, сложением с нулем), но можно исправить это т.н. prop-обрезанием, т.е. постулированием равенства всех доказательств одного типа высшим конструктором. Для удобства работы можно построить изоморфизм между "каноническим" предикатом четности и факторизованным. Элиминировать из такого предиката назад в natы можно через введение промежуточного сигма-пропа или рекурсией по числам-индексам.

Вторая идея - использовать высшее индуктивно-рекурсивное определение для всего субтипа сразу. Т.е. строим сразу структурно чётные числа со вшитым сложением, одновременно определяя функцию toN для проекции в наты и добавляем высший конструктор для инъективности toN. Тут на словах обрисовывают построение изоморфизма с предыдущим определением, однако доступного кода нет. Пришлось реконструировать его самому на основе последующих разделов (поверх библиотеки cubical-mini): https://gist.github.com/clayrat/7e7e33d72fa2cf19dfe855c90981a41f

Фактически обе техники сводятся к построению DSL для операций на субтипах - блокирование редукции за счет кодирования функций данными и ускоряет тайпчекинг. Далее авторы решают перейти к примеру с конечными упорядоченными множествами Fin, кодируют их как сигму из ната и индуктивного неравенства (с конструкторами 0 < S _ и x < y -> S x < S y), благополучно забывают про первичную мотивацию и дальше работают только с самим типом неравенства - зашивают в него конструкторы для транзитивности и разницы-на-единицу (плюс проп-обрезание), подчеркивают что пруфы над расширенным вариантом сохраняют новые конструкторы, а не "нормализуют" их до двух канонических. Также обещают показать высшеиндуктивно-рекурсивный вариант в коде - но его там тоже нет.

Дальше статья переходит к формализации обобщения первой идеи (IF) через факторизованные (фри)монады над индексированными контейнерами и их морфизмами - это называют "пропозициональной монадой" и строят ее фри-аналог. В качестве очередного примера авторы показывают как построить поверх этой конструкции субтип списков, где элементы попарно связаны заданным пропозициональным отношением. Затем формализуют обобщение второй идеи с высшеиндукцией-рекурсией (IR), называя ее "свободным расширением субтипа", используя файберы на индексированных контейнерах, подробно описывают построение изоморфизма между этой кодировкой и IF, с переносом списочного примера.

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

В качестве родственных подходов статья называет SProp, аннотации стираемости и абстрактные определения. Проблема у первых двух - недостаточная композициональность; у последних - необходимость в дополнительных доказательствах. Как направление для будущей работы указывается задание произвольных равенств между операциями, выработка языка комбинаторов для субтипов и поиск более удобных элиминаторов.

#hott

BY Covalue