Esquemas de Recursión en Agda
No hace falta decir, la construcción estándar en 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
Es impresionante y extremadamente útil.
Intentando definir algo similar en Agda (lo pondré solo para completar)
data Fix (f : Set -> Set) : Set where
mkFix : f (Fix f) -> Fix f
falla porquef No es necesariamente estrictamente positivo. Esto tiene sentido, podría fácilmente obtener una contradicción de esta construcción al elegir adecuadamente.
Mi pregunta es: ¿hay alguna esperanza de codificar esquemas de recursión en Agda? Se ha hecho? ¿Qué se requeriría?