Types Considered Harmful

Leslie Lamport

                   lamport@src.dec.com

Wed 23 Dec 1992 [10:54]

1 Introduction

A mathematician might define len(s) to denote the length of s, for any finite sequence s. Many computer scientists would find this definition naive. They consider len to be a highly polymorphic function, and they believe it can be defined formally only in a language with a sophisticated type system—if it can be defined at all. We show that conventional mathematics can be formalized without the use of types. It is quite easy to define len formally.

Types are so widely accepted in programming languages that most computer scientists have forgotten their drawbacks. Even if the benefits outweigh the drawbacks for programming languages, the same balance need not hold for other domains. We claim that types are not just unnecessary, they are harmful in formalizing mathematics. This claim has implications for the design of specification languages and mechanical theorem provers.

2 Formalizing Mathematics

2.1 Zermelo-Fraenkel Set Theory

The formalism that seems to be most widely regarded as the best foundation for ordinary mathematics is Zermelo-Fraenkel set theory [2]. The particular version of Zermelo-Fraenkel set theory described here will be called ZF. We consider formal definitions, but not formal reasoning, so we will not describe the precise axioms of ZF.

In ZF, one reasons only about sets. Since we want to reason about the number 2, it must be a set. Mathematicians usually don’t think of 2 as a set because they don’t care what its elements are. To be consistent with ordinary usage, we let value be synonymous with the term set of

= ≠ ∈ ∉ ∅ ∪ ∩ ⊆ \ [set difference] {e_{1}, …, e_{n}} [Set consisting of elements e_{i}] {x ∈ S : p} [Set of elements x in S satisfying p] {e : x ∈ S} [Set of elements e such that x in S] 2^{S} [Set of subsets of S] ⋃ S [Union of all elements of S] ⟨e_{1}, …, e_{n}⟩ [The n-tuple whose i^{th} component is e_{i}] S_{1} × … × S_{n} [The set of all n-tuples with i^{th} component in S_{i}]

Figure 1: The operators of set theory.

Zermelo-Fraenkel set theory, and we use set to refer to those values that mathematicians usually regard as sets, such as the set R of real numbers.

Figure 1 describes a collection of operators from set theory that we have found adequate for ordinary mathematics. Some of these operators can be defined in terms of the others. The rest are effectively defined by axioms. For example, the Separation Axiom [2, page 325] asserts that, for any set S, the expression {x ∈ S : p} denotes a set consisting of all elements of S satisfying p. This axiom is valid only because S is considered to lie outside the scope of the bound variable x. Thus, {x ∈ {x} : x ∉ x} equals {y ∈ {x} : y ∉ y}, which equals either {x} or ∅. Similarly, S lies outside the scope of x in {e : x ∈ S}.

For most uses of ZF, it suffices to understand the meanings of the operators of Figure 1, and to know that two sets are equal iff (if and only if) they have the same elements. Certain applications require axioms that guarantee the existence of “enough” distinct sets. In computer science, it seems necessary only to assume that, for every set S, there is some value v such that v ∉ S. More sophisticated mathematical applications may need more powerful assumptions, such as the Axiom of Choice [2, page 335].

Naive informal reasoning about sets can be unsound. A common source of error is reasoning about collections of elements that are “too big” to be sets, where a collection is too big if it has “as many elements as” the collection of all sets. For example, the collection of all sets having a single element is too big because the correspondence S ↔ {S} shows that there are as many single-element sets as there are sets. Such errors are avoided by using the operators of Figure 1, with which one can construct only legal sets. For example, Russell’s paradox asserts that the “set” R of all sets that are not elements of themselves satisfies R ∈ R iff it satisfies R ∉ R. The “set” R cannot be expressed with the operators of Figure 1.

