Arcane Sentiment

Previously I speculated that the word “datatype” might have been used in computing before 1958. In response, dvt found a precedent from 1945! It's Konrad Zuse's very early language Plankalkül (Plan Calculus). Zuse's notes pervasively use the words Angabentyp and Angabenart, without bothering to define them. Modern German uses “Daten” instead of “Angaben”, but the terms are otherwise unchanged: “Datentyp” and “Datenart”.

Plankalkül was the world's first programming language, and it begins from first principles: the only primitive type is the bit, charmingly called a “Ja-Nein-Wert” (yes-no-value). It builds everything else out of arrays and tuples. The section on datatypes begins:

Angaben und ihre Darstellung [Data and its representation]

Die auftretenden Angaben können mannigfacher Art sein. Z.B. J.-N.-Werte, Zahlen, Listen usw. [The data given can be of various types, e.g. Y-N-values, numbers, lists etc.]

[...]

Die Unterscheidung der einzelnen Angabenarten soll nun wie folgt formalisiert werden [The distinction between the various datatypes will now be be formalized as follows]:

Angaben-Strukturen [Data structures]

Unter Struktur einer Angabe wird der komponentenmäßige Aufbau einer Angabe ohne Hinblick auf die Bedeutung der einzelnen Fälle und Komponenten verstanden. [The structure of a datum is the component composition of a datum without regard to the meaning of the individual instances and components.]

Wir haben Angaben von starrer und von variabler Struktur. Wir führen nun Angabenstrukturzeichen ein, welche jeder Angabe zugeordnet sind. Diese werden mit S und einer Kennzahl bezeichnet. Die Entwicklung der zusammengesetzten Strukturen erfolgt dann durch „Strukturgleichungen“ aus einfachen (bereits definierten) Strukturen. [We have data of fixed and of variable structure. We now introduce data structure symbols, which are assigned to each datum. These are denoted by S and an ID number. The development of composite structures then follows by “structure equations” from simple (already defined) structures.]

So wird dem einfachen Ja-Nein-Wert das Strukturzeichen S0 zugeordnet. Eine Folge von n J-N-Werten hat dann die Struktur S1.n. Es gilt die Strukturgleichung: [Thus the structure symbol S0 is assigned to the simple yes-no value. Then a sequence of n yes-no values has the structure S1.n. The structural equation applies:]

S1.n = n × S0

Durch Verfolgung der Strukturgleichungen ist es jederzeit möglich, den Aufbau einer Angabe zu ermitteln, auch wenn dieser sehr kompliziert ist. [By following the structure equations, it is possible at any time to determine the composition of a datum, even when it is very complex.]

Plankalkül was never implemented (well, not until 1975), but Zuse wrote enough code in it to discover the need for generics, and duly invented them:

Wir brauchen noch „unbestimmte“ Strukturzeichen. Wollen wir z.B. andeuten, daß eine Angabe aus einer Liste von n Gliedern besteht, ohne die Struktur des Gliedes im einzelnen festzulegen, so schreiben wir: n × σ. [We still need “undefined” structure symbols. Let us suppose, for example, that a datum consists of a list of n elements, without specifying the structure of the individual elements, so we write: n × σ.]

Für σ kann dann ein beliebiges Strukturzeichen eingesetzt werden. [For σ any structure symbol can be used.]

¤ × σ Ist das allgemeinste Strukturzeichen einer Liste. (Struktur der Glieder und Zahl der Glieder offen gelassen). Is the common structure symbol of a list. (Structure of elements and number of elements left open.)

¤ × 2σ Ist die Struktur einer Paarliste, bei der die Glieder der einzelnen Paare von gleicher Struktur σ sind. Is the structure of a pair-list where the elements of each pair are of the same structure σ.

¤ × (σ, τ) Ist die Struktur einer Paarliste bei der die Vorderglieder die Struktur σ, und die Hinterglieder die Struktur τ haben. Is the structure of a pair-list where the front elements have the structure σ and the back elements have the structure τ.

2 × n × σ Ist keine Paarliste, sondern ein Paar von Listen. Is not a pair-list, but a pair of lists.

Array indexes, incidentally, are zero-based:

Es sei noch darauf aufmerksam gemacht, daß bei einer aus n Gliedern bestehenden Angabe der höchste Index der Komponenten gleich n − 1 ist, da die Komponentennumerierung mit 0 beginnt. [It should be pointed out that for a datum consisting of n elements, the highest index of the components is equal to n − 1, as the component numbering begins with 0.]

