Proof Assistants Stack Exchange is a question and answer site for mathematicians and computer scientists who develop and use proof assistants. It only takes a minute to sign up.
Sign up to join this community
Is "simple type theory" a folklore, or does it have a formal definition? On nlab, it's only discussed "practically":
In practice any type theory is called a simple type theory if type formation is not indexed, that is the judgment that a type A is well-formed has no other inputs
Do we use simply-typed $\lambda$-calculus and simple type theory interchangeably?
As a matter of modern terminology it's probably fine to identify "simple type theory" with simply typed lambda calculus, or only say STLC. But in the past it did refer to a somewhat specific flavor of type theory so historians may have hair to split on this topic. Below is a quick summary based on the History of type theory on Wikipedia.
In the 1900s, Bertrand Russell comes up with the first theory of types, or type theory as we call it today. Of course, before a century of evolution, it probably looked quite different from what we're familiar with today.
In the 1930s, Alonzo Church comes up with the untyped lambda calculus. Early on were failed attempts at turning that into a logical system. It was more effective as a model of computation, alongside Turing machines.
In the 1940s, Church comes up with the simply typed lambda calculus, as A Formulation of the Simple Theory of Types.
The purpose of the present paper is to give a formulation of the simple theory of types[1] which incorporates certain features of the calculus of λ-conversion.
[1] The simple theory of types was suggested as a modification of Russell's ramified theory of types by Leon Chwistek in 1921 and 1922 and by F. P. Ramsey in 1926.
As an additional bit of historical curiosity, apart from the outdated notation, the STLC is quite recognizable in its original formulation:
(2) if x_β is a variable with subscript β and M_α is a well-formed formula of type α, then (λ x_β M_α) is a well-formed formula having the type αβ; (3) if F_αβ and A_β are well-formed formulas of types αβ and β respectively, then (F_αβ A_β)is a well-formed formula having the type α.
And later, type theory and lambda calculus are further intertwined by Curry-Howard, so that nowadays it's acceptable to just confuse the two. But it may still be reasonable to maintain at least some connotative distinction, saying "type theory" to emphasize on aspects that are more logical and "lambda calculus" to emphasize on those that are more computational.
I share many of the sentiments of Li-yao Xia's answer and I would like to add some context from literature.
For an interesting view of what some people think of, when they say simple type theory (myself included), there is the Seven virtues of simple type theory. Note that this view involves additional equality rules to turn the lambda calculus into fully fledged logic.
Compared to this formulation, what ends up being called simply-typed lambda calculus in many classes about theory of computation omits any mention of equality in my experience. An example of this would be these lecture notes by Ralph Loader, note the distinct lack of equality inference rules. It's more of terms + reductions + a type system over these terms, no internal way of talking about equality.
Here there's another distinction that stands out, beta reduction in this form of STLC tends to be given by a relation built from one-step beta reduction (as in the lecture notes). On the other hand in the Seven virtues of simple type theory beta reduction is a single equality rule with a constraint on free variables and invoking substitution rules instead.