The formulas of ZF are formed from the operators of set theory, the usual operations of first-order predicate logic, and two additional constructs. The first is if p then e_{1} else e_{2}, which equals e_{1} if p is true, and otherwise equals e_{2}. The second is choose x : p, which denotes some arbitrarily chosen value x for which the predicate p is true, if one exists, and otherwise denotes a completely arbitrary value. For example, choose x : x ∉ R denotes some unspecified value that is not a real number. The choose operator is known to logicians as Hilbert’s ε-symbol [1]. Although this operator appears to introduce the Axiom of Choice to ZF, it actually adds no new properties of sets.

2.2 Functions

It is customary to define functions to be sets of ordered pairs. For example, the reciprocal function that maps every nonzero real number r to 1/r is defined to be the set {⟨r, 1/r⟩ : r ∈ R\{0}}. However, it does not matter how functions are defined. What we need are the four operators described in Figure 2. For reasons discussed below, we write f[x] instead of the more conventional f(x) to denote the result of applying the function f to the value x. Every function f has a domain, which is a set denoted dom f. The set [S → T] consists of all functions f such that dom f = S and f[x] ∈ T for all x ∈ S. The notation [x ∈ S ↦ e] is used to describe a function explicitly; for example, [r ∈ R\{0} ↦ 1/r] denotes the reciprocal function, whose domain is the set R\{0} of nonzero reals.

We now have the operators we need to describe all the functions of ordinary mathematics. Consider, for example, the factorial function. This is the unique function fact, whose domain is the set N of natural numbers, such that fact[0] = 1 and fact[n] = n · fact[n−1], for n > 0. Hence, fact equals

choose f : f = [n ∈ N ↦ if n = 0 then 1 else n · f[n−1] ]

f[e] [Function application] dom f [Domain of the function f] [S → T] [Set of functions with domain S and range a subset of T] [x ∈ S ↦ e] [Function f such that f[x] = e for x ∈ S]

Figure 2: Operators for expressing functions We use the following syntax to mean that fact is defined to be this function.

fact[n : N] =^{Δ} if n = 0 then 1 else n · fact[n−1]

2.3 Operators

Let us now consider the problem of defining len(s) to denote the length of an arbitrary sequence s. We represent a sequence s of length n by a function whose domain is the set {1 … n} of natural numbers from 1 through n, letting s[i] represent the i^{th} element of the sequence. (We let {1 … 0} denote the empty set, so the empty sequence, which has length zero, is the unique function whose domain is the empty set .)

As a warmup exercise, we define the set seq(S) of all sequences of elements in S. An n-element sequence in seq(S) is a function with domain {1 … n} and range a subset of S. The set of all such sequences is denoted by [{1 … n} → S], and seq(S) is the union of all such sets, for all natural numbers n. Hence, seq(S) is the set ⋃ { [{1 … n} → S] : n ∈ N}.

Now, let us define len(s). A sequence of length n is a function with domain {1 … n}. Thus, n is the length of a sequence s iff n is a natural number and dom s equals {1 … n}. Hence, len(s) can be defined to equal choose n : (n ∈ N) ∧ (dom s = {1 … n}).

What is len? One would like to call it a function and consider len(s) to be an instance of function application. However, the domain of a function is a set. If len were a function, its domain would have to be the collection of all sequences, which is “too big” to be a set. We must consider len to be an operator, just like ⋃. For any value v, the expression ⋃ v denotes a value, so (⋃ v) ∈ S is a formula of ZF. However, ⋃ by itself does not denote a value, and ⋃ ∈ S is a meaningless string of symbols, not a formula of ZF. Similarly, len(v) denotes a value, for any value v; but len by itself does not denote a value, and len ∈ S is a syntactically incorrect, meaningless string of symbols.

We find it helpful to distinguish functions from operators by using square brackets for function application. However, this is not necessary; ordinary parentheses can be used for both. In a properly designed formal language, one can determine syntactically whether a symbol denotes a value or an operator, so f(x) is unambiguous.

2.4 What is 1/0?