Separately from data structures, Plankalkül supports constraints on which values can actually be used:

Eine Angaben-Beschränkung liegt vor, wenn die volle Variabilität der zu einer Angabenart gehörenden Struktur nicht voll ausgenutzt ist. Z.B. können Dezimalziffern durch 4 J.N.-Werte dargestellt werden. Es werden jedoch nur 10 von den 16 möglichen Variationen ausgenutzt. [A data-restriction is available when the full variability of the structure belonging to a datatype is not fully used. E.g. decimal digits can be represented by 4 bits. However, only 10 of the 16 possible variations are used.]

In solchen Fällen wird durch eine Beschränkungsformel angegeben, welche Fälle der Struktur in den Definitionsbereich der Angabenart fallen. Eine solche Formel wird mit B und einer Kennzahl bezeichnet. [In such cases, a restriction formula specifies which cases of the structure fall within the defined range of the datatype. Such a formula is denoted by B and an ID number.]

“Typ” and “Art” are synonyms, so they're ripe for distinction by anyone who wants words for two concepts. Zuse does: Angabentypen are optional annotations distinct from both structures and restrictions, while Angabenarten bundle all three together:

Angabentypen [Datatypes]

Den gleichen Strukturen und Beschränkungsformeln können Angaben verschiedener Bedeutung zugeordnet sein. (Z.B. x = und y = Koordinaten). Im allgemeinen ist es nicht nötig, diese zu unterscheiden. Ist dies jedoch vorteilhaft, so werden Typenbezeichnungen eingeführt. Z.B. T1, T7 usw. [The same structures and restriction-formulas can be assigned to data of different meaning. (E.g. x = and y = coordinates). In general it is not necessary to distinguish them. If it is advantageous, however, type-designations will be introduced. E.g. T1, T7 etc.]

Angabenart [Datatype]

Jeder Angabenart ist eine Struktur und evtl. eine Beschränkung bzw. eine Typenbezeichnung zugeordnet. Darüber hinaus kann eine Angabenart noch durch spezielle Bedeutungen der Komponenten gekennzeichnet sein. (Z.B. Zahlen in halblogarithmischer Form, vergl. Zahlenrechnungen S. 119 ff). [Each datatype is assigned a structure and possibly a restriction or type-designation. In addition, a datatype can be further characterized by specific meanings of the components. (E.g. numbers in semi-logarithmic [=floating-point] form, see Numerical Calculations, p.119 ff.)]

Alle diese Kennzeichnungen können dann unter einem Angabenzeichen A zusammengefaßt werden. Ist eine Angabe durch ein A-Zeichen z.B. A10 gekennzeichnet, so ist die besondere Kennzeichnung der Struktur usw. nicht erforderlich, da diese in A10 mit enthalten ist. [All these identifiers can be combined under one data symbol A. If a datum is marked with an A-symbol, e.g. A10, the specific identifier of the structure etc. is not required, as it is included in A10.]

Angabenart-Zeichen können jedoch auch einer Gruppe analoger Angabenarten verschiedener Struktur zugeordnet sein. Z.B. können Zahlen durch verschiedene Strukturen (z.B. Dual-Zahlen, Dez.-Zahlen) dargestellt werden. Jedoch kann ein allgemeines Zeichen (z.B. A8 vergl. Zahlenrechnen S. 121) eingeführt werden, welches lediglich besagt, daß es sich um eine Zahl handelt, ohne ihre Struktur im einzelnen festzulegen. [Datatype symbols can, however, also be assigned to a group of analogous datatypes of different structures. E.g. numbers can be represented by various structures (e.g. binary numbers, decimal numbers). However, a generic symbol (e.g. see A8, Numerical Calculations, p.121) can be introduced which only says that it is a number, without specifying its structure in detail.]

Wir führen entsprechend σ ein unbestimmtes Angabenartzeichen α ein. [We introduce an undefined datatype symbol α corresponding to σ.]

With abstract types in 1945, Plankalkül's type system is ahead of its time. So is its support for predicate calculus, which is worth a post of its own. Less exotically, it has the basic features of languages a decade later: (one-armed) conditionals, loops, function calls, and the assignment statement (written left-to-right).

One feature of Plankalkül is conspicuously primitive. All of the symbols for data structures, restrictions, constants, variables, and so on are not named but numbered. It's like Intercal but 27 years earlier!

Zuse noticed that it was confusing to so many numbers with so many different meanings, and tried to distinguish them with a unique two-dimensional syntax:

