Is simply typed lambda calculus equivalent to primitive recursive functions It's well known that the computation models untyped lambda calculus and $\mu$-recursive function are equivalent in terms of computability (in fact they are both Turing complete.) It is also well known that, among some of the variations of them, the simply typed lambda calculus ($\lambda_{\rightarrow}$) and the primitive recursive function ($R_p$), are less powerful (i.e. neither of them is Turing complete.)

Since the intuition of the essential restrictions applied in both cases feels similar, I have the instinct that the class of functions computable by either of them is the same, i.e. $\lambda_{\rightarrow} \cong R_p $; but I cannot find any literature discussing this issue myself after a quick search.

Thus, I'd like to ask 1) whether simply typed lambda calculus and primitive recursive function are equivalent and 2) if so, is there any literature that I can have a look at discussing this?
The simply-typed λ-calculus with β-equality at type (o → o) → o → o  (which can be seen as type of the natural numbers, whenever o is any base type) can define exactly the extended polynomials (= polynomials with if-then-else), see (1). Other notions of equality change this. (2) shows that using $\beta\eta$-equality leads to a larger class of definable functions, although no simple
characterisation is given.

Schwichtenberg's result
can be generalised to functions on words over the binary alphabet,
represented as type (o → o) → ((o → o) → o → o), see (3), and also to
free algebras, see (4).





H. Schwichtenberg, Definierbare Funktionen im λ-Kalkül mit Typen.    
M. Zakrzewski, Definable Functions in the Simply Typed λ-Calculus.
M. Zaionc, Word operation definable in the typed lambda-calculus.
M. Zaionc, λ-Definability on free algebras.