Схемы рекурсии в Agda

Излишне говорить, что стандартная конструкция в Haskell

newtype Fix f = Fix { getFix :: f (Fix f) }

cata :: (Functor f) => (f a -> a) -> Fix f -> a
cata f = f . fmap (cata f) . getFix

это здорово и очень полезно.

Пытаюсь определить аналогичную вещь в Агде (напишу просто для полноты картины)

data Fix (f : Set -> Set) : Set where
    mkFix : f (Fix f) -> Fix f

терпит неудачу, потому что f не обязательно является строго положительным. Это имеет смысл — я мог бы легко получить противоречие из этой конструкции, выбрав соответствующий вариант.

Мой вопрос: есть ли надежда на кодирование схем рекурсии в Агде? Это было сделано? Что потребуется?


recursion haskell recursion-schemes agda catamorphism
person luqui    schedule 05.02.2013    source источник
comment
На POPL в этом году была презентация о кодировании типов данных à la Carte в Coq. Они описывают удобную для Coq альтернативу конструкции Fix, хотя я должен признаться, что еще не полностью ее понимаю. Вот ссылка на их реализацию: cs.utexas.edu/~bendy/MTC /index.php   -  person Mikhail Glushenkov    schedule 05.02.2013
comment
Страница метатеории а ля карт перемещена на people.csail.mit.edu/bendy/ ВТС   -  person Steven Shaw    schedule 28.09.2016

Ответы (1)


arrow_upward
17
arrow_downward

Вы найдете такое развитие (по ограниченному набору функторов) в Канонический учебник по Агде от Ульфа Норелла!

К сожалению, не все обычные схемы рекурсии действительно могут быть закодированы, потому что все "разрушающие" схемы потребляют данные, а все "конструктивные" производят кодовые данные, поэтому понятие ввода одного в другое обязательно частично. Вы могли бы, вероятно, сделать все это в монаде partiality, но это довольно неудовлетворительно. Это более или менее то, что делают категористы, когда говорят, что «истинная категория» Haskell — это CPO⊥, потому что его начальные алгебры и терминальные коалгебры совпадают.

person copumpkin    schedule 05.02.2013
comment
Спасибо - характеристика полиномиальных функторов - это то, как я думал, вы могли бы это сделать. Мне было любопытно, есть ли более общий способ, но похоже, по крайней мере, его нет в фольклоре. - person luqui; 13.02.2013
comment
Я думаю, что для более общего способа потребуется способ аннотировать ваш f : Set -> Set, говоря, что он строго положителен в своем аргументе. Mini Agda поддерживает это с аннотацией типа f : ++Set -> Set. У него также есть много других причудливых аннотаций, которые могут сделать вещи более интересными :) - person copumpkin; 14.02.2013