For any value v, the expression len(v) denotes a value. What value is denoted by len(R)? By definition, it equals choose n : (n ∈ N) ∧ (dom R = {1 … n}). Since R is not a function, we don’t know what value is denoted by the expression dom R, so we don’t know whether it equals {1 … n} for any natural number n. Hence, we don’t know what value len(R) denotes; perhaps it equals \sqrt{2}, perhaps it doesn’t. More precisely, the axioms of ZF do not allow us to determine whether the formula len(R) = \sqrt{2} is valid.

Let us switch to a more familiar example. We might define x/y to equal choose r : (r ∈ R) ∧ (r · y = x). Since there is no r satisfying (r ∈ R) ∧ (r · 0 = 1), this definition allows us to say nothing about 1/0 except that it is a value. It might equal \sqrt{2}; it might equal seq(R).

Elementary school children and programmers are taught that 1/0 is meaningless, and they are committing an error by even writing it. More sophisticated logicians say that 1/0 equals the nonvalue ⊥, which acts like a virus, turning infected expressions to ⊥. They devise complicated rules to describe how it spreads—for example, declaring that (0 = 1) ∨ (0 = ⊥) equals ⊥, but (0 = 1) ∧ (0 = ⊥) equals false.

Instead of calling 1/0 an error or a nonvalue, it is much simpler to say that 1/0 is some value—we just don’t know what value. Even 1/(⋃ R) is a value. This causes no problems. Consider the formula

(x ∈ R) ∧ (x ≠ 0) ⇒ (x · (1/x) = 1)

It is valid when any value is substituted for x. Substituting 0 for x yields

(0 ∈ R) ∧ (0 ≠ 0) ⇒ (0 · (1/0) = 1)

which is valid regardless of what 1/0 equals and whether or not 0 · (1/0) equals 1, because 0 ≠ 0 is false. Substituting ⋃ R for x yields

((⋃ R) ∈ R) ∧ ((⋃ R) ≠ 0) ⇒ ((⋃ R) · (1/(⋃ R)) = 1)

which is valid regardless of what 1/(⋃ R) equals, because (⋃ R) ∈ R is false.

2.5 An Example: The Riemann Integral

To illustrate how to formalize ordinary mathematics in ZF, we define the Riemann integral of elementary calculus as the limit of trapezoidal approximations to the (signed) area under the graph of the function. Define a partition p of the interval from a to b to be a monotonic sequence p[1], …, p[n] of reals such that p[1] = a and p[n] = b. Approximating the area under the graph of f between p[i] and p[i+1] by a trapezoid, such a partition p yields the following approximation S_{p}f to ∫_{a}^{b} f.

∑_{i=1}^{n−1} (p[i+1] − p[i]) · ( f[ p[i] ] + f[ p[i+1] ] ) / 2

Define a partition p to be a δ-partition iff |p[i+1]−p[i]| < δ, for i = 1, …, n− 1. The Riemann integral ∫_{a}^{b} f is defined to be the limit of approximations S_{p}f for δ-partitions p, as δ goes to zero. More precisely, ∫_{a}^{b} f is the unique number satisfying the following property: for every ϵ > 0 there exists a δ > 0 such that | ∫_{a}^{b} f − S_{p}f| < ϵ for every δ-partition p. If no such number exists, then f is not integrable on the interval from a to b, and ∫_{a}^{b} f is not defined.

This definition is formalized in Figure 3, assuming only the set R of real numbers, the subset N of naturals, and the usual arithmetic operations and ordering relations on numbers. First, the set R^{+} of positive reals, the absolute value, and the set {m … n} are defined. Then, ∑_{m}^{n} f is defined to

equal ∑_{i=m}^{n} f[i]. We consider ∑_{m}^{n} f to be syntactic sugar for ∑(f, m)[n], where

we have made ∑(f, m) a function with domain N to permit a recursive definition. Next, we define the set P_{a}^{b}(δ) of all δ-partitions of the interval from a to b, and the approximation S_{p}f. (It does not matter what S_{p}f equals if p is not a partition.) Finally, we define the integral in terms of the operator S. Note that the value of ∫_{a}^{b} f is unspecified if f is not integrable on the interval from a to b.