Die Zeilendarstellung [The line format]

Um die zu einer Angabe gehörenden verschiedenen Kennzeichnungen, wie Variablen-Index, Komponentenangabe, Angabenart bzw. Struktur usw. übersichtlich darstellen zu können, werden diese einzelnen Kennzeichnungen je verschiedenen Zeilen einer Formel zugeordnet. [To be able to show the various identifiers belonging to a datum, such as variable index, component data, datatype or structure etc., these individual identifiers are assigned to different lines of a formula.]

Wir haben zunächst die Hauptzeile, in welcher die Formel in der bisher üblichen Art dargestellt wird. [First we have the main line in which the formula is shown in the usual way.]

Die nächste Zeile dient der Unterscheidung der verscheidenen Variablen, welche durch den „Variablen-Index“ erfolgt. (V ). Eine weitere Zeile dient der Kennzeichnung der Komponenten der durch die Zeile 1 und 2 gekennzeichneten Variablen. (Komponentenindex K.) [The next line serves to distinguish the different variables, which is done by the “variable index” (V). Another line serves to identify the components of the variables indicated by lines 1 and 2. (Component index K.)]

Es wird also z.B. der Ausdruck [Thus e.g. the expression]

K1(V3) Komponente 1 von V3 [Component 1 of V3]

wie folgt geschrieben [is written as follows]:

V
3
1

bzw. [or] K2.3(Z4) =

Z
4
2.3

In modern notation, those are V3[1] and Z4[2, 3].

Weitere Zeilen können der Kennzeichnung der Struktur und Angabenart bzw. der Beschränkung und dem Typ dienen. [Further lines may be used to indicate the structure and type of data, or the restriction and the type.]

Im allgemeinen wird entweder die Angabe der Struktur oder der Angabenart genügen. (S = Index bzw. A = Index) [In general either the specification of the structure or of the datatype suffice. (S-index or A-index.)]

z.B. [e.g.]

Z
4
2.3
0

bedeutet: „Z4, Komponente 2.3”. Der Wert ist von der Struktur S0. [means: “Z4, component 2.3”. The value is of the structure S0.]

Die Strukturangabe bzw. Angabenart – Angabe bezieht sich dabei auf die Komponente. [The structure specification or datatype specification refers to the component.]

Die einzelnen Zeilen werden durch Vorsetzen der Buchstaben V, K, S bzw. A vor die Zeilen der Formel gekennzeichnet: [The individual lines are identified by prefixing the letters V, K, S or A before the lines of the formula:]

 | Z ^ Z
V | 4 2
K | 2.3
S | 0 0

Wird von einer Angabe keine Komponente gebildet, so bleibt der Komponenten-index frei. [If no component is established for a datum, the component index remains empty.]

