Several Types of Types in Programming Languages

Abstract

Types are an important part of any modern programming language, but we often forget that the concept of type we understand nowadays is not the same it was perceived in the sixties. Moreover, we conflate the concept of “type” in programming languages with the concept of the same name in mathematical logic, an identification that is only the result of the convergence of two different paths, which started apart with different aims. The paper will present several remarks (some historical, some of more conceptual character) on the subject, as a basis for a further investigation. We will argue that there are three different characters at play in programming languages, all of them now called types: the technical concept used in language design to guide implementation; the general abstraction mechanism used as a modelling tool; the classifying tool inherited from mathematical logic. We will suggest three possible dates ad quem for their presence in the programming language literature, suggesting that the emergence of the concept of type in computer science is relatively independent from the logical tradition, until the Curry-Howard isomorphism will make an explicit bridge between them.

1 Introduction

Types are an important part of modern programming languages, as one of the prominent abstraction mechanisms over data¹. This is so obvious that we seldom realise that the concept of type we understand nowadays is not the same it was perceived in the sixties, and that it was largely absent (as such) in the programming languages of the fifties. Moreover, we now conflate the concept of “type” in programming languages with the concept of the same name in mathematical logic—an identification which may be (is it?) good for today, but which is the result of a (slow) convergence of two different paths, that started quite apart with different aims. Tracing and recounting this story in details, with the painstaking accuracy it merits, it is well beyond the limits of this paper—it could be the subject of a doctoral thesis. We will instead make several remarks (some historical, some of more conceptual character) that we hope will be useful as a basis for a further investigation. We will argue that there are three different characters at play in programming languages, all of them now called types: the technical concept used in language design to guide implementation; the general abstraction mechanism used as a modelling tool; the classifying tool inherited from mathematical logic. We will suggest three possible dates ad quem for their presence in the programming language literature, suggesting that the emergence of the concept of type in computer science is relatively independent from the logical tradition, until the Curry-Howard isomorphism will make an explicit bridge between them. As we will see, the investigation on the arrival on the scene of these three characters will bring us to the (early) seventies.

2 From Types to “Types”

One of the first questions to be cleared is when the very word “type” stably entered the technical jargon of programming languages². Contrary to folklore, early documentation on FORTRAN does not use the word, at least in the technical sense we mean today. In one of the early manuals, dating 1956 [3], we read, for instance

Two types of constants are permissible: fixed points (restricted to integers) and floating points (page 9)

or

Two types of variables are also permissible (with the usual distinction based on the initial letter) (page 10)

but also

32 types of statement (page 8)

These are generic uses of the term “type”—“kind” or “class” could be used instead. Especially because, on page 14 there is a detailed discussion of what happens when one mixes integers and floats. And “type” is never used. The noun “mode” is used instead³:

A FORTRAN expression may be either a fixed or a floating point expression, but it must not be a mixed expression. This does not mean that a floating point quantity can not appear in a fixed point expression, or vice versa, but rather that a quantity of one mode can appear in an expression of the other mode only in certain ways. $(\ldots )$ Any fixed point (floating point) constant, variable, or subscripted variable is an expression of the same mode. $(\ldots )$ If SOMEF is some function of n variables, and if E, F, ..., H are a set of n expressions of the correct modes for SOMEF, then SOMEF (E, F, ..., H) is an expression of the same mode as SOMEF. (page 14)

When, then, do we find a precise occurrence of our technical term? For sure in the report on Algol 58 [31] published in December 1958. There, “type” is used as a collective representative for “special types, e.g., integral, or Boolean” (page 12). Declarations (needed for non real-valued identifiers) are called “type declarations”:

Type declarations serve to declare certain variables, or functions, to represent quantities of a given class, such as the class of integers or class of Boolean values.

Form: $\varDelta \sim$ type (I,I,...I) where type is a symbolic representative of some type declarator such as integer or boolean, and the I are identifiers. Throughout the program, the variables, or functions named by the identifiers I, are constrained to refer only to quantities of the type indicated by the declarator (page 16).

Algol 58 is the result of a meeting held in Zurich at the end of May 1958, between an ACM group (including Backus and Perlis) and a European group. Each group had its own preparatory paper [2, 4], and both such papers do not use “type”. Of the two, only the ACM’s one discusses the issue of the declaration for non real-valued identifiers, using the general term “class”:

