Which of the following are you asking: are there ways of
enriching the simply-typed $\lambda$-calculus with
mechanisms (presumably by restricting the available forms of
recursion) such that
exactly the terminating programs are typable?
more terminating programs are encodable than with the simple
restriction you are describing in your question?
The answer to (1), as pointed out by Toxaris, is: if you want
type-checking to be decidable, then no. This follows directly
from the uncomputability of the halting problem. The answer
to (2) is positive, and Dave Clarke's answer gives an
example. Indeed there are countless ways of doing so, some
ad-hoc: e.g. if you have a particular (terminating) program $M$
of type $\alpha$ you want to add to the simply-typed
$\lambda$-calculus, you simply add a rule $\Gamma \vdash M :
\alpha$ to your typing system. For a more interesting and
principled way you could look at Barendregt's $\lambda$-cube,
which presents three orthogonal axes of extending the
simply-typed $\lambda$-calculus, all of which make the
simply-typed $\lambda$-calculus strictly more expressive
without losing normalisation. Relatedly, you can look at
induction principles, which are related closely to recursion. Note that this is an active area
of research because the more expressive you make your typing system,
the harder it becomes to prove that the calculus indeed only
types normalising programs.
Note that the problem is usually not to find a fragment of total functions
that we can use to program our terminating programs in. The total
fragments of lambda-calculus given by more expressive parts of the
$\lambda$-cube (e.g. $F_{\omega}$ or the calculus of constructions)
are very expressive. The problem is usually that it is
often inconvenient to encode a terminating program in such a
fragment. R. Harper gives the example of the $gcd$ function computing
the greatest common divisor:
$$
\begin{align*}
\textit{gcd}(m,0) & = m \\
\textit{gcd}(0,n) & = n \\
\textit{gcd}(m,n) & = \textit{gcd}(m-n,n) \quad \text{if}\ m>n \\
\textit{gcd}(m,n) & = \textit{gcd}(m,n-m) \quad \text{if}\ m<n
\end{align*}
$$
It is easy to see that this function terminates, but expressing it
using simple recursion schemes is no fun. Most programs we care
about in daily programming life are terminating for simple reasons and can typically
be encoded using relatively simple recursion schemes (e.g. primitive recursion).
That's why it was a major insight of Ackermann's and Sudan's that primitive
recursion is not enough.
For this reason powerful recursion schemes
(including the unrestricted recursion of most programming languages)
are typically a convenient device to make programming simpler, rather
than necessary for expressivity. Note that in the presence of higher-order functions,
primitive recursion is quite powerful, and enables us to encode e.g. the Ackermann function:
$$
\begin{array}{lcl}
\textit{Ackermann} \ 0 & = & \lambda x. x+1 \\
\textit{Ackermann} \ ( m+1 ) & = & \textit{Iter}\ ( \textit{Ackermann}\ m ) \\
\textit{Iter}\ f\ 0 & = & f\ 1 \\
\textit{Iter}\ f\ ( n+1 ) & = & f\ ( \textit{Iter}\ f\ n )
\end{array}
$$
BTW, the simply-typed $\lambda$-calculus with primitive recursion is also known as Gödel's System T and its expressivity has been studied in great detail and is well understood: we can define exactly the recursive function whose totality can be
proved in first-order logic, starting from the usual axioms for the elementary data
types, eg the Peano axioms for natural numbers.
In this context, you may find the paper Total Functional Programming by DA Turner interesting.
Non-typing work on termination. There's also a lot of ongoing work, both theoretical and implementation oriented, on termination analysis that's
not using (compositional) typing systems, but static analysis
techniques. An example is Microsoft's T2 termination prover.
foo
? The first and second case overlap. Is the first one supposed to take precedence? $\endgroup$