Figure 3 may not be simple, but its complexity comes from the mathematical concept it is defining. The translation of the ordinary definition into ZF was straightforward. The major departure from conventional mathematical notation is in writing ∑_{m}^{n} f instead of ∑_{i=m}^{n} f[i]. To permit such notation,

we would need some way of indicating in the definition of ∑_{i=m}^{n} f[i] that i is

a bound variable, and that f lies in its scope, but m and n do not.

2.6 Further Remarks

In ordinary, informal mathematics, the meaning of a symbol depends on its context. The symbol × in a text on set theory denotes the Cartesian

R^{+} =^{Δ} {r ∈ R : 0 < r}

|r| =^{Δ} if r < 0 then −r else r

{m … n} =^{Δ} {i ∈ N : (m ≤ i) ∧ (i ≤ n)}

∑_{m}^{n: N} f =^{Δ} if n ≤ m then 0 else f[n] + ∑_{m}^{n−1} f

P_{a}^{b}(δ) =^{Δ} { p ∈ seq(R) :

∧ (p[1] = a) ∧ (p[len(p)] = b)

∧ ∀ i ∈ {1 … len(p)−1} : ∧ if a ≤ b then p[i] ≤ p[i+1]

else p[i] ≥ p[i+1]
∧ |p[i+1] − p[i]| < δ }

S_{p}f =^{Δ} ∑_{1}^{len(p)−1}[ i ∈ N ↦ (p[i+1] − p[i]) · ( f[ p[i] ] + f[ p[i+1] ] ) / 2 ]

∫_{a}^{b} f =^{Δ} choose r : ∧ r ∈ R

∧ ∀ ϵ ∈ R^{+} : ∃ δ ∈ R^{+} : ∀ p ∈ P_{a}^{b}(δ) : | r − S_{p}f | < ϵ

Figure 3: The definition of the Riemann integral.

product, while in an advanced calculus text it may denote the product of vectors in three-space. The symbol x may be used to denote different values in different parts of a proof. A complete formal language for mathematics would include hierarchically structured contexts, and definitions that apply only within a specified context. This structuring is independent of whether or not one uses types.

Mathematicians sometimes use the same symbol to denote different things within a single context. An advanced calculus text might let × denote both Cartesian product and vector product, hoping the reader will figure out that x × y ∈ S × T asserts that the vector product x × y is in the Cartesian product S × T. When the rules for disambiguating the use of a symbol can be stated precisely, they can be defined formally. For example, a × b can be defined to equal if a ∈ R × R × R then … else . . .. However, it is probably better to write x×y ∈ S × T than to explain how to distinguish between two different uses of ×.

3 Types

We have never found a rigorous, universally accepted definition of a type. However, we can define type correctness. We first define a class to be a collection of values that satisfies some property expressible in ZF. For example, the collection of all finite sequences is a class, since a value s is a finite sequence iff it satisfies the ZF formula ∃ S : s ∈ seq(S). In a typed system, every operator has a domain that is a class. The domain of operator len would be the class of all finite sequences. The function-application operator, which maps the pair ⟨f, x⟩ to the value f[x], has as its domain the class of all ⟨f, x⟩ such that x ∈ dom f. A formula is type correct iff its validity does not depend on the result of applying an operator to any argument not in its domain. Thus, (∃ x ∈ R : x^{2} < 0) ⇒ (7 = len(R)) is type correct even though R is not in the domain of len, since the formula’s validity does not depend on the value of len(R).

Type correctness is a reasonable requirement for a formula. However, type systems generally require a formula to be type checkable, meaning that a type-checking algorithm can determine that the formula is type correct. To make type checking easy, most typed languages allow only a restricted form of classes to be used as types, and have conservative rules for type checkability. A type correct formula need not be type checkable, and it may have to be re-expressed in a more complicated fashion to appease the type checker. More complex type systems can provide more expressive power, at the cost of making the language more complicated. But, any language with a decidable type-checking procedure must disallow some type-correct formulas.

Conventional wisdom asserts that type checking catches enough errors in programs to be worth the inconvenience caused by prohibiting some typecorrect programs. We do not dispute this assertion. But, mathematics is not programming. Programs operate on simple, finite data structures—not on Riemann-integrable functions on the real line. The complexity introduced by working around the restrictions of a type system is a potential source of error. In the realm of mathematics, type checking could cause more errors than it catches.

Our experience has been that, when writing a rigorous proof of a theorem, one quickly finds any error in its statement that could be caught by a type checker. There are applications in which theorems are written (perhaps implicitly) but not proved—for example, specifying complex systems. Type checking can catch errors in these applications. However, type checking need not imply the constraints of a type system. Type correctness can be expressed as a theorem in ZF. For example, type correctness of the definition of len is expressed by the formula ∀ S : ∀ s ∈ seq(S) : len(s) ∈ N. Type checking does not require a typed language. One can assert type correctness with theorems, and rename the type checker to be an automatic theorem prover. A language could even provide a syntax for writing those theorems as if they were type declarations—for example, a “typed” definition of len might be written

len(s : seq(Any)) : N =^{Δ} choose n : (n ∈ N) ∧ (dom s = {1 … n})

But unlike type declarations, failure of the theorem prover (type checker) to verify the type-correctness theorem asserted by such a definition need not force one to rewrite the definition. The theorem could be proved by other methods, or simply accepted without proof.

4 Conclusion

Although types may be good for programming languages, we claim that formal mathematics should employ an untyped language. We also claim that specification should be more like mathematics than like programming. A specification language should encourage an abstract description of what a program or system is supposed to do, not a low-level description of how it behaves. Everything we have said about the unsuitability of types for mathematical formulas applies to specifications.

It is sometimes argued that, because programming languages use types, a language for specifying programs should also be typed. However, an untyped formalism such as ZF is likely to be better than a typed one for describing a different type system. A typed specification language would be convenient only for specifying programs written in a language with the same type system. But, verifying that a program implements a specification that uses the same type system is not likely to catch an error caused by misunderstanding some subtle feature of the type system. We do not find Pascal to be a good language for specifying Pascal programs.

It should be obvious that theorem proving is mathematics, not programming. Yet, most mechanical theorem provers use a typed language, making it harder to express mathematics. These provers are better at reasoning about types than at reasoning about sets, the most fundamental data type of mathematics. Given the type declarations m, n : N and + : N × N → N, a theorem prover will immediately deduce that m + n : N. But, it can take considerable effort to convince the prover that m ∈ N, n ∈ N, and + ∈ [N × N → N] imply m + n ∈ N (where m + n means +[⟨m, n⟩] ). Any algorithm for deducing the types of expressions provides a method for deducing facts about set membership. Sets are a more natural choice than types as the basis for a general-purpose theorem prover.

We have found that most computer scientists have an unreasonable attachment to types. They are suspicious of any attempt to eliminate types, and many will refuse to believe that the brief outline of ZF presented here can be made completely formal. ZF serves as the foundation for a complete specification language, with a precise formal semantics, that will be described elsewhere. Here, we can only assure the reader that mathematicians have gotten along quite well for two thousand years without types, and they still can today.

Acknowledgements

I have profited from comments on an earlier version by Mike Gordon, Peter Hancock, James Horning, Heiko Krumm, and Peter Ladkin.

References

[1] A. C. Leisenring. Mathematical Logic and Hilbert’s ε-Symbol. Gordon and Breach, New York, 1969.

[2] J. R. Shoenfield. The axioms of set theory. In Jon Barwise, editor, Handbook of Mathematical Logic, chapter B1, pages 317–344. North-Holland, Amsterdam, 1977.