Primitive recursive functional

In mathematical logic, the primitive recursive functionals are a generalization of primitive recursive functions into higher type theory. They consist of a collection of functions in all pure finite types.