Purely algebraic abstractions

Any abstraction expresses something all its instances share. Usually this is semantic: all instances have some common meaning. They represent the same values, or perform the same computation, or support the same operations. When you know a construct is an instance of a certain abstraction, you know something about what it means.

Some abstractions are different. Their instances have no meaning in common, only algebraic properties. These are purely algebraic abstractions. Such an abstraction tells what transformations are valid on its instances' expressions, but says nothing about what they mean.

The classic algebraic abstractions are (of course) those of abstract algebra: groups and rings and fields and such. They abstract the properties necessary for algebraic transformations, and nothing else. If you know that your objects and their operators form a ring, you can manipulate formulae and even prove theorems about them, without knowing anything about what they mean.

In contrast, most abstractions in computing focus on meaning, and express algebraic properties only incidentally. If you have a java.util.Collection or a java.util.Map, you know you can add and remove items, test whether they're there, and iterate over them — but do you know any algebraic properties? Even the most basic properties are broken by unusual collections like caches or Bloom filters. They're semantically legitimate collections, and their algebraic properties are unreliable because they're irrelevant.

(Algebraic abstractions are not entirely reliable either, because most of their computational incarnations don't quite satisfy their axioms. Reflection and other debugging features can often detect differences between supposedly equivalent objects. Limitations of memory and time create edge cases where expressions equivalent in denotation are different in operation. Floating-point arithmetic makes a sport of breaking nearly every algebraic property that could be expected of it. But similar problems afflict nearly all attempts to reason about abstractions; they're not specific to algebraic abstractions, and they don't make them useless. The equivalences generally hold for the properties we care to preserve, so they're correct in practice though not in theory.)

Haskell typeclasses

Most Haskell typeclasses have semantic content: Show and Num are about operations with the same meaning for all their instances; Eq expects algebraic properties (reflexivity and transitivity) but still defines the meaning of ==. There are a small but increasing number of purely algebraic typeclasses: the Prelude has Monoid, Functor, Applicative and Monad, whose instances have nothing in common but algebraic equivalences.

This is why monads are so hard to learn. Each student of Haskell asks what monads mean, and invents a variety of wrong answers (typically semantic generalizations of IO actions), because they're sure that such an important abstraction must be meaningful, and have never heard of algebraic abstraction. Eventually they learn to use monads without asking what they mean, because monads don't mean anything.

This is a sore point among Haskellers. It will get more sore, because Haskell is gaining more algebraic abstractions. Applicative is in the Prelude now!

Haskell Prime numbers

Haskell Prime is a collection of ideas for future versions of Haskell, including a proposal to generalize the numeric typeclasses by removing their semantic content, replacing Num and most of its subclasses with purely algebraic classes:

(+) :: AbelianGroup a ⇒ a → a → a
(*) :: Ring a ⇒ a → a → a
(/) :: DivisionRing a ⇒ a → a → a
mod :: EuclideanDomain a ⇒ a → a → a

(A division ring is like a field except that multiplication is not necessarily commutative.)

This makes the numeric operations maximally general, at the cost of making them meaningless. It also gives mundane code types (and type errors) that make sense to mathematicians and no one else:

factorial :: (Ring a, Ord a) ⇒ a → a
sum :: AbelianGroup a ⇒ [a] → a

