14

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?

Robin Green
  • 32,079
  • 16
  • 104
  • 187
luqui
  • 59,485
  • 12
  • 145
  • 204
  • 4
    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: http://www.cs.utexas.edu/~bendy/MTC/index.php – Mikhail Glushenkov Feb 05 '13 at 05:12
  • 1
    The Meta-theory à la Carte page has moved to http://people.csail.mit.edu/bendy/MTC/ – Steven Shaw Sep 28 '16 at 10:39

1 Answers1

18

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.

copumpkin
  • 2,836
  • 18
  • 25
  • 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. – luqui Feb 13 '13 at 11:47
  • 2
    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 :) – copumpkin Feb 14 '13 at 04:12