Рекурсивные схемы в Агда
Излишне говорить, что стандартная конструкция в 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
является удивительным и чрезвычайно полезным.
Попытка определить аналогичную вещь в Agda (я поставлю ее только ради полноты)
data Fix (f : Set -> Set) : Set where
mkFix : f (Fix f) -> Fix f
не выполняется, потому что f не обязательно строго положителен. Это имеет смысл - я мог бы легко получить противоречие из этой конструкции, подобрав надлежащим образом.
Мой вопрос: есть ли надежда на кодирование схем рекурсии в Агда? Это было сделано? Что потребуется?
Ответы
Ответ 1
Вы найдете такое развитие (над ограниченным универсумом функторов) в учебном пособии Ульфа Норелла в Католической Агде!
К сожалению, не все обычные схемы рекурсии действительно могут быть закодированы, потому что все "разрушительные" потребляют данные, а все "конструктивные" производят кодаты, поэтому понятие подачи одного в другое обязательно является частичным. Возможно, вы могли бы сделать все это в монархии пристрастности, но это довольно неудовлетворительно. Это более или менее то, что делают категористы, когда говорят, что Haskell "истинная категория" является CPO ", хотя ее исходные алгебры и терминальные коалгебры совпадают.