A data symbol falls in one of the following classes: (a) Integer (b) Boolean (c) General (page 4)

Declarations are called “Symbol Classification Statements”; their concrete syntax is the same as in the final Algol 58 report⁴:

The symbol classification statements are:

INTEGER ($s_1,\ldots ,s_n$)

BOOLEAN ($s_1,\ldots ,s_n$)

but it is striking how during the Zurich meeting the committee realised that the different “classes” could be grouped together, and given a name as a collective—types were born. It is also remarkable that, at least from these references, the technical term appears to be just a semantical shift from the generic one; in particular, there is no clue that in this process the technical term “type” from mathematical logic had any role⁵. This process will come to maturity in Algol 60 [1]:

Integers are of type integer. All other numbers are of type real.

or

The various “types” (integer, real, Boolean) basically denote properties of values.

Observe the word “types” under quotes, as to stress that it is no longer the ordinary word, but the technical one.

What this term means is simple—data values are partitioned in disjoint classes; each class is mapped to a specific memory representation. Type information collected from the source program guides the compiler for memory allocation and choice of machine operations to be used during translation. Moreover, these types provide a certain level of abstraction over such implementation details, avoiding the manipulation of a value by operations of different types. However, besides the availability of indexed values (arrays), there is no linguistic provision for dealing with more structured data, or for data “naturally” belonging to classes not available as primitive types.

3 Data Types and Abstractions

Algol 58 treats arrays separately from types. One first declares the type of an identifier (unless it is a real-valued one, for which no such declaration is needed), than declares the identifier to be an array, fixing the number of dimensions (and assigning lower and upper bounds for the indexes). With all its maturity with respect to “types”, Algol 60 makes no change in the treatment of arrays—types denote properties of just “simple” values.

That Algol’s provision for primitive data was too restrictive, was clear even to its designers⁶. To address this “weakness,” John McCarthy advocates a

way of defining new data spaces in terms of given base spaces and of defining functions on the new spaces in terms of functions on the base spaces. [27] (page 226)

The new data space constructors are the Cartesian product, the disjoint union, and the power set, each of them equipped with its canonical (universal) maps, which are used to define functions on the new spaces from functions on the base spaces. McCarthy’s paper treats the question at a general meta-level, it does not propose a specific language, and it does not use the term “type”, but it sets a clear roadmap on how to introduce new types in programming languages—instead of inventing an arbitrary new palette of primitive types, provide general, abstract⁷ mechanisms for the construction of new types from the base ones. Base types could be taken as frugal as the single “null set”, since natural numbers could be defined from it. Although McCarthy’s paper has no explicit reference to any type-theoretic, mathematical logic paper (it cites Church’s logic manual, though), we think this is one of the first contacts of the two concepts we are concerned with in this essay, albeit still in an anonymous form.

The challenge to amend the “weakness of Algol” was taken up in more concrete forms, and in similar ways, by Tony Hoare [17], and by Ole-Johan Dahl and Kristen Nygaard [11], around 1965. Hoare’s paper, with an explicit reference to McCarthy’s project introduces at the same time the concepts of (dynamically allocated) record and typed reference. A record is an ordered collection of named fields ⁸; the life of a record does not follow the life of the block in which the record is created. Typed references may be seen like pointers, but no operations are allowed on them, besides creation and dereferencing (that is, access to the “pointed”, or referenced, object). Moreover, when such a reference is created, the type (or class, in the paper’s terminology) of the referenced record is fixed and cannot be dynamically modified. Records are not a new idea—the concept was introduced in “business oriented languages”, FLOWMATIC first, then COBOL (see, e.g., [21]), where the field of a record may be a record itself (nested records), thus permitting static hierarchical structures (i.e., trees). Also dynamically allocated structures⁹ were already available in “list processing languages”, of which LISP is the main representative. Lisp’s S-expressions [26] may indeed be seen as dynamic records composed of two unnamed fields. Moreover, since S-expressions may be nested, they may be used to simulate more complex structures. What is new in Hoare’s proposal, however, is from one side the flexibility in modelling provided by arbitrary named fields; from the other, and crucially, Hoare’s records may contain references to other records, thus allowing for the explicit representation of graph-like structures.

