What’s higher-order about so-called higher-order references?

A reviewer, in one of those off-hand little low-level comments they leave, which one is sometimes tempted to ignore as one works on a revision because they’re not strictly actionable, has absolutely nerd-sniped me.

What does “higher-order” in “higher-order references” mean? (References as in Reynolds 1970.)

We appear to have inherited the phrase “higher-order” from higher-order logic, which it refers to the union of first-order logic, and second-order logic, and third-order logic, and so on. Here, “order” refers to what quantifiers can quantify over. For example, zeroth-order logic has no quantifiers. First-order logic can quantify individuals. Second-order logic can quantify over things that quantify over individuals (sets). Etc.

So what is a higher-order function? Well, a function that can quantify over functions that can quantify over functions, etc. Really, we could perhaps generalize to higher-order values to make a closer analogy to higher-order logic. A zeroth-order value cannot quantify over other values—values such as naturals and booleans. These are sometimes called ground values. A function cannot be a zeroth-order value, since it quantifies over other values. A first-order value can quantify over zeroth-order values. A fairly restricted function would be a first-order value. A second-order value could quantify over values that quantify over values, so for example a function of type (A -> B) -> C, where A, B, and C are ground values, would be second order.

So far all this makes sense.

What is a higher-order reference?

Well… that is a surprisingly complicated question.

Of late, “higher-order reference” seems to mean “reference to a higher-order, effectful function”. The phrase appears in this sense at least as early as 1998 (Abramsky et al.), in which Abramsky et al. use “higher-order reference” to refer to references that contain higher-order functions that can, when called, modify the heap. But this use of “higher-order” is at odds with most other uses of “higher-order”. It’s not used to mean that the reference merely quantifies over other references. Instead, it’s used to mean references that quantify over higher-order, effectful functions, a different class of values. That is, this use of “higher-order” refers not to the order of the reference, but the order of the values the reference contains. If we were to use “higher-order reference” more consistently with “higher-order logic”, it should mean references to references to references etc. to values.

The phrase “general references” avoids the problem, but does not solve it. This phrase is often used, including by op. cit., to include other forms of higher quantification in references, such as cyclic references and references to existential types, etc., as well as references to higher-order, effectful functions. To quote:

By general references we mean references which can store not only values of ground types (integers, booleans, etc.) but also those of higher types (procedures, higher-order functions, or references themselves).

Ahmed (2004) uses similar phrasing:

general references — that is, mutable cells that can hold values of any closed type including other references, functions, recursive types, and impredicative quantified types.

The emphasis is on their generality, which distracts from a key semantic issues (higher-order, effectful functions in particular are responsible for interesting semantics questions).

The situation is worse if we look at the phrase “first-order references”, which also appears in Abramsky et al.. This appears to refer to references to ground values, i.e., references to zeroth-order values. So a first-order reference is indeed a first-order value, in that it quantifies over zeroth-order values. But that means “first-order” in “first-order reference” is used in a difference sense than “higher-order” in “higher-order references”: it refers to the order of quantification of the reference itself, and not to the order of the quantification of the contents of the reference.

Even more frustratingly, it seems the phrase “higher-order reference” used to use “higher-order” in the original sense. Janssen et al. (1977) use “higher order reference” to refer to references that quantify over references! Readings over some of the related papers around that time, it seems the semantics of such references were quite interesting. It’s unclear to me when exactly the phrase took on the new sense of “higher-order”.

So how do I concisely, and pedantically, refer to those references that can contain higher-order (effectful) functions (but not necessarily other non-first-order values)? My student Sean Bocirnea proposed “higher-order value references” (HOVR; pronounced “hoover”). Perhaps we’d use “higher-order function reference” (HOFR; “hoofer”) to speak of those only required to contain higher-order functions. These are less verbose than any alterantive I’ve come up with, but have bad mouth-feel.

Given the phrase has had a new sense for at least almost 30-years old at this point, I’m a a little reluctant to be inventing new phrases. Perhaps I should just leave it at this, with this note serving as a historical marker of this accident of language. But I’m also insufferably pedantic, and the phrase does have two meanings, so perhaps I should create a new phrase.