They consist of a collection of functions in all pure finite types.
The primitive recursive functionals are important in proof theory and constructive mathematics.
They are a central part of the Dialectica interpretation of intuitionistic arithmetic developed by Kurt Gödel.
An object of type 0 is simply a natural number; it can also be viewed as a constant function that takes no input and returns an output in the set N of natural numbers.
The primitive recursive functionals are the smallest collection of objects of finite type such that: