The range of total computable $\mathbb{N} \to \mathbb{N}$ functions definable in a type theory corresponds to the proof-theoretic strength of the theory.
There is no total language for all total computable $\mathbb{N} \to \mathbb{N}$ functions. This is a constructive analogue to Gödel's second incompleteness theorem. If such a language existed, it would also contain its self-interpreter function for a suitable $\mathbb{N}$-encoding of programs, but that would make it possible to write general recursive programs, contradicting totality.
For some type theories, the range of definable functions can be concisely characterized by an ordinal number. In this case, we have an ordinal number $\alpha$ such that the fast-growing function $f_{\alpha} : \mathbb{N} \to \mathbb{N}$ grows faster than any definable function in the theory. Here's a listing of ordinals for some type theories.
For any type theory with an impredicative universe, no proof-theoretic ordinal is known. Here the strength of the theory can be explained by comparison to other systems. As Dan Doel mentioned, System F (a non-dependent stratified theory with an impredicative universe) has the same strength as second-order arithmetic.
Simple type theory with $\mathbb{N}$ is also known as Gödel's System T, and has strength $\epsilon_0$. This is stronger than primitive recursive arithmetic; the Ackermann function is definable in System T but not in PRA. The System-T-definable functions are also precisely the functions which are provably total in Peano Arithmetic. Calling the recursion principle of System T (or HoTT) "primitive recursion" is a bit confusing, because it's not the same thing as the recursion principle in PRA.
Infinitary inductive types (such as W-types) increase strength in predicative theories significantly. Intuitively, that's because their induction principles immediately provide a form of transfinite induction.
Is there a total computable function ℕ→ℕ which cannot be formed from
the above "generalized" primitive recursion?
It depends on what other features are supported in the type theory. If we only have $\mathbb{N}$ and functions, $f_{\epsilon_0}$, Goodstein sequences and hydra games are examples for undefinable functions. If we have infinitary inductive types (or W-types), we get a power boost and we can easily define these functions. For example, in Agda we can define $f_{\epsilon_0}$ in the following way:
data ℕ : Set where
zero : ℕ
suc : ℕ → ℕ
data O : Set where
zero : O
suc : O → O
lim : (ℕ → O) → O -- ℕ-branching node (infinitary)
iter : {A : Set} → ℕ → (A → A) → A → A
iter zero f a = a
iter (suc n) f a = f (iter n f a)
f : O → ℕ → ℕ
f zero n = n
f (suc α) n = iter n (f α) n
f (lim g) n = f (g n) n
_+_ : O → O → O
α + zero = α
α + suc β = suc (α + β)
α + lim f = lim (λ n → α + f n)
_*_ : O → O → O
α * zero = zero
α * suc β = (α * β) + α
α * lim f = lim (λ n → α * f n)
_^_ : O → O → O
α ^ zero = suc zero
α ^ suc β = (α ^ β) * α
α ^ lim f = lim (λ n → α ^ f n)
ω : O
ω = lim (λ n → iter n suc zero)
fε₀ : ℕ → ℕ
fε₀ = f (lim (λ n → iter n (ω ^_) ω))
Best Answer
This can be written as $$\phi(m,n)=\begin{cases} h^{\circ n}(g(m-n))&m>n\\ h^{\circ m}(f(n-m))&m\le n \end{cases}$$ so in terms of (positive) difference, case distinction, and simple recursion.