IMPS types are essentially the same as types in Church's simple theory
of types. In Church's system, types are syntactic expressions that
denote sets of objects and that are assigned to formal expressions
(formulas and terms). They have two purposes:
(1) They provide information about the value of an expression: If
the type of an expression E is t, then the value of E is a member of
the denotation of t.
(2) They are used to guarantee, on a purely syntactic basis, that
operators are applied only to the right kind of arguments. For
example, suppose A is of type i (for integer), B is of type r (for
real), F is of type i->i, and G is of type r->r. Then by simply
comparing the types of A, B, F, and G, one can determine that F(A) and
G(B) are legitimate, well-formed expressions (of type i and r,
respectively), but F(B) and G(A) are not legitimate expressions.
The first purpose is very useful in both programming languages and
logics for mechanizing mathematics. This is one reason why some
people prefer a type theory for qed.
The second purpose is quite useful in programming languages, but it
can be a hindrance in logics for mathematics. For example, if the
denotation of type i is the set of integers, the denotation of type r
is the set of real numbers, and integers were considered to be real
numbers, then G(A) would intuitively be a meaningful expression
although it is not well-formed. Moreover, F(B) would also intuitively
be a meaningful expression if B denoted an integer. This is one
reason some people prefer a theory without types for qed.
There are basically two approaches to dealing with the shortcomings of
Church's type system. The first approach, often favored by computer
scientists, is to develop a more sophisticated type theory, with such
things as polymorphism and subtypes. The second approach is to relax
the requirement that the correct matching of operators with arguments
is determined in a purely syntactic way. We have taken the second
approach in developing the IMPS logic. We wanted to remain as close
as possible to standard mathematical practice in which the correct
matching of operators with arguments is, in fact, determined on a
semantic basis.
The IMPS logic is a version of simple type theory that differs from
Church's system in two major ways:
(1) Functions are allowed to be partial and expressions are allowed
to be nondenoting. For example, the function x |-> 1/x is not defined
for 0 and 1/0 is nondenoting. Thus the correct matching of operators
with arguments is determined on a (mostly) semantic basis.
(2) There are certain kinds of subtypes called sorts which, like
Church's types, are syntactic expressions that denote sets of objects
and that are assigned to formal expressions.
Let us now consider how sorts are different from types and how they
relate to partial functions and nondenoting expressions.
Like Church's types, IMPS sorts provide information about the value of
an expression, but in a slightly different way: If the sort of an
expression E is s, then the value of E is a member of the denotation
of s (PROVIDED E IS DENOTING). Unlike Church's types, sorts are
allowed to "overlap". This means that in the IMPS logic one can
assert, for instance, that one sort s1 is contained in another sort s2
by a formula of the form
forall x:s1 . #(x,s2),
where #(E,s) means that E is denoting and its value is contained in
the denotation of the sort s.
Sorts can be used in a much freer way than types. For example,
suppose A is of sort i, B is of sort r, F is of sort i->i, and G is of
sort r->r. Also, suppose that i is a syntactic subsort of r (written
i <= r). As a consequence of i <= r, the denotation of i (say the set
of integers) is a subset of the denotation of r (say the set of real
numbers). Then the sort i->i would denote the set of partial
functions from the integers to the integers; r->r would denote the set
of partial functions from the reals to the reals; and i->i <= r->r.
(The latter relationship makes perfectly good sense since every
partial function from the integers to the integers is also a partial
function from the reals to the reals.) F(A), F(B), G(A), and G(B) are
all well-formed expressions; F(A) and F(B) are of sort i, and G(A) and
G(B) are of sort r. If the value of B were some noninteger, say the
number pi, then F(B) would be well-formed but nondenoting.
Thus we see that sorts are more flexible than types, but they are
still very useful for mechanizing mathematical reasoning. I would
also claim that a logic with partial functions, nondenoting
expressions, and sorts is closer to mathematical practice than a logic
with types in which the correct matching of operators with arguments
is determined purely on a syntactic basis.
The development of IMPS has shown that partial functions, nondenoting
expressions, and sorts are useful and can be effectively implemented
in a simple type theory. They could just as well be useful and
effectively implemented in a first-order logic or even in a set
theory.
Bill Farmer