Covalue

3 ноября выступил с докладом на семинаре PSSV'23 по теме, которой интенсивно занимаюсь последние пару месяцев - guarded recursion (склоняюсь к переводу "отложенная рекурсия"). Сделаю тут небольшой конспект, более подробную информацию можно найти на слайдах и в github-репе.

Вкратце, идею отложенной рекурсии можно охарактеризовать как исчисление "задумок" (thunks), восходит она к модальным логикам доказуемости (система Гёделя-Лёба и подобные ей). В guarded системе типов отложенное вычисление, возвращающее A, обозначается как ▷A. Этот конструктор типов оснащен структурой аппликативного функтора, т.е., в качестве базовых операций мы можем отложить вычисление на один шаг (next : A → ▷A) и применить на следующем шаге функцию к аргументу (ap : ▷(A → B) → ▷A → ▷B). Основная же рабочая конструкция - это оператор (уникальной) отложенной неподвижной точки fix : (▷A → A) → A. С программистской точки зрения он ведет себя как рекурсия, возвращающая после каждой итерации контроль вызывающей стороне, что позволяет записывать тотальные алгоритмы в продуктивном виде, т.е., как потенциально бесконечную серию завершающихся вычислений, которая может быть прервана после каждого шага. Потенциально незавершающиеся вычисления на практике встречаются повсеместно - это всевозможные серверные программы и потоковые преобразования данных.

Классические структуры, которые можно определить с помощью отложенной рекурсии это:
* бесконечные потоки (streams)
* ко-списки (т.е., последовательности, могущие быть как конечными, так и бесконечными)
* расширенные числа Пеано (где есть терм для ∞)
* partiality monad (монада частичности, т.е., некоторое значение, получение которого отложено на неопределенное количество шагов, от 0 до ∞)

Применения отложенной рекурсии можно концептуально разделить на два класса: работа с бесконечными структурами напрямую и кодирование нестрогопозитивных рекурсивных типов. В качестве представителя первого класса можно привести определение и верификацию алгоритма Бёрда replaceMin, и его дальнейшие обобщения до MonadFix / value recursion. Нестрогопозитивные же определения можно продемонстрировать на примере алгоритма Хофманна для обхода дерева в ширину, вообще, такие конструкции (+ упомянутая монада частичности) часто всплывают при работе с моделями ЯП методом логических отношений и построении денотационных семантик. На этих идеях основано молодое направление ТЯП под названием (synthetic) guarded domain theory, где любой тип одновременно является доменом - это позволяет значительно упростить работу, избавившись от многочисленных доказательств "доменности".

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

GitHub

GitHub - clayrat/guarded-cm: Experiments with guarded recursion

Experiments with guarded recursion. Contribute to clayrat/guarded-cm development by creating an account on GitHub.

www.tgoop.com/covalue/77

1.4K viewsNov 24, 2023 at 08:37

3 ноября выступил с докладом на семинаре PSSV'23 по теме, которой интенсивно занимаюсь последние пару месяцев - guarded recursion (склоняюсь к переводу "отложенная рекурсия"). Сделаю тут небольшой конспект, более подробную информацию можно найти на слайдах и в github-репе.

Вкратце, идею отложенной рекурсии можно охарактеризовать как исчисление "задумок" (thunks), восходит она к модальным логикам доказуемости (система Гёделя-Лёба и подобные ей). В guarded системе типов отложенное вычисление, возвращающее A, обозначается как ▷A. Этот конструктор типов оснащен структурой аппликативного функтора, т.е., в качестве базовых операций мы можем отложить вычисление на один шаг (next : A → ▷A) и применить на следующем шаге функцию к аргументу (ap : ▷(A → B) → ▷A → ▷B). Основная же рабочая конструкция - это оператор (уникальной) отложенной неподвижной точки fix : (▷A → A) → A. С программистской точки зрения он ведет себя как рекурсия, возвращающая после каждой итерации контроль вызывающей стороне, что позволяет записывать тотальные алгоритмы в продуктивном виде, т.е., как потенциально бесконечную серию завершающихся вычислений, которая может быть прервана после каждого шага. Потенциально незавершающиеся вычисления на практике встречаются повсеместно - это всевозможные серверные программы и потоковые преобразования данных.

Классические структуры, которые можно определить с помощью отложенной рекурсии это:
* бесконечные потоки (streams)
* ко-списки (т.е., последовательности, могущие быть как конечными, так и бесконечными)
* расширенные числа Пеано (где есть терм для ∞)
* partiality monad (монада частичности, т.е., некоторое значение, получение которого отложено на неопределенное количество шагов, от 0 до ∞)

Применения отложенной рекурсии можно концептуально разделить на два класса: работа с бесконечными структурами напрямую и кодирование нестрогопозитивных рекурсивных типов. В качестве представителя первого класса можно привести определение и верификацию алгоритма Бёрда replaceMin, и его дальнейшие обобщения до MonadFix / value recursion. Нестрогопозитивные же определения можно продемонстрировать на примере алгоритма Хофманна для обхода дерева в ширину, вообще, такие конструкции (+ упомянутая монада частичности) часто всплывают при работе с моделями ЯП методом логических отношений и построении денотационных семантик. На этих идеях основано молодое направление ТЯП под названием (synthetic) guarded domain theory, где любой тип одновременно является доменом - это позволяет значительно упростить работу, избавившись от многочисленных доказательств "доменности".

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

BY Covalue