Is simply typed lambda calculus equivalent to primitive recursive functions
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.