Исследовательская группа

Лаборатория языковых инструментов

Обобщенные преобразователи типизированных данных

October 19

В докладе рассматривается разбиение рекурсивно определённых функций над алгебраическими типами данных на несколько классов (катаморфизмы, анаморфизмы, параморфизмы, хиломорфизмы). Каждый из этих классов предполагает свою схему рекурсии, выразимую как функция высшего порядка. Мы явно выделим эти схемы в некоторых распространённых базовых функциях и докажем их интересные свойства.

Это движение в сторону Squiggol-стиля функционального программирования. Он предполагает большее использование очень абстрактного кода (например схем рекурсий), свойства которого заранее формально доказаны, что помогает в дальнейшем верифицировать программу целиком.

Докладчик: Игорь Жирков.

Материалы