(I'm not sure why + is on AbelianGroup instead of something more general like Magma. Maybe it's to comply with users' expectation that + be associative and commutative.)

This proposal brings the straightforward clarity of Monad to arithmetic, an area where Haskell has long suffered from comprehensibility bordering on practicality.

I'm not sure algebraic abstractions are always a bad idea for programming languages, but the difficulty of Monad suggests they're hazardous.

A semantic abstraction tells you what its instances mean. An algebraic abstraction only tells you what transformations preserve that meaning. That's enough for optimization, but not for understanding.

Antedating “datatype” all the way to Plankalkül

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.

Don't abbreviate rare names

Some languages are too consistent about keeping their names short. Arc and Wart call their macro-defining operators mac instead of defmacro or define-macro.

I understand how a designer could see mac as an important operator. If you think of macros as a central, distinctive feature of your language, and if you use quite a few of them to bootstrap your standard library, they feel important enough to deserve a short name.

mac does almost nothing for the length of programs, though. Macro definitions, however fundamental, aren't common enough for it to matter. define-macro is short enough. I prefer defmacro, but only because it follows a naming convention that makes other, more common names shorter; it's not common enough itself to justify an irregularly short name.

Save the aggressive abbreviation for common operations like make-hash-table. Giving that a one-word name (or even {}) makes more difference.

It's a normative theory.

When a theory fails to usefully describe reality, one bad response is to demand that reality stop disobeying it. Cosma Shalizi illustrates:

A: Hey, you over there, the one walking! You're doing it wrong.
B: Excuse me?
A: You're only using two feet! You should keep at least three of your six in contact with the ground at all times.
B: ...
A: Look, it's easily proved that's the optimal way to walk. Otherwise you'd be unstable, and if you were walking past a Dutchman he could kick one of your legs with his clogs and knock you over and then lecture you on how to make pancakes.
B: What? Why a Dutchman?
A: You can't trust the Dutch, they're everywhere! Besides, every time you walk it's really just like running the gauntlet at Schiphol.
B: It is?
A: Don't change the subject! Walking like that you're actually sessile!
B: I don't seem to be rooted in place...
A: It's a technical term. Look, it's very simple, these are all implications of the axioms of the theory of optimal walking and you're breaking them all. I can't get over how immobile you are, walking like that.
B: "Immobile"?
A: Well, you're not walking properly, are you?
B: Your theory seems to assume I have six legs.
A: Yes, exactly!
B: I only have two legs. It doesn't describe what I do at all.
A: It's a normative theory.
B: For something with six legs.
A: Yes.
B: I have two legs. Does your theory have any advice about how to walk on two legs?
A: Could you try crawling on your hands and knees?

Cosma is thinking of Bayesian statistics, but I sometimes feel the same way about type theory.

In both cases the problem is not with the theory, but with the movement that insists that the theory should be used for everything, whether it works or not.

Many happy returns

Some languages can return multiple values from a function, just as they can pass multiple arguments to a function. I used to think this was an important language feature. Functions that return more than one result are common, after all, so every language has a way to express them — by returning structures, or side-effecting reference parameters, or CPS — or, instead of these workarounds, by supporting multiple return values directly. It complicates the language kernel a little, but it makes code cleaner, right?

No, it doesn't. There are several reasons for a function to return multiple values. None of them require direct language support, and for most of them, it's not even helpful.

Secondary values

Some functions return one useful value, plus some secondary values that aren't interesting to most callers. For instance, Common Lisp's two-argument floor returns a quotient and a remainder, but usually you just want the quotient. This is where built-in multiple values shine: they can automatically ignore the extra value, so the common case Just Works, with no effort from either the caller or the multivalued function.

CL-USER> (format nil "π is about ~S" (floor 355 113))
"π is about 3"
CL-USER> (floor 355 113)
3
16

Returning and destructuring a tuple doesn't handle secondary values well. When the caller wants all the values, it's fine (and equivalent to built-in multiple values), but in the more common case where the caller wants only the primary value, it forces them to explicitly extract one component. This can often be done with a convenience function like left (l, r) = l, but it still adds noise.

If your language supports overloading on return type, you can make the function return either the primary value or the structure — whichever the caller wants. This is a rare and difficult feature, though.

Returning secondary values by side effect works surprisingly well. If the caller doesn't want the secondary values, it's no trouble, since the arguments to which to write them can be optional. When the caller does want them, it requires binding a variable, which typically forces the expression into a block, which is occasionally a problem for functional code. It's not very verbose, though:

int floor(int a, int b, int *remainder = NULL);

int remainder;
int quotient = floor(a, b, &remainder);

Now for my favorite: continuation-passing style. It has a bad reputation because it's associated with total CPS transformation, in which every continuation becomes an explicit lambda, which is onerous and unreadable. That is indeed bad. If you pass explicit continuations only where needed, however, it's no worse than other uses of λ.

CPS provides a way to handle secondary values at least as well as built-in multiple values do, but without language support. With no explicit continuation, the function returns the primary value, but if a continuation is provided, it receives all the values:

imaginary-lisp> (floor 355 113)
3
imaginary-lisp> (floor 355 113 (λ (quot rem) rem))
16

Success and failure

Often a secondary value encodes success or failure, as in Common Lisp's gethash, read, or macroexpand-1, or any of the many Go functions that return an error as their second value. This means callers who don't care about errors can simply ignore the extra value, while those who do can still get it.

(multiple-value-bind (val present?) (gethash vars varname)
  (if present? val (error "Unbound variable: ~S" varname)))

file, err := os.Open("/some/path")
if err != nil {
    panic(err)
}

Returning a structure + pattern matching handles this cleanly and safely: you simply return a different structure for each continuation. Usually this is something like Haskell's Maybe or Either:

case (Data.Map.Strict.lookup vars varname) of
  Nothing → error "Unbound variable: ~S" varname
  Just val → val

case foo of
  Left err → error err
  Right x → x

This can be a little verbose, but the verbosity can sometimes be eliminated by operators that automatically propagate the failure case, such as Haskell's various monad operators.

CPS has an even cleaner way to handle this: success and failure are two different continuations, so the function can simply take an optional continuation for handling errors, or two explicit continuations (of which the success continuation is often the identity function):

(slurp filename
  (fn (err) (error "Unable to open ~S: ~S" filename err)))

(gethash vars varname i (fn () (error "Unbound variable")))

This multiple-continuation style is often used in Smalltalk, where it's particularly convenient because of Smalltalk's terse lambdas. Toward Leakage Containment (Julia Lawall and Dan Friedman, 1992) recommended it for Scheme, but got little attention, perhaps because it used the nonsensical name “continuation-constructing style” (and didn't mention it in the title). I call it multi-CPS and find it very convenient — often more so than catching exceptions.

Complex returns

Some functions really do have multiple values to return — sometimes lots of them, like Common Lisp's get-setf-expansion, with five values, or get-decoded-time, with nine. These functions tend to be awkward to use regardless of how you receive the return values, but the least awkward way is to return a structure, because then at least you're not forced to name each result individually. That's why most languages do this for times:

time_t now = time(NULL);
tm *decoded = localtime(&now);
printf("The year is %d.\n", tm.tm_year + 1900);

This is less painful than Common Lisp's multiple-return-value approach, which often forces you to bind more values than you care about:

(multiple-value-bind (sec min hour day month year)
                     (get-decoded-time)
  (format t "The year is ~S.~%" year))

setf expanders are a similarly complex result that ought to be a structure.

(multiple-value-bind (temps forms svars writeform readform)
                     (get-setf-expansion x e)
  ...)

Simpler cases, like partitioning a collection, are adequately handled by tuples (if you have destructuring) or CPS (if you don't).

Why so much trouble?

Expression languages get much of their elegance by encoding dataflow in program structure. Each expression has one parent, and can therefore easily specify what to do with one return value. When there is more than one, there's not enough room in the structure to express what to do with each value, so we have to specify it in some more other way.

I still think multiple return values are important, but I no longer think they require special language support. There are plenty of good alternatives, and improving a language's support for those alternatives (by e.g. optimizing destructuring or λ) is easier than complicating the core semantics, and more likely to be useful for other purposes.

A brief history of “type”

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.

Incorrect optimization in 1963

Floating-point users today are accustomed (or resigned, sometimes) to compilers that make invalid optimizations by assuming all arithmetic is mathematically correct instead of rounding. The situation used to be worse. A 1963 IBM Fortran II manual warns that it did this for integers too:

FORTRAN assumes that mathematically equivalent expressions are computationally equivalent. Hence, a sequence of consecutive multiplications, consecutive divisions, consecutive additions, or consecutive subtractions, not grouped by parentheses will be reordered, if necessary, to minimize the number of storage accesses in the object program.

Although the assumption concerning mathematical and computational equivalence is virtually true for floating point expressions, special care must be taken to indicate the order of fixed point multiplication and division, since fixed point arithmetic in FORTRAN is “greatest integer” arithmetic (i.e., truncated or remainderless). Thus, the expression

5*4/2

which by convention is taken to mean [(5 × 4)/2], is computed in a FORTRAN object program as

((5/2)*4

i.e., it is computed from left to right after permutation of the operands to minimize storage accesses.

The result of a FORTRAN computation in this case would be 8. On the other hand, the result of the expression (5 × 4)/2 is 10. Therefore, to insure accuracy of fixed point multiplication and division, it is suggested that parentheses be inserted into the expression involved.

(Reordering “to minimize the number of storage accesses” is pointless in a constant expression, but apparently the optimizer did it anyway.)

If this reordering can be prevented by redundant parentheses, then parentheses don't only affect parsing; they change semantics by introducing a barrier against algebraic transformations!

Giving parentheses this additional meaning has an unfortunate effect: other optimizations can no longer ignore them. The manual continues by describing one such problem:

One important type of optimization, involving common subexpressions, takes place only if the expression is suitably written. For example, the arithmetic statement

Y = A*B*C + SINF (A*B)

will cause the object program to compute the product A*B twice. An efficient object program would compute the product A*B only once. The statement is correctly written

Y = (A*B) * C + SINF (A*B)

By parenthesizing the common subexpression, A*B will be computed only once in the object program.

In general, when common subexpressions occur within a expression, they should be parenthesized.

There is one case in which it is not necessary to write the parentheses, because FORTRAN will assume them to be present. These are the type discussed in “Hierarchy of operations,” and need not be given. Thus

Y = A*B+C+SINF (A*B)

is, for optimization purposes, as suitable as

Y = (A*B)+C+SINF (A*B)

I'm not sure whether the problem is simply that A*B*C does not contain the subexpression A*B, or that the CSE lifter sees it but can't merge it with (A*B) because they're not equivalent in all contexts.

Optimizers today still have limitations, and still make invalid transformations, but they've become much more subtle!

Errors are not the same as incorrectness

Program checkers, if they are to check objective properties rather than the prejudices of their authors, must ground their judgements in some aspect of programs' behavior. (Or in their maintainers' behavior, but that's much harder to prove anything about.) Usually the property they check is whether the program will have errors at runtime. If it will fail dynamically, then the checker judges it a bad program statically.

This is an obvious premise, and it's the standard justification for all sorts of program checking, but it's not necessarily true, as Andreas Rossberg points out:

Take the following degenerate program for computing travel routes:

ComputeAndDisplayTravelRoute(inputs);
"boo" - 1;

This will throw a type error on the second line, and a tool like Dialyzer would (correctly) diagnose that (it's obviously trivial in this case). However, before this error is raised, the program actually successfully completes its designated job, namely computing a travel route and displaying it to the user. Yet such a program is defined as "invalid". I'm asking why.

Crashing on exit is a fairly common problem. (Games seem particularly prone to this, perhaps because graphics has so much hardware-dependent setup and teardown.) It doesn't usually cause any problem for the user, so it's not a high priority to fix. But the usual standard of program checking considers it unforgiveable.

Programs that produce errors (of any kind, not just type errors) are usually much worse than programs without. But not always. The properties we check are only an approximation to the ones we care about.

If Scheme were like Scheme

Scheme's numbers are not like the rest of its library. They're older, and they're mostly borrowed from other languages (Maclisp and Common Lisp), so they follow those languages' style rather than Scheme's. They're designed more for the convenience of users than of theorists; they have a usefully complete feature set; they have a printed representation; their operations are predefined and polymorphic and have very short names.

What would Scheme be like if numbers followed the same style as the rest of the language?

It would be necessary to import a library before using any numbers.

(import (scheme numbers))

Numeric constants would be provided as functions returning the constant, apparently because the section of R^NRS they appear in is called “Standard Procedures”. Only the most basic constants would be provided; pi would not be among them.

(define (exact-rational-zero)
  (make-exact-rational (exact-integer-zero) (exact-integer-one)))

Numbers would have no printed representation. Creating them would require explicit constructor calls.

There would be no polymorphism. Most operations would include a type in their name.

(define (factorial n)
  (if (exact-integer<=? n (exact-integer-one))
    (exact-integer-one)
    (exact-integer-multiply! (factorial (exact-integer-subtract n (exact-integer-one))) n)))

The distinction between exact and inexact numbers would still be supposedly “orthogonal to the dimension of type”. But the lack of polymorphism would make it even more obvious that in practice exactness was simply one of the type distinctions: that between floats and everything else.

Floating-point numbers would be called “inexact rationals”. Their constructor would take a numerator and denominator, just like exact rationals; their floating-point representation would be considered an implementation detail. Various details of the specification would be inconsistent with IEEE floating point.

NaN would not be a number, of course. inf.0 and -inf.0 would be exact transfinite numbers, not inexact rationals. There would be no negative zero.

Names would be descriptive, like inexact-rational-square-root and exact-integer-greatest-common-divisor.

There would be exact-integer->list and list->exact-integer operations to convert to and from lists of digits (in arbitrary bases). Converting the lists into strings would be up to you. Converting anything other than exact integers to strings would also be up to you.

Numbers would be portably mutable. Some operations would have destructive versions. (If we did this exercise on Python, some would have only destructive versions.) Racket would omit these, supposedly to make optimization easier, but would have separate mutable numbers for programs that need them.

Operations more obscure than exponent would be left to SRFIs. Users would be able to choose between the widely supported SRFI and the complete SRFI.

exact-integer-divide would not be provided, on the grounds that it's not defined for all integers, and can't be implemented efficiently without special hardware.

There would be a portable way to use exact integers as indexes into lists, but not into vectors or strings. This would be remedied in R⁷RS.

Some implementations would support surprisingly obscure and practical floating-point operations, while omitting basic operations their authors never needed.

(define (numerically-stable? thunk tolerance)
  "Run a floating-point computation with various rounding modes to see
if this significantly changes the result. This is not a reliable test
of numeric stability, but it's an easy way to find bugs."
  (let ((down (call-with-rounding-mode round-down thunk))
        (up (call-with-rounding-mode round-up thunk))
        (nearest (call-with-rounding-mode round-to-nearest thunk))
        (zero (call-with-rounding-mode round-to-zero thunk))
        (roughly-equal? (lambda (a b)
                         (inexact-rational<=?
                          (inexact-rational-absolute-value
                           (inexact-rational-subtract a b))
                          tolerance)))))
    (and (roughly-equal? down up)
         (roughly-equal? down nearest)
         (roughly-equal? down zero)
         (roughly-equal? up nearest)
         (roughly-equal? up zero)
         (roughly-equal? nearest zero)))

There would be debates about whether eq? should “work” on numbers. This would really be about whether numeric operations should always return fresh numbers, and whether the compiler would be allowed to copy them, but no one would mention these merely implementational issues.

eqv? and equal? would compare numbers, even immutable ones, by identity. Hashtables would — OK, standard Scheme doesn't have hashtables. But if it did, the default hash function would hash numbers by identity, not by value.

Arithmetic overflow would still be “a violation of an implementation restriction”. There would still be no way to find out how large a number could safely be.

There would still be no bitwise operations on integers. Schemers who understood the purpose would advise using an implementation that supports bitvectors instead of abusing numbers. Those who did not would say they're easy to implement.

(define two (exact-integer-add (exact-integer-one) (exact-integer-one)))
(define (exact-integer-bitwise-and a b)
  (list->exact-integer (map exact-integer-minimum
                            (exact-integer->list a two)
                            (exact-integer->list b two))))

Complex numbers would, mercifully, be left to a SRFI. The SRFI number would be real, but in most implementations complex-number support would be purely imaginary.

All the comparison predicates would end in ?.

Edit: Replaced some stray uses of <= and + and min with their counterfactual-Scheme equivalents.

In the HN comments, cousin_it says:

We can see similar examples in other languages, e.g. C++ strings are "like C++" and a pain to use, while Java strings are "not like Java" and a pleasure to use. Maybe language design really isn't about general-purpose elegance, but about finding good special-purpose solutions.

Or about using the good general-purpose solutions you already have.

Parentheses are more annoying in infix

There's a lot of code in functional languages written with a C or Java accent. The reverse is much rarer, but I have seen some: C++ written with a Lisp accent.

I didn't like it.

I didn't like the fooP convention for predicates. I didn't like the large multi-line expressions. And I especially didn't like the redundant parentheses.

What? A lisper doesn't like parentheses?

Parens are not high on the list of things that bother me in Lisp. They're only a little verbose, only a little distracting, only a little trouble to match. Large expressions don't bother me either; they're clearer than the alternative. And I like foo-p, because it's short and pronounceable.

Was I just objecting to C++ that didn't look like C++? Was I offended by contact between pretty Lisp and icky C++?

For fooP, that's probably the whole of it. It's camelCase instead of hyphenated, so it looks wrong as Lisp, and it's not standard C++ style, so it looks wrong as C++. And I'd rather not have to explain to other C++ programmers why I'm using a convention from some weird academic language. But I don't have a substantive objection.

For the other two features, I do.

Large expressions in prefix notation are easy to parse. The root operator is plainly visible at the beginning, and indentation goes a long way toward making the structure clear. Large expressions in infix are not so easy. The root operator is buried somewhere in the middle, and one must parse much of the expression to find it. There's no easy way to indent infix expressions, so breaking an expression across multiple lines doesn't alleviate much of the parsing load. This is why programmers in infix languages usually prefer to break such expressions into multiple statements.

Parentheses in Lisp are consistent: they all delimit lists, and almost all delimit forms. The semantics of the forms may be arbitrarily variable, but those of the parens are always the same. In C++, however, parentheses have several different meanings. They sometimes override precedence, sometimes call (or declare) functions, sometimes do typecasts, and sometimes delimit conditions in control structures. So a nest of parentheses in C++ is much more ambiguous than in Lisp, and it takes more parsing effort to determine which ones are which.

This goes some way toward explaining why so many programmers are suspicious of Lisp's syntax. Large expressions and nests of parentheses are suspicious in infix languages, and this suspicion does not instantly vanish in a new language.

Effects vs. side effects

Commonly used terms get abbreviated. Thus functional programmers often say “effect” instead of “side effect”. I approve of this usage – not only because it's shorter, but because it frees up “side effect” for another concept. This is something assembly language programmers know, and have known for decades, that other programmers seldom speak of.

Most machines have no notion of a return value; the only way for parts of a program to communicate is by mutating registers. So assembly language programs must do all their communication by effect. This means they distinguish between different kinds of effect. In particular, they distinguish effects that are part of a routine's contract from those that, however consistent, are not intentional: side effects.

Consider this implementation of factorial on a typical register machine:

;The factorial function, iteratively
;args: r1 = n
;results: r2 = n!
;All other registers are preserved.
factorial:
  li r2, 1
loop:
  cmpi r1, 1
  ble done
  mul r2, r2, r1
  sub r1, r1, 1
  b loop
done:
  ret

This function leaves its result in r2, but also happens to set r1 to 1. This is a side effect: an effect not in the routine's contract. It is, of course, a bad idea to rely on these, but by accident or desperation, assembly programmers occasionally do, which is why they have a name for them.

(Recursive factorial is more complex than iterative on most machines – often absurdly so, if you strictly follow an ABI that wants you to save registers and construct stack frames. This is one of the reasons programmers accustomed to low-level languages don't take readily to recursion. To them, it looks unnecessarily complex, because it is complex in implementation. High-level languages hide this complexity, but low-level programmers know it's still there.)

It's not normal for programs in higher-level languages to have side effects in this sense, because they have fewer ways to accidentally have effects. Supposedly unobservable effects like preloading caches are common (and are occasionally relied on), but typically any observable effect that isn't part of the interface is a bug. So this concept is less useful in higher-level languages. The more general concept of relying on unspecified behaviour remains useful, though, and it's quite familiar from discussions of language specs.

Functional programming advocacy suffers from a focus on purity, where state is considered a sin to be avoided absolutely. One way the movement might make progress is to distinguish between different kinds of effects, so they could say which ones are deadly and which are venial, rather than treating all effects as indistinguishable evil. Vocabulary analogous to the assembly language programmers' “side effect” might help with this.

Customary semantics

What is the real, definitive semantics of a language? There are three standard answers:

1. The natural-language specification, because it's the one the designers understand.
2. The reference implementation, because it's unambiguous and well-tested.
3. The formal semantics (of whichever flavor), because it avoids implementation concerns, so it's simpler than a real implementation. (Or because it's difficult and therefore “rigorous”.)

There's a controversial fourth option: the definitive semantics of a language is the behavior that is consistent across all conventional implementations.

This approach has some virtues:

• It identifies the behavior you can rely on. Implementations have bugs and deliberate deviations from the spec, where you can't rely on the specified behaviour. They also have widely supported extensions which you can rely on, even though they're not in the spec.
• Unlike any other means of defining semantics, implementations are heavily tested. Formal semantics can be tested by turning them into implementations, but seldom are; natural-language specifications aren't mechanically tested at all.
• It's reconstructable. Users can always find out what their implementations do, even when the spec is not publicly available, or is difficult to read. (Most specs are.) Sometimes this shows them implementation-dependendent behavior, but by comparing implementations they can discover the customary semantics.

Deferring to custom is unpopular among language designers and theorists. We see it as an ill-defined, unstable foundation about which nothing can be known with confidence, and on which nothing can be built reliably. We remember the chaos that engulfed HTML and CSS and Javascript when their users treated buggy implementations as specs, and we don't want it to happen again. We want our semantic questions to have authoritative answers, and mere custom does not provide that.

But it's the de facto standard among users of languages. Most programmers are not language lawyers, and can't readily figure out whether the spec says their code will work. But they can easily try it and see what happens.

We can tell users not to do this. We can tell them to avoid empiricism, to seek authority rather than evidence, to shut their lying eyes and trust in doctrine. This is not good advice in most areas, not even in other areas of programming, nor for semantics of other languages natural or artificial. Is it really good advice for programming languages?

Whether it's good advice or bad, users don't listen. Their models are based on the behaviour they observe. As a result, many popular “myths” about languages — that is, widely held beliefs that are officially supposed to be false — are true in the customary semantics. For example, here are some parts of C's customary semantics that are not part of the formal specification. Some of them are violated on unusual architectures, but most C users have never written for such an architecture, so custom doesn't care.

• Signed integers are represented in two's complement. (Rumor has it this is not quite always true.)
• Signed integer overflow is modulo word size, like unsigned.
• All pointer types have the same representation: an integer.
• NULL is represented as 0.
• Memory is flat: it's all accessible by pointer arithmetic from any pointer.
• Pointer arithmetic is always defined, even outside array bounds. Overflow is modulo word size, just like integers.
• Dereferencing an invalid pointer, such as NULL or an out-of-bounds pointer, blindly tries to use the address.
• Compilers generate native code. The built-in operators compile to machine instructions.
• char is exactly eight bits wide.
• Characters are represented in a superset of ASCII.

(I thought sizeof(char) == 1 was only in the customary semantics, but it's actually in the spec.)

Much of the furor over optimizations that exploit undefined behaviour is because they're invalid in the customary semantics. Some C compiler maintainers have come to believe that the spec is the whole of the contract between compilers and users, and thus that users don't care about semantics not defined therein. It's a convenient belief, since it permits optimizations that would otherwise be impossible, but it's wildly at odds with what their users want. This isn't the only problem with these optimizations — they make for perverse error behaviour under any semantics — but this is why users tend to see them as not merely bad but incorrect.

Language lawyers, especially those who write specs, should take customary semantics more seriously, so they don't contradict the semantics in actual use.

Why is breadth-first numbering hard?

John Launchbury gave Chris Okasaki an annoying puzzle:

Given a tree T, create a new tree of the same shape, but with the values at the nodes replaced by the numbers 1 .. |T| in breadth-first order.

Go ahead and solve it. I'll wait.

If you want to solve it functionally, I'll wait longer.

Chris posed this puzzle to many functional programmers, and found that they had a surprisingly hard time with it. They took a long time to solve it, and their solutions were seldom elegant. He came up with various hypotheses as to why: did the programmers not know breadth-first traversal or queues? Did they prematurely commit to lists or pattern matching? He didn't seem to find any of them convincing. Neither do I.

One hypothesis he didn't mention is that most functional programmers see a recursive data structure and immediately try to process it by straighforward structural recursion, with a call tree isomorphic to the data structure. When you have many tools, and you encounter a nail, you reach for your hammer, right? But in this case structural recursion is the wrong tool, and it takes a while for programmers to backtrack far enough to notice.

It may take even longer for them to identify the right tool. Queues, like hashtables, are a little awkward for functional programmers, because their most natural implementations are stateful, as are many of their applications. They're almost always used linearly (i.e. there's only one version of the queue at a time), so eschewing state buys no useful flexibility, and incurs the extra hassle of explicitly passing the updated queue around. It also prevents using the efficient circular-buffer representation, just as it usually prevents using hashtables.

They're also a little awkward to use in functional languages, because none of the most familiar and widely implemented functional data structures (lists, tree dictionaries, tree sets, tries) is easily used as a queue, so would-be queue users must look up a queue library, or build one, or use pairs of lists (if they know this trick), or use some inappropriate data structure, or give up and use some other algorithm. Which is what most of Chris's subjects did.

Meanwhile, Java users use its ordinary LinkedList class (which is a doubly-linked list, and thus a reasonably efficient deque) to win contests without having to worry about any of this. Can your functional language do as well?

“Persistent” is older than I thought

“Persistent” usually refers to data that persists across multiple executions of a program. But in the last few years I've occasionally heard it used, especially in the Clojure community, for data structures that are updated nondestructively. (The old version persists after the update — get it?)

I saw this as a newfangled sloppy usage, but it ain't so. Like many seemingly new usages, it's surprisingly old. It dates back at least to 1985, when it appears prominently in Sarnak & Tarjan's Planar Point Location Using Persistent Search Trees. It was popularized a few years later by the same authors plus two others in Making Data Structures Persistent, and Tarjan has used it many times since then.

The more common sense — data that persists across program executions — is not much older. The earliest uses I've found are from several papers in 1976. Earlier ones are about either persistence of phosphors (an important issue for CRTs) or fault-tolerance by persistently retrying. It apparently caught on quickly, at least in the database community, because Jim Gray's 1977 Notes on Data Base Operating Systems takes it as standard enough to use without bothering to define it.

So it's reasonable to object to “persistent”=“nondestructive” because it conflicts with a more important concept, but not because it's new.

Maybe now someone will tell me it's in some very standard source like Knuth and I never noticed...

A sound bug finder is an unsound correctness prover

This account of Coverity, a commercial bug-finding tool for C and C++, illustrates a peculiar attitude common in the program-checking field:

we were also unsound. Our product did not verify the absence of errors but rather tried to find as many of them as possible. Unsoundness let us focus on handling the easiest cases first, scaling up as it proved useful. We could ignore code constructs that led to high rates of false-error messages (false positives) or analysis complexity, in the extreme skipping problematic code entirely (such as assembly statements, functions, or even entire files). Circa 2000, unsoundness was controversial in the research community, though it has since become almost a de facto tool bias for commercial products and many research projects.

Most program checkers prove theorems about programs. In particular, most aim to prove programs correct in some respect (e.g. type safety). A theorem prover is sound iff all the theorems it proves are true. So a correctness-prover that claims a buggy program is correct is unsound, but one that rejects a correct program is not. People in the program-checking field are accustomed to this, so they habitually think soundness = proving the absence of bugs.

But a bug-finder doesn't aim to prove correctness. Instead, it aims to prove incorrectness: to prove the presence of bugs. It's sound iff all the bugs it reports are real bugs — that is, if it has no false positives. False negatives (overlooking bugs) are OK, because they don't make its claims incorrect.

Unfortunately, most interesting properties are undecidable, so a checker can't be sound at both bug-finding and correctness-proving, unless its claims are very weak.

So Coverity did the right thing, in theory as well as practice, when they focused on suppressing false positives. Their bug finder was unsound, but it was unsound because it reported spurious errors, not because it missed some real bugs.

Addendum: bug finders in languages

The most visible bug finders (especially in academia) are those, like the ML typechecker, that try to prove something about the program, and report a bug if they fail. These are unsound as bug finders, since they sometimes report nonexistent bugs. Unfortunately, bug finding is their main use, so their standard of soundness does not fit.

This is particularly problematic for checkers that are built in to a compiler, and don't just complain but prevent programs from running. (This is part of why they're so visible — if the checker makes mistakes you can't ignore, you have to be aware of it.) It's hard (especially in theory) to justify a compiler that rejects correct programs. Sound bugfinders don't have this problem.

Why Lambda the Ultimate doesn't make me feel stupid

This search term appeared in my referer logs a few years ago: “lambda the ultimate makes me feel stupid”.

I used to feel that way — at least, I felt ignorant and despised. The denizens of LtU know an intimidating amount of theory, and some are quick to scorn anyone who doesn't, and demand that they read heaps of literature (often of dubious quality or relevance) before being permitted to talk. Not having read most of that literature, I accepted their evaluation, and felt ignorant.

But then battles of the War of Types erupted there, and λ the Ultimate became λ_T the Ultimate, or even System F the Ultimate. Anyone who dared suggest that dynamic typing was a reasonable basis for a language, or even a meaningful concept, faced voluminous condescension and condemnation. The seemingly knowledgeable scholars appeared to neither know nor care about the fundamental concepts of their field, and treated its greatest successes with learnèd disdain.

I do respect very much the elephant, and if your work dismisses him as an ill-formed dinosaur, it is not zoology.

(I don't think the dynamic typists gave a good account of themselves either; there was lots of handwaving about flexibility and little mention of the importance of simple semantics. But I found them less offensive, not only because I agree with them, but because they didn't demand the anathematization of the other side, nor of the object of study.)

The War of Types subsided, and LtU became once more a place of academic quiet, disturbed only by announcements of new PL papers. It still makes me feel ignorant at times, but it no longer makes me feel stupid. Sometimes it even makes me feel wise. Which is a much more dangerous emotion. When I feel stupid or ignorant, I study to become less so, but when I feel wise, I do nothing.

Exceptions are (mostly) for humans

Most languages have a way to signal a generic error with a string as the error message. This makes it easy to include relevant information in the description of the error: something as simple as (error "serve-ice-cream: quantity=~S must be positive" q) provides a human-readable description with whatever information you think is relevant. It's not machine-readable, but most errors don't need to be handled mechanically, so this is not usually a problem.

Languages with exception systems also allow signalling errors in a machine-recognizable way, typically by defining a new exception class. This is often considered the “proper” way to signal errors, but it's more work than a generic error, so it's typically done only for polished public interfaces. Errors that aren't exposed in such an interface (or aren't intended to be exposed — errors are a kind of implementation detail that's hard to hide) generally make do with strings.

When you do create an exception class, it's also more work to include relevant information in the exception. Typically you have to define slots, arrange for them to get the appropriate values, and then embed them in the error message. This requires changing several parts of the definition as well as the call site, so it's enough trouble that you often won't do it. Error reporting code is seldom high on the priority list until the error happens.

I ran into this problem a while ago, in a utility function which reported a rare error by throwing a C++ exception class like this:

class negative_error : public domain_error {
public:
    not_integer_exn() : domain_error("value must not be negative") {}
};

This was fine until the error finally happened. A high-level catch-almost-anything handler caught the exception and displayed the error message, which told me almost nothing about the problem. Since this was C++ and not running under a debugger, there was no automatic stack trace, and no hint of what value was negative, or who cared, or why. If I had been lazy and signaled the error with throw domain_error("serve_ice_cream: quantity=" + to_string(q) + " must not be negative"), the relevant information would have been in the string, but because I had done it the “right” way, it was not.

(The designers of C++ are aware of this problem. That's why all the standard exceptions take strings. negative_error should have too.)

In an ideal exception system, convenience and machine-readability would not conflict. It should be easy to signal an an-hoc error with a human-readable message and machine-recognizable fields. It might help to allow throwing exceptions without declaring them first, e.g. (throw '(negative-error domain-error) :quantity q "value must not be negative"). (Wasn't this allowed in some early exception systems?) But if it's only easy to have one of the two, choose the convenient human-readable form. That's the one you'll use.

What happened to “manifest” and “latent”?

Chris Strachey has remarkably influential lecture notes. His 1967 Fundamental Concepts in Programming Languages introduced or popularized a lot of now-standard terminology: r-value and l-value, first-class, polymorphism (ad-hoc and parametric), and maybe parametric type.

It also introduced some terms which didn't catch on, among them manifest and latent:

We call attributes which can be determined at compile time in this way manifest; attributes that can only be determined by running the program are known as latent.

These are the concepts now called “static” and “dynamic”. I'm not sure why Strachey bothered to introduce his own words for them, since the standard ones already existed, and he was evidently more comfortable with them — when he discusses types on the same page, he consistently uses “dynamic”, not “latent”. (Was “dynamic typing” already a standard term by 1967?) Maybe he reserved “static” and “dynamic” for behaviour, and wanted different words for the time when a property could be determined.

He acknowledges that the boundary between static and dynamic is fuzzy, and explains why it's useful anyway:

The distinction between manifest and latent properties is not very clear cut and depends to a certain extent on questions of taste. Do we, for example, take the value of 2 + 3 to be manifest or latent? There may well be a useful and precise definition—on the other hand there may not. In either case at present we are less interested in the demarkation problem than in properties which are clearly on one side or other of the boundary.

I wish more academics dared to do that.

Neither “manifest” nor “latent” caught on, and they might have been forgotten like most new coinages — but decades later, both have been resurrected with new meanings in connection with type. “Manifest typing” now refers to languages that require type declarations — an important concept that lacked a short name. “Manifest” is readily reinterpretable as “appearing in source”, and while it might confuse people who remember the old sense, we are few. Less usefully, “latent typing” serves as a euphemism for “dynamic typing” among type-theory partisans (bizarrely, as the word they object to is “type”, not “dynamic”, but at least it avoids using the terminology of the savages). In neither case does Strachey's original meaning survive; if you speak of some property other than type as “manifest” or “latent”, most proglang researchers will not understand.

Where do closures come from?

Common Lisp's function form is usually described as a device for switching between namespaces: it evaluates its argument in the “function” namespace instead of the normal “variable” namespace.

Older sources have a completely different idea: they say function makes closures. The Hyperspec says:

If name is a lambda expression, then a lexical closure is returned.

and

function creates a closure of the lambda expression

Both of these lines were inherited from CLtL, so this is not a new interpretation, nor one incompatible with the best of knowledge. What's going on?

To begin with, these two interpretations of function aren't observably different in portable Common Lisp. The only portable way to get a closure is by (function (lambda ...)) or by macros like defun that might expand to it. ((lambda ...) expands to (function (lambda ...)), because unlike all other special forms, lambda is in the function namespace, but that's just a historical quirk.) The only way to use lambda without function is ((lambda ...) ...), which has the same semantics regardless of whether it makes a closure. So portable code can't tell the difference.

Implementation-specific extensions can. If compile is extended to non-null lexical environments, it will make closures out of lambda-expressions without any help from function. Or if there's a named-lambda form that makes closures, it's unnecessarily complex to attribute the closure in (function (lambda ...)) to function.

So Common Lisp culture favors the simpler interpretation: lambda makes closures, and function is a mere namespacing operator.

Like so many oddities of CL, the old interpretation comes from Lisp Machine Lisp. The 1984 Lisp Machine Manual introduces function by saying it “has two distinct, though related, meanings.” The first is to get a symbol's function definition, and the second is to make a closure:

(let (a)
  (mapcar (function (lambda (x) (push x a))) l))

passes mapcar a specially designed closure made from the function represented by (lambda (x) (push x a)). When mapcar calls this closure, the lexical environment of the function form is put again into effect, and the a in (push x a) refers properly to the binding made by this let.

These two meanings were reflected in implementations. Guy Steele's reference interpreter (in the CL mailing list archive) doesn't bother to make a closure for ((lambda ...) ...), only for (function (lambda ...)). But when optimizing compilers became the norm, it no longer seemed silly (or inefficient) for lambda to always make a closure, so reinterpreting function as a namespacing operator made sense.

Surprisingly, this is not the first time function has been reinterpreted. The Pitmanual says Maclisp's function didn't make closures — it took a different form, *function, to even partially do that. function was equivalent to quote, except that in compiled code it would make a compiled function instead of just a lambda-expression — it permitted compilation but didn't change scoping. When Lisp Machine Lisp changed it to make closures, that was largely backward compatible, since most lambdas were intended to use lexical scope anyway. (I'm not sure when compilers started to use lexical scope — was that in Maclisp?)

I don't think any other language construct has had so many unrelated meanings over the years, let alone done so while preserving the meaning of existing code. function was originally a hint to the compiler, then a way to make closures, and then a namespacing operator. Its history probably ends there, since most new lisps eschew multiple namespaces and omit function rather than repurpose it, but three unrelated meanings is impressive.

Trivial program checkers

Typecheckers get (and deserve) a lot of attention for their ability to find bugs, but their success leads people to think typechecking is the only way to check programs. It's not. There are useful program checkers much simpler than any typechecker. Here's an example:

grep scanf

This finds real bugs in real programs — and not just ordinary bugs, but security holes due to %s overflowing buffers.

Here's another checker:

grep 'printf[^"]*$'

This finds printfs that don't have a literal string on the same line, which usually means someone forgot the format string and did this:

fprintf(file, somestr);

...instead of this:

fprintf(file, "%s", somestr);

It's a stupid bug, yes, but not a rare one. I once ran this checker on a large application and found dozens of instances of this bug. I also found dozens of false positives, from things like these:

snprintf(somewhere->buffer, MAX_BUFFER,
         "format string", args);
fprintf(file, message_format_strings[status], description);

But they were obvious false positives, so it was easy to ignore them.

Here's an even less selective checker:

grep '(\w\+ \?\*)'  #beware different versions of grep

This finds pointer typecasts, which (in C++, more than in C) are often misguided — they might indicate unsafe downcasts, or non-type-safe containers, or casting away constness, or simple unnecessary casting. It also finds a great many false positives, of course — mostly function prototypes and innocent casts.

These checkers don't prove the absence of the errors they look for. A program that doesn't contain the string scanf might still call it via a library or by dlsym. The printf checker can be defeated by something as simple as a printf-like function whose name doesn't contain printf — hardly a rare occurrence! The cast checker misses mundane things like (char**) and (IntPtr). They only find bugs; they don't guarantee their absence.

They're also not very powerful. They find only certain specific errors, not a wide variety. A real lint program can do much better.

But when you don't have a real lint handy, or when your lint doesn't find the problem you're worried about, simple textual checkers can be valuable.

“They only find bugs”. “Only certain specific errors”. Faint criticism.

In addition to being useful, these checkers are a reminder that there are many ways to check programs. None of them are typecheckers in either sense — not in the common sense, because they don't check datatypes, and not in the type-theory sense, because they don't classify expressions. They aren't even aware of the existence of expressions — they see code only as text. This is not a very powerful approach, but it's enough to find a lot of bugs.

Not all checkers are typecheckers.