Das Zeichen A kann stets an Stelle des Zeichens S gesetzt werden; aber im allgemeinen nicht umgekehrt. Die für Strukturen bereits definierten Kennzahlen dürfen dann nicht mehr für Angabenarten benutzt werden: (Z.B. gibt es nur eine Struktur S0, S1.n und die Zeichen A0, A1.n sind mit diesen Strukturzeichen identisch.) [The symbol A can always be used in place of S, but in general not vice versa. The ID numbers already defined for structures can thus no longer be used for datatypes: (E.g. there is only one structure S0, S1.n and the symbols A0, A1.n are identical to these structure symbols.]

If only Zuse had thought of giving them names! But he was trying to solve a different problem, of typography:

Mit Hilfe dieser Darstellung ist es leicht möglich, die einzelnen Angabenarten zu unterscheiden. Es ist nicht mehr wie bisher in der Mathematik nötig, verschiedene Zeichenarten für verschiedene Angabenarten heranzuziehen. (Z.B. deutsche Buchstaben für Vektoren.) Ein solches Verfahren wäre im allgemeinen Plankalkül nicht anwendbar, da die Zahl der verschiedenen Angabenarten innerhalb der gleichen Rechenpläne bzw. Plangruppen derartig mannigfaltig sein kann, daß die zur Verfügung stehenden Zeichenarten nicht ausreichen. [With the help of this representation it is easily possible to distinguish the individual datatypes. It is no longer necessary, as hitherto in mathematics, to draw up different types of symbols for different datatypes. (E.g. German letters for vectors.) Such a method would not be practical for general plan calculus, as the number of different datatypes in one program or program-group can be so many that the available types of symbols are not enough.]

Constanten [Constants]

Den einzelnen Angabenarten, Typen bzw. Strukturen können Constanten zugeordnet werden, denen spezielle Bedeutung zukommt. Eine Constante ist ein bestimmter Fall aus der Menge der möglichen Variationen einer Angabenart bzw. Struktur. Sie werden mit C und einer Kennzahl bezeichnet. [To the individual datatypes, types or structures constants can be assigned which have special significance. A constant is a particular case from the set of possible variations of a datatype or structure. They are denoted by C and an ID number.]

In addition to constants, Plankalkül distinguishes three kinds of variables (input, intermediate, and output). Since all four can be used in the same context, the symbols C, V, Z and R must appear on every variable reference to distinguish them, so the two-dimensional syntax is not helping much. It's also difficult to transcribe, so I'll stop here rather that trying to translate all 180 pages.

I don't know if Plankalkül was known to the designers of later programming languages, or if it had any influence. But its casual usage of the words “Angabentyp” and “Angabenart” suggests they were already established in 1945.

The word “type” has a variety of meanings in programming languages, which are often a focus of confusion and contention. Here's a history of its use, focusing on particularly influential languages and papers.

1956: Fortran “modes”

The term “type” was apparently not yet established in 1956, because the Fortran manual speaks of integer and floating-point “modes” instead. It has something called “statement types”, but those are what are now called syntactic forms: assignment, conditional, do-loop, etc.

The 1963 Fortran II manual speaks of "two types of constants" (integer and floating-point), but this seems to be just the English word. When it talks about these types in more detail, it calls them “modes”, e.g. “arguments presented by the CALL statement must agree in number, order, mode, and array size with the corresponding arguments in the SUBROUTINE statement”. (Evidently the terms “formal” and “actual” parameters weren't established yet either.)

1958-63: Algol

Algol is one of the most influential languages in history. It introduced if ... then ... else, the int n declaration syntax, and semicolons. It also popularized the term “type”. The Algol 58 report defines type declarations on variables in terms of the “type” and “class” of values:

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. [...] 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.

The Algol 60 report is more consistent:

The various “types” (integer, real, Boolean) basically denote properties of values. The types associated with syntactic units refer to the values of these units.

Note that types are explicitly a property of values, not variables or expressions. But does “basically” mean someone thought otherwise, or just that this isn't a formal definition?

1967: Strachey's Fundamental Concepts

Chris Strachey's Fundamental Concepts in Programming Languages was an influential set of lecture notes that established a bunch of common terms. It defines types thus:

Most programming languages deal with more than one sort of object—for example with integers and floating point numbers and labels and procedures. We shall call each of these a different type and spend a little time examining the concept of type and trying to clarify it.

Strachey takes it for granted that types can be static or dynamic, and prefers static typing only for reasons of efficiency (which was, after all, of overwhelming importance in 1967):

It is natural to ask whether type is an attribute of an L-value or of an R-value—of a location or of its content. The answer to this question turns out to be a matter of language design, and the choice affects the amount of work, which can be done when a program is compiled as opposed to that which must be postponed until it is run.

Strachey does not mention type theory, because no one had yet realized that it could be applied to programs. That changed in the next year.

1968: type theory

James Morris was the first to apply type theory to programming languages, in his 1968 Lambda-calculus models of programming languages. “A system of types and type declarations is developed for the lambda-calculus and its semantic assumptions are identified. The system is shown to be adequate in the sense that it permits a preprocessor to check formulae prior to evaluation to prevent type errors.”

He begins by explaining what types are and why they matter, using the term in the usual programming-languages sense:

In general, the type system of a programming language calls for a partitioning of the universe of values presumed for the language. Each subset of this partition is called a type.

From a purely formal viewpoint, types constitute something of a complication. One would feel freer with a system in which there was only one type of object. Certain subclasses of the universe may have distinctive properties, but that does not necessiate an a priori classification into types. If types have no official status in a programming language, the user need not bother with declarations or type checking. To be sure, he must know what sorts of objects he is talking about, but it is unlikely that their critical properties can be summarized by a simple type system (e.g., prime numbers, ordered lists of numbers, ages, dates, etc.).

Nevertheless, there are good, pragmatic reasons for including a type system in the specifications of a language. The basic fact is that people believe in types. A number is a different kind of thing from a pair of numbers; notwithstanding the fact that pairs can be represented by numbers. It is unlikely that we would be interested in the second component of 3 or the square root of < 2,5>. Given such predispositions of human language users, it behooves the language designer to incorporate distinctions between types into his language. Doing so permits an implementer of the language to choose different representations for different types of objects, taking advantage of the limited contexts in which they will be used.

Even though a type system is presumably derived from the natural prejudices of a general user community, there is no guarantee that the tenets of the type system will be natural to individual programmers. Therefore it is important that the type restrictions be simple to explain and learn. Furthermore, it is helpful if the processors of the language detect and report on violations of the type restrictions in programs submitted to them. This activity is called type-checking.

Then he switches without explanation to taking about static checkers, e.g:

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.

So the confusion between programming-language and type-theory senses of the word began with the very first paper to use the latter.

1968: APL

APL-360 was the most popular dialect of APL. Its manual doesn't use the word “type”; it speaks of “representations” of numbers. But it considers these an implementation detail, not an important part of its semantics.

APL has a lot of unique terminology — monad and dyad for unary and binary operators, adverb and conjunction for high-order operators, and so on — so it's not surprising that it has its own word for types too.

1970: Pascal

Wirth's 1970 definition of Pascal is, as usual, plain-spoken: “The type of a variable essentially defines the set of values that may be assumed by that variable.” (But there's that “essentially”, like Algol's “basically”.)

1970-73: Lisp belatedly adopts the term

Like Fortran, early Lisps used the word “type”, but only in its ordinary English sense, never as a technical term. AIM-19, from 1960 or 1961, speaks of “each type of LISP quantity”, but doesn't use “type” unqualified. Similarly, the 1962 Lisp 1.5 Manual uses the word for various purposes, but not as an unqualified term for datatypes. The most common use is for function types (subr vs. fsubr); there are “types of variables” (normal, special, common), but datatypes were not, apparently, considered important enough to talk about. They might not have even been seen as a single concept — there are awkward phrases like “bits in the tag which specify that it is a number and what type it is”, which would be simpler with a concept of datatypes.

This changed in the early 1970s. The 1967 AIM-116a and 1970 AIM-190 still don't use “type”, but the 1973 Maclisp manual and 1974 Moonual do, and it consistently means “data type”. Most tellingly, they have typep, so the term was solidly ensconced in the name of a fundamental operator.

1973: Types are not (just) sets

By 1973, the definition of types as sets of values was standard enough that James Morris wrote a paper arguing against it: “Types are not sets”. Well, not just sets. He was talking about static typechecking, and argued that checking for abstraction-safety is an important use of static typechecking. The abstract explains:

The title is not a statement of fact, of course, but an opinion about how language designers should think about types. There has been a natural tendency to look to mathematics for a consistent, precise notion of what types are. The point of view there is extensional: a type is a subset of the universe of values. While this approach may have served its purpose quite adequately in mathematics, defining programming language types in this way ignores some vital ideas. Some interesting developments following the extensional approach are the ALGOL-68 type system, Scott's theory, and Reynolds' system. While each of these lend valuable insight to programming languages, I feel they miss an important aspect of types. Rather than worry about what types are I shall focus on the role of type checking. Type checking seems to serve two distinct purposes: authentication and secrecy. Both are useful when a programmer undertakes to implement a class of abstract objects to be used by many other programmers. He usually proceeds by choosing a representation for the objects in terms of other objects and then writes the required operations to manipulate them.

1977: ML and modern static typing

ML acquired its type system in about 1975 and was published in 1977. Until this point, the application of type theory to programming languages had been theoretical, and therefore had little influence. ML made it practical, which has probably contributed a lot to the terminological confusion.

ML's theoretical support (along with the misleading slogan “well-typed expressions do not go wrong”) came out in the 1978 paper A Theory of Type Polymorphism in Programming, which despite being about type theory, speaks of types containing values:

Some values have many types, and some have no type at all. In fact “wrong” has no type. But if a functional value has a type, then as long as it is applied to the right kind (type) of argument it will produce the right kind (type) of result—which cannot be “wrong”!

Now we wish to be able to show that—roughly speaking—an Exp expression evaluates (in an appropriate environment) to a value which has a type, and so cannot be wrong. In fact, we can give a sufficient syntactic condition that an expression has this robust quality; the condition is just that the expression has a “well-typing” with respect to the environment, which means that we can assign types to it and all its subexpressions in a way which satisfies certain laws.

The short version

So here's the very brief history of “type” in programming languages:

1. It wasn't used at all until 1958.
2. Types as sets of values: Algol-58.
3. The type-theory sense: Morris 1968.

These may not be the earliest uses. I got most of the old manuals from Paul McJones' collection, which is a good place to look for more. I welcome antedatings.

I'm also curious about the term “datatype”, which might plausibly be ancestral to “type”. I could find no uses of it older than “type”, but I may be looking in the wrong field. Statistical data processing is much older than computing, and has dealt with datatypes for a long time. Might the terms “datatype” and “type” have originated there?

Update August 2015: Jamie Andrews said much the same seven months earlier.

Update June 2017: In HN comments, dvt found “datatype” in 1945, in Plankalkül.

There should be more language research like Stefan Hanenberg's experiment on how static typing affects productivity. It uses a rigorous methodology which is standard everywhere except in software engineering research: a controlled experiment. It compares a substantial number of programmers solving the same problem in two purpose-built languages which differ only in a single feature: the presence of a static type system.

Unfortunately the languages tested are not state of the art – the dynamically typed language is approximately Smalltalk, and the static types are those of early Java, with required type annotations and casts and no parametric types. Not surprisingly, it found that this sort of static typing is useless or worse. (Curiously, it also found that debugging type errors took longer when they were found statically than when they were found dynamically, but this is weak evidence, because the debugging times may include work other than fixing the type errors.)

This needs to be replicated with parametric types and optional type annotations!

The obvious languages to compare are a minimal pair differing only in the presence of the static checker — perhaps ML and ML-minus-the-typechecker, since that's easy to implement. We can do better, though: we can distinguish between different effects of static typing. There are many hypotheses about how it affects productivity; some of the most plausible are:

• It finds bugs faster.
• It directs the user's attention to types. (It's not clear whether (when?) this helps or hurts.)
• It restricts programs by preventing constructs like arbitrary union types and variable arity.

ML-minus-the-typechecker suffers from the third effect: even though it doesn't have a typechecker, its library is limited to things the typechecker can handle – so no read or eval or type predicates or even printf (without exotic tricks). So if that effect is important, comparing ML to ML-minus-the-typechecker will not detect it.

We can distinguish between these three effects by devising a way to inflict each effect independently. We can start with a dynamically typed language with an appropriate standard library, and vary three features:

• To find bugs, use a nonrestrictive (“soft”) typechecker, which detects some type errors but doesn't interfere with running programs.
• To selectively divert the user's attention to types, vary the prominence of type declarations: whether they're used in the standard library documentation, whether they're printed in the output of the REPL, whether they're emphasized in the language documentation, and maybe even whether they're enabled at all.
• To restrict programs, use a version of the standard library with everything that would confuse the Hindley-Milner typechecker removed or altered. (This is not the typechecker we're testing, but it represents a typical degree of restriction.) This doesn't restrict user code, but restricting the library should have a similar effect, especially on small programs. (We could also restrict user code by running the H-M typechecker on it and delaying error reporting until runtime, to make it less helpful for finding bugs.)

The eight combinations of these three features allow us to test all three hypotheses, and detect interactions between them.

(Note that we don't test the Hindley-Milner typechecker, because it both finds bugs and restricts programs, and we want to distinguish between these effects. It would be interesting to compare it to the nonrestrictive typechecker, though, to compare the two checkers' efficacy at finding bugs. Has this been done before?)

One experiment like this can do more to advance our understanding of type systems than ten type theory papers, because it addresses questions we care about, not just ones we know how to answer. I wish I could do this one myself, but as that's unlikely to happen, I encourage someone else to do it.

(Via It will never work in theory — the world's finest, and probably only, empirical software engineering research blog.)

(By the way, I was surprised to see the Mann-Whitney U-test used for all the significance tests, instead of Student's t-test. I thought the U-test was a special-purpose test for ordinal (not cardinal) data, but apparently some statisticians recommend it as the default significance test, on the grounds that it's more robust and only a little less powerful.)

A while ago, I made a simple mistake using zlib:

char *file = "/some/path";
gzFile f = gzopen(file, "wb");
if (f) {
 gzprintf(file, "something\n");
 /* ... */
}

This is a static type error, of course: gzprintf expects a gzFile, not a char*, and they have different C types. Unfortunately, C doesn't detect it, because (in older versions of zlib) gzFile happens to be a typedef for void*, and in C char*, like all pointers, can autoconvert to void*. By accident of memory layout, this didn't crash at runtime either; it simply did nothing, causing me some puzzlement when this one line was missing from the otherwise intact output.

In addition to providing a puzzle, this mistake sheds light on some confusing terminology. Like most terms related to type, “weak typing” has several meanings. I usually reserve it for languages with typechecks that don't always apply, either because they can be suppressed by casts, or because some common¹ operations don't provide them. But it's also used for the unrelated concept² of autoconversion.

I thought this was just an arbitrary reuse of a term, but the autoconversion of char* to gzFile demonstrates a common meaning: autoconversion, like casts and missing type checks, means some type errors aren't detected. They usually cause conversions instead of blind misinterpretation of data (though not in this case), but from the user's point of view, the effect is the same: the type checks are unreliable. If you accidentally do arithmetic on a Perl string and it autoconverts to zero, it's small comfort that the conversion is type-safe — the program still continues happily computing incorrect results after a type error. So it makes sense to use the same term for any system of type checks that overlooks some errors. It's confusing to call completely different mechanisms by the same name, but the result is the same: both autoconversion and casts make type checks weak.

¹ If some rare, exotic operations circumvent typechecks, that's OK, because you won't use them by accident.

² And sometimes for even more unrelated concepts like dynamic typing, but this usage is usually either careless or pejorative. When people want to talk about dynamic typing, they don't call it “weak typing”.

Provocative titles work. When a famous type theorist like Benjamin Pierce gives a talk titled Types Considered Harmful, it gets my attention. (Eventually. Years later. After someone links me to it.) This talk describes a contract-checking system, which wouldn't be very interesting in its own right, title or no, but it also includes a bunch of insights about typechecking. Here are the good bits:

First (and this is not new), why does type inference find bugs? It's not because there's anything special about types per se, but simply because it entails enough analysis that inconsistencies in the program are likely to produce contradictions.

• Attempting to prove any nontrivial theorem about your program will expose lots of bugs
• The particular choice of theorem makes little difference!
• Typechecking is good because it proves lots and lots of little theorems about your program

(“Proving theorems” sounds scary, but if you describe it as “checking properties” it means the same thing and is much less intimidating.)

Second, it acknowledges an oft-ignored cost of static typing: it makes languages much more complicated.

Fancy types make the programmer's head hurt

• Type systems – especially very precise ones – force programmers to think rigorously about what they are doing
• This is good... up to a point!
  • Do we want languages where a PhD* is required to understand the library documentation?

* two PhDs for Haskell

Fancy types make my head hurt

• Complex type systems can lead to complex language definitions
• Easy to blow the overall complexity budget

The notion of a complexity budget ought to be more widely used. In addition to the limitations of designer and implementor effort, there's a limit to how much users will learn about a language. Once the language's complexity reaches this limit, additional features are not very useful, because the users who are supposed to benefit from them don't know about them.

Third, it has a useful interpretation of the relationship between typechecking, contract checking (in the particular form described in the talk), and tests:

• Types ~ General but weak theorems (usually checked statically)
• Contracts ~ General and strong theorems, checked dynamically for particular instances that occur during regular program operation
• Unit tests ~ Specific and strong theorems, checked quasi-statically on particular “interesting instances”

These two dimensions of generality and strength are easy to reuse:

• A dynamic typecheck is specific (because it checks only one case) and weak (because all it proves is that the value has the right type) and checked dynamically.
• The purity of core Haskell is another general and weak theorem — or rather assumption, as it's not checked at all.
• Traditional assertions are specific, of variable strength, and checked dynamically.
• Model checkers prove general strong theorems statically.
• The “typeful” style often used in ML and Haskell, where more distinctions are moved into types, is an attempt to make the typechecker's weak theorems stronger.

The title is not just for provocation. It's also a summary of the talk's apparent thesis. Pierce doesn't say this explicitly in any of the slides, so maybe I'm reading my own conclusion into them, but he seems to be saying: proving theorems about programs is good, but having no choice about which theorems to prove is bad. What if the theorem that's forced on you is hard to prove, or easy to prove but not by the methods the checker knows? What if it's not even true, or shouldn't be true? A typechecker (or any obligatory checker) is “considered harmful” because it chooses the theorems for you, and you can't refuse it when it chooses poorly.

“Well-typed programs don't go wrong.” This slogan for ML-style static typing is infamous, since it's true only under an extraordinarily narrow definition of “go wrong”. This definition is not used for any other purpose, so it's virtually impossible for an innocent listener to arrive at the “correct” interpretation. For propaganda purposes, this is a feature, as it allows the user to make an outrageous claim and then blame its falsity on the audience's ignorance.

The slogan is a little bit justifiable in its original context. Robin Milner introduced it (along with polymorphic type inference) in his 1978 paper A Theory of Type Polymorphism in Programming, as the heading “Well-Typed Expressions Do Not Go Wrong”. The original use refers to a toy language in which the only possible runtime errors are type errors, so the typechecker really does prove the absence of all errors. Well-typed expressions, in that language, can loop forever or run out of memory, but they can't have semantic errors: they can't “go wrong”.

Milner must have known it was misleading, though.

It's not just different languages that distinguish types in different ways. It's pretty common for one implementation of one language to have several type mechanisms serving different purposes. For instance, a typical optimized Lisp will have:

1. Multiple representations of variables (integer, float, and tagged pointer), for efficient unboxed arithmetic
2. Tags distinguishing pointers from fixnums (and sometimes characters, nil, and immediate floats)
3. Dynamically typed objects
4. A sublanguage for describing sets of objects, especially inferred or declared static types.

The first two are not called "type" in Lisp, but they would be in a lower-level language. The last two are both called "type" even though they are quite different things. Perhaps surprisingly, this doesn't cause much confusion in practice.

An ML implementation might have:

1. The same multiple representations of variables
2. The same tagged pointers (they make garbage collection simpler, even if they're not actually used)
3. Dynamically tagged objects, to allow sum types
4. Those famous static types, which are the only one of these mechanisms that's normally called "type" in ML.

The first three mechanisms are basically the same as in Lisp, despite the languages' seemingly opposite approaches to type. Where they differ is in how they describe types - and of course in what static types they allow. I find it particularly amusing that ML sum types use the same mechanism as dynamic type. It's not called that, and it's not used the same way, but ML data is partly dynamically typed.

I missed something in my previous post on the many meanings of type. Despite the profusion of seemingly incompatible senses, there is one that is consistent across languages. In every language I know of, type is the difference between an integer and a string.

Some languages, like Bliss and Forth, have no such distinction. Everyone agrees in calling them untyped. Of course they still handle integers and strings, but the language doesn't know which is which. They're distingushed only by how they're used (hence the alternate name operator-typed).

Most languages do distinguish, of course, but they do it in completely different ways. In each language, the mechanism it uses is called type. And this is where the confusion starts. In each language community, the word type becomes attached to the mechanism that language uses, and then to other uses of that mechanism - even those that have nothing to do with distinguishing integers from strings. Eventually users come to believe their sense is the real one, and that all the others must be bastardizations of it. And if they realize how different the senses are, they are tempted to think that they have nothing in common, and that type means nothing at all.

But all these senses reflect different answers to the same underlying problem. There is a common meaning to type across languages, and it is not any of the languages' senses. It is the ill-defined problem of having multiple types of data in one language: integers, floats, functions, arrays, lists, hashtables, strings.

Chris Smith has a good article on static and dynamic typing. It is clear about the terminological confusion:

I realize that may sound ridiculous; but this theme will recur throughout this article. Dynamic and static type systems are two completely different things, whose goals happen to partially overlap.

It does overstate the confusion is a few places (weak and strong typing do have widely accepted definitions) but in general it's very good until the last third, when it falls into the very trap it warns about: supposing that all type systems have the single goal of proving correctness. That is not a goal of dynamic typing at all, and it's not even a major goal of static typing for most users, because the properties ordinary type systems prove are rarely the ones programmers care about. The main point of static typing, at least for me, is not to prove anything, but to find bugs. I don't care if the type system proves that a particular bug doesn't exist, because that's rarely information I can use. But when it locates a bug - or even suspects one - that is valuable, because it saves time. Proofs may help find bugs by narrowing the search space, but the proofs themselves are not why we use typecheckers. We use them to find bugs faster.

Type is one of the most overloaded words in computer science. It has at least six important senses:

1. The representation of a variable, in low-level languages.
2. The class or constructor of a value, in most dynamically typed languages.
3. Any set of values, in Lisp.
4. A protocol or interface an object implements, in Smalltalk.
5. An intended meaning of values, in static typing.
6. A theorem about a program, in type theory.

Each of these is the one true sense of “type” to some people, and absurd to others, even though the first five are obviously related.

A lot of misunderstandings come from confusion of different senses of “type”. For example, some static typists say “static typechecking eliminates runtime type errors”. If this means “static theorem checking eliminates runtime theorem errors”, it's trivially true. But “runtime type error” usually means a value of the wrong class, and with this interpretation it's blatantly wrong.

My advice is to avoid the word “type” when you want to be understood, unless you know how your audience will interpret it.