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