Схемы рекурсии в Агде

Question

Излишне говорить, что стандартная конструкция в 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 не обязательно строго положительный. Это имеет смысл - я мог бы легко получить противоречие из этой конструкции, выбрав соответствующий.

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

Answer 1

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

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