Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

What is the connection between primitive recursion and catamorphisms?

Using the following catamorphism for natural numbers I can implement various arithmetic algorithms whithout having to deal with recursion:

cataNat :: b -> (b -> b) -> Natural -> b
cataNat zero succ = go
  where
    go n = if (n <= 0) then zero else succ (go (n - 1))

fib :: Natural -> Natural
fib = fst . cataNat (0, 1) (\(a, b) -> (b, a + b))

cataNat looks similar to primitive recursion to me. At least each application of it seems garuanteed to terminate, no matter which combination of zero and succ is provided. With each iteration the overall problem is decomposed by the smallest/simplest problem instance. So even if it is technically not primitive recursion it seems to be equally expressive. If this is true it would mean that a catamorphism is not enough to express general recursion. We would probably need a hylomorphism for that. Is my reasoning correct, that is, does the equivalence hold for any type of catamorphism, not just for natural numbers?

like image 223
Iven Marquardt Avatar asked Jun 20 '20 20:06

Iven Marquardt


1 Answers

Primitive recursion corresponds directly to a paramorphism.

You're correct that a catamorphism has equivalent theoretical power to a paramorphism, but they can be different in important ways in operational terms. For an example, let's go to lists instead of Nats.

cata :: b -> (a -> b -> b) -> [a] -> b
cata = flip foldr -- I'm lazy, but this argument order makes a bit more sense for this example

para :: b -> (a -> [a] -> b -> b) -> [a] -> b
para z _ []     = z
para z f (x:xs) = f x xs (para z f xs)

-- Removes the first element from the list which is equal to the other argument
delete1 :: Eq a => a -> [a] -> [a]
delete1 x xs = cata (const []) (\el k found -> if not found && el == x then k True else el : k found) xs False

-- Removes the first element from the list which is equal to the other argument
delete2 :: Eq a => a -> [a] -> [a]
delete2 x xs = para [] (\el raw processed -> if el == x then raw else el : processed) xs

Look at how awkward delete1 is, compared to delete2. Not only do you have to contort your logic by making the result of cata a function, but there's a very real operational cost, too. You have to traverse everything in the list after finding a matching element, and re-create all the (:) constructors. That can have a noticeable cost in efficiency. In comparison, delete2, when it finds the target element, can just use the existing tail of the list for the remainder, without even looking at it. Of course, most uses of foldr (real world, not this example) don't produce a function and don't want access to the unprocessed tail of the list. For them, the catamorphism is going to be slightly more efficient simply because of passing around less data.

So in terms of theoretical power, they're equivalent. In operational terms, each has a use, though catamorphisms are a lot more common.

For some expansion of the idea in more general terms, see the recursion-schemes library. It uses a rather different-looking formulation of the idea so that it can abstract over data types with different shapes, instead of needing a different type for cata/para for each data type they can be applied to. But it really is just an alternate way of packing up the same ideas, and other kinds of morphisms are covered as well, including much more niche (or even possibly useless) ones.

like image 147
Carl Avatar answered Nov 08 '22 09:11

Carl