Writing lambda calculus higher order recursion scheme in Haskell-CodePudding

[I'm on new grounds here, there might be some ambiguities]

Consider the recursor (which is a generalization of primitive recursion over higher types)

R_\sigma A B 0 = A
R_\sigma A B (S(C)) = B(R_\sigma A B C) C

Where R is of type sigma, A is of type sigma, B is of type sigma -> N -> sigma and C is of type N.

If we take the type of sigma to be a natural number, the recursor is primitive recursion and with it we can define the primitive recursive functions. Now, if we change the type of sigma to be N -> N, we can use R to define functions that outgrow primitive recursive functions, an example being Ackermann function, but all the functions defined will be total. My interest is to understand how the recursor really works, because the concept seems useful in another context.

I came across an article that defines R as above and uses lambda calculus to define the functions of predecessor, addition and multiplication as follows (sorry about the presentation - I don't have reputation to post images)

Pred^{N->N} = R_N 0_N (\lambda a^N b^N.b)
Add^{N->N->N} = \lambda x^N. R_N x(\lambda a^N b^N.S_  a)
Mult^{N->N->N} = \lambda x^N. R_N 0_N(\lambda a^N b^N. Add a x)

After some working on this I was not able to define the functions nor the recursor in Haskell. I tried to define the recursor as a function

rn :: Int -> (Int -> Int -> Int) -> Int -> Int
rn a b 0 = a
rn a b c = b(rn a b (c-1)) (c-1)

But I don't understand, for example, how I can use this to define the multiplication because I don't understand how the parameters should be fed/defined. Should I implement two different functions for the different recursion schemes?

The predecessor seems to work when written like this, and I can get the addition implemented, but multiplication goes over my head.

project2to2 :: Int -> Int -> Int
project2to2 m n = n

predecessor :: Int -> Int
predecessor a = rn 0 project2to2 a

How would one define the recursor and the Pred, Add and Mult functions with it in Haskell?

CodePudding user response：

This seems mainly an issue of concrete syntax:

predecessor :: Int -> Int
predecessor = rn 0 (\a b -> b)

add :: Int -> Int -> Int
add = \x -> rn x (\a b -> 1 a)

mult :: Int -> Int -> Int
mult = \x -> rn 0 (\a b -> add a x)