In Simula [11], Dahl and Nygaard had already implemented analogous ideas, with the aim to design an extension to Algol for discrete event simulation: a record class is an activity; a record is a process; a field of a record is a local variable of a process (see also [18]). References are not a prime construct of the language; instead, there are sets, which are bidirectional lists of elements, each of them being (a pointer to) a process. What is really new in Simula I is that a (dynamically created) “process” encapsulates both data objects and their associated operators, a concept that will be called object in Simula 67 (see, e.g., [10]) and which will be popularised by Alan Kay in the context of Smalltalk [14, 23].

Of the two papers we are discussing, it will be Hoare’s one to have the major, immediate impact. Although the proposal is for an extension to Algol 60, it will not materialise into the “official” Algol family—Algol W, which we shall discuss later, is not an official product of the Algol committee¹⁰. The paper is fundamental because types change their ontology—from an implementation issue, they programmatically become a general abstraction mechanism¹¹:

the proposal is no arbitrary extension to an existing language, but represents a genuine abstraction of some feature which is fundamental to the art or science of computation. (page 39)

This happens on (at least) three levels. First, it implements McCarthy’s project into a specific programming language, extending the concept of type from simple to structured values¹². Starting from this paper, “structured values” are organised in types in the same way as “simple values”, thus opening the way to the modern view of data types.

Second, types are a linguistic modelling tool:

In the simulation of complex situations in the real world, it is necessary to construct in the computer analogues of the objects of the real world, so that procedures representing types of even may operate upon them in a realistic fashion. (page 46)

The availability of a flexible way of data structuring (contrasted to the rigid structure provided by arrays) is seen as the linguistic mechanism that provides the classification of “the objects of the real world”. Moreover, the possibility to embed references into records allows for the construction of complex relational structures. Data are no longer “coded” into integers or reals—a record type naturally represents a class of complex and articulate values. Even more importantly, following McCarthy, the language only provides general means of construction—the definition of new classes of data being left to the programmer.

Finally, the combination of record types and typed references provides a robust abstraction over the memory layout used to represent them. By insisting that references be typed, the type checker may statically verify that the field of a record obtained by dereferencing is of the correct type required by the context—primitive types are true abstractions over their representation. In retrospect,

I realised that [types] were essential not only for determining memory requirements, but also for avoiding machine-dependent error in a running object program. It was a firm principle of our implementation that the results of any program, even erroneous, should be comprehensible without knowing anything about the machine or its storage layout. [20]

Hoare’s proposal, including the terminology (“record classes”), will find its context into the joint paper [38], and finally will be implemented in Algol W [36], which will have a significant impact on subsequent languages, being an important precursor of Pascal. In Algol W the picture and the terminology are complete:

Every value is said to be of a certain type. $(\ldots )$ The following types of structured values are distinguished: array: $(\ldots )$, record: $(\ldots )$. (pages 16-17)

The last step yet to be done was the unification of two aspects that were still distinct in Hoare’s proposal—classification (i.e., modelling) and abstraction. In Algol W, primitive types and user defined record types do not enjoy the same level of abstraction. On one hand, primitive types (integers or floats, say) are an opaque capsule over their implementation-dependent representation, and the type system ensures that on a primitive type only operations of that type are allowed. On the other hand, the user may well define a record class for modelling ‘the objects of the real world”, but there is no way of fixing which operations are allowed on such class, besides the general ones manipulating records and references. The user will probably define functions taking as argument values of these record classes, but the type system cannot enforce that only such operations are allowed to manipulate those values. In the literature of the early seventies there are several proposals for allowing (and enforcing) stricter checks. Morris [30] advocates that the type system (including user-defined types) guarantee that only the prescribed operations on a type could operate on its values (forbidding thus the manipulation of the representations of those values). A thesis which will be further elaborated and formulated in modern terminology¹³ by Reynolds in his seminal [34], which also extends it to polymorphic situations:

The meaning of a syntactically-valid program in a “type-correct” language should never depend upon the particular representation used to implement its primitive types. $(\ldots )$ The main thesis of [Morris [30]] is that this property of representation independence should hold for user-defined types as well as primitive types. 

From now on, types will be the central feature of programming languages as we understand them today¹⁴.

4 Classifying Values

Types inhabit mathematical logic since the early days, with the role of restricting the formation of formulas, in order to avoid paradoxes¹⁵. They are a discipline for (statically—as we would say today) separating formulas “denoting” something from formulas that “do not denote”. In the words of the Preface to Principia Mathematica [37]:

It should be observed that the whole effect of the doctrine of types is negative: it forbids certain inferences which would otherwise be valid, but does not permit any which would otherwise be invalid.

The opposition “denoting” vs. “non denoting” becomes, in programming languages, “non producing errors” vs. “producing errors”¹⁶. Types as a classifying discipline for programs—and with the same emphasis on the fact that some valid formulas will be necessarily forbidden, for decidability’s sake—are found in the programming languages literature as early as in the PhD thesis of Morris [29]:

We shall now introduce a type system which, in effect, singles out a decidable subset of those wfes that are safe; i.e., cannot given rise to ERRORs. This will disqualify certain wfes which do not, in fact, cause ERRORS and thus reduce the expressive power of the language. (page 89)

Morris performs his “analysis” by taking first the type-free $\lambda$-calculus, and imposing then the constraints of the “simple” functional types, formulated as a type-assignment system. More specifically, Morris says that “the type system is inspired by Curry’s theory of functionality”, quoting [8], while there is no reference to [7], which apparently would have been a more precise reference. The reason could be that Church formulates his theory directly with typed terms, instead of seeing types as predicates on type-free terms. Were this the reason, Morris’ thesis would be the first reference to the now common distinction between typing “à la Curry” and “à la Church”.

Are these the types of mathematical logic? They share the same aims, but the connection is implicit, even unacknowledged. The fact that Church’s [7] is not cited by Morris could certainly be explained as we argued above, but it is nonetheless revealing of the lack of awareness for the mathematical logic development of the concept. The first explicit connection we know of, in a non technical, yet explicit, way is [19], but the lack of acknowledgement is going to persist—neither Morris’ [30] or Reynolds’ [34] cites any work using types in logic. Certainly the Zeitgeist was ripe for the convergence of the two concepts, and there was a formidable middleman—$\lambda$-calculus. Used first by Landin as a tool for the analysis of Algol (and then by Scott, Strachey, Morris, Reynolds, and all the rest), at the dawn of the seventies $\lambda$-calculus was the lingua franca of conscious programming language theorists, both in the type-free and the typed version. Programming languages and proof-theory were talking the same language, but the conflation was always anonymous. In Reynolds’s [34] a second order (“polymorphic”) typed lambda-calculus is independently introduced and studied, almost at the same time in which Girard [13] uses it as a tool to prove cut-elimination for second order logic; Milner [28] presents a type-reconstruction algorithm for simple types, independently from Hindley [16] (which will be cited in the final version). The Curry-Howard isomorphism [22] (the original manuscript dates 1969 and was widely circulated, at least in the proof-theory and lambda-calculus communities) will be the catalyst for the actual recognition¹⁷, which comes only in Martin-Löf’s [24], written and circulated in 1979, which presents a complete, explicit correspondence between proof-theory and functional languages. The paper will have significant impact on following research (and not only the one on programming languages).

This slow mutual recognition of the two fields tells a lot on their essential differences. For most of the “types-as-a-foundation-of-mathematics” authors, types where never supposed to be actually used by the working mathematician (with the debatable exception of Russell himself). It was sufficient that in principle most of the mathematics could be done in typed languages, so that paradoxes could be avoided.

Types in programming languages, on the contrary, while being restrictive in the same sense, are used everyday by the working computer programmer. And hence, from the very beginning in Algol, computer science had to face the problem to make types more “expressive”, and “flexible”¹⁸. If in proof-theory “typed” means first of all “normalizing”, in computer science there are — since the beginning — well-typed programs which diverge. While mathematical logic types are perceived as constraints (they “forbid” something, as in Russell’s quote above), types in programming languages are experienced as an enabling feature, allowing simpler writing of programs, and, especially, better verification of their correctness¹⁹.

The crucial point, here and in most computer science applications of mathematical logic concepts and techniques, is that computer science never used ideological glasses (types per se; constructive mathematics per se; linear logic per se; etc.), but exploited what it found useful for the design of more elegant, economical, usable artefacts. This eclecticism (or even anarchism, in the sense of epistemological theory) is one of the distinctive traits of the discipline, and one of the reasons of its success.

But this is the subject of an entirely different paper.