Finally, we say an expression is well typed if there exists some type such that . For example, the program is not well typed since we can't apply 42 to a function expecting (). But the program is well typed because we can build the derivation/proof tree of its typing:
It also happens that these rules, in conjunction with the natural operational semantics defined for this system of simply typed lambda calculus , is sound. Soundness (in the case of this is equivalent to normalization) essentially says that well typed programs do not get stuck.
Finally, we illustrate the analogy between types in and first order logic.
It was noticed some time ago that the judgements within first order constructive/intuitionistic logic look REALLY REALLY similar to judgements for our typing relation. In first order logic, we say
for some logical context and some logical atom , that if all of the logical elements within the context hold/are true, then we can conclude that are also true.
Compare this to the type relation case where
to mean that given the inputs and an expression (such that we can transform these two into a collection of type judgements), then we can satisfy the relation .
Under these same interpretations however, we can get an isomorphic set of rules. For example, the rules for the left/right conjunction rules are respectively
these are both quite similar to a derived typing rule from #1, #2 and our rule
similarly for sum types and function types w.r.t to disjunction and implications
For the disjunction case,
is isomorphic to the typing rules for left and right terms
and the derived case rule
As an exercise to the reader, show the same isomorphism between and .
This then suggests that if it's possible to construct a term in that has a type , then the derivation tree proving that can be directly translated into first order logic as a proof of the logic analog of .