Role of Term Constants in Simply Typed Lambda Calculus In the Wikipedia article on Simply Typed Lambda Calculus (among other places), there is a notion of a "term constant".  This is particularly notable in the production grammar given:



In this production grammar, the c is the term constant.  I am new to the simply typed variant of lambda calculus -- I do not understand what role this constant plays in the overall computations of STLC.  Can anyone give some examples of how the term constant is used and explain its general purpose?
As per Sam's request, I rephrase my comment as an answer.

Constants play an important role in λ-calculi (not just the simply typed variant).


They are often convenient: even though we can usually represent our target data using
$\lambda$-terms without constants this tends to be unwieldy. For example
integers 
directly by some variant of an unary encoding, e.g. the Church encoding has $$\lambda g x. \underbrace{g ( g ( ... g ( g\ x ) .. ) ) }_{n}$$ as representation of $n$. That leads to cumbersome, unreadable terms. With constants we can  do arithmetic with 0,1,2,..., and +,−,∗,... 
In a typed calculus, we need  constructors for types, and constants play this rule. E.g. 0,1,2,..., or +,−,∗,...
for the type of integers, true,false... or ∨,∧ for booleans etc. 


Note that the STLC was born with constants : Church's original
formulation contains constants $N_{oo}$, $A_{ooo}$, $\Pi_{o(o\alpha)}$
as well as $\iota_{\alpha(o\alpha)}$, representing negation,
disjunction, universal quantification and the selection operator,
respectively.