Recursion Schemes in Agda

Question

Needless to say, the standard construction in 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 

is awesome and extremely useful.

Trying to define a similar thing in Agda (I'll put it just for completeness sake)

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

fails because f is not necessarily strictly positive. This makes sense -- I could easily get a contradiction from this construction by picking appropriately.

My question is: is there any hope of encoding recursion schemes in Agda? Has it been done? What would be required?

Daubigny

At POPL this year, there was a presentation about encoding Data Types à la Carte in Coq. They describe a Coq-friendly alternative for the Fix construction, though I must confess that I don't understand it fully yet. Here's a link to their implementation: cs.utexas.edu/~bendy/MTC/index.php – Mcgrody

The Meta-theory à la Carte page has moved to people.csail.mit.edu/bendy/MTC – Pip

Answer 1

You'll find such a development (over a restricted universe of functors) in Ulf Norell's canonical Agda tutorial!

Unfortunately not all the usual recursion schemes can really be encoded because all the "destructiony" ones consume data and all the "constructiony" ones produce codata, so the notion of feeding one into the other is necessarily partial. You could probably do it all in the partiality monad but that's rather unsatisfactory. That is more or less what the categorists are doing when they say that Haskell's "true category" is CPO⊥ though, because its initial algebras and terminal coalgebras coincide.

Burgage

Thanks -- characterizing the polynomial functors is how I thought you might do it. I was curious if there was a more general way, but it looks like at least it's not present in the folklore. – Daubigny

I think a more general way would need a way to annotate your f : Set -> Set saying that it is strictly positive in its argument. Mini Agda has support for that, with an annotation like f : ++Set -> Set. It also has lots of other fancy annotations that could make things more interesting :) – Burgage