What is higher-order in higher-order abstract syntax?

Question

I understand that using higher-order abstract syntax essentially means using host (meta) language abstraction facilities to represent binders in embedded (object) language. But, Why exactly is it higher-order? Why is traditional abstract syntax called first-order abstract syntax?

I read the paper (Frank Pfenning, and Conal Elliott, Higher-Order Abstract Syntax, PLDI'88) that introduced HOAS as we use today. I could not quite understand the following paragraph ($\S$ 3.2) that describes encoding in HOAS:

In this first generalization, simply typed lambda terms represent programs. .. . The lexical terminals and the operators that do not introduce variable bindings are, respectively, first-order and second-order constants of the $\lambda$-calculus. Another crucial change occurs for the variables. Operators in the object language that are binding constructs are now explicitly encoded as third-order constants. As the following examples will show, this requires that bound object language variables actually become variables in the typed lambda calculus.

Particularly, I am not convinced why encodings for binding-introducing constructs like let (shown in Figure 1 of the paper) are considered third-order.

Answer 1

Re: "why encodings for binding-introducing constructs are considered third-order", the conventions are a bit arbitrary, and I've usually heard these encodings described as "second-order". For example, although in these notes by Gilles Dowek, the order $o(T)$ of a simple type $T$ (Definition 2.3) is defined as

\begin{align} o(p) &= 1 \tag{$p$ atomic} \\ o(S \to T) &= \max(1+o(S),o(T)) \end{align}

on the other hand in these notes by Herman Geuvers, the order $h(T)$ of a simple type $T$ (Definition 22/Exercise 7) is defined as

\begin{align} h(p) &= 0 \tag{$p$ atomic} \\ h(S \to T) &= \max(1+h(S),h(T)) \end{align}

I'm not sure why Pfenning & Elliott chose the 1-indexed numbering scheme, but I suppose it might be the influence of the literature on higher-order matching/unification.

Answer 2

You can think of $\lambda$-abstraction as an operator $\Lambda$ which takes a function from terms to terms into a term: $$\Lambda : (\mathsf{Term} \to \mathsf{Term}) \to \mathsf{Term}.$$ The type of $\Lambda$ is higher-order because it maps functions to objects, so it is a functional of rank 2. This is where the name comes from.

For example, if $\mathsf{id}$ is the identity map then $\Lambda(\mathsf{id})$ is the term $\lambda x . x$.

Constructors, for example $\mathsf{succ}$ as a constructor for the type of natural numbers, can naturally be viewed as first-order because they take terms to terms.

Of course, for the above to make sense, we need to be able to speak about functions between terms at the meta-level. And there are various subtleties: in principle one can have weird functions between terms that do not correspond to anything that can be written down in the syntax (consider a non-computable map). So if you're not careful, you're going to end up with "exotic terms" $\Lambda(f)$ that create a lot of trouble.

The usual solution is to somehow limit $\mathsf{Term} \to \mathsf{Term}$ to only "nice" functions. One possibility is PHOAS, another is to use a meta-theory such as Logical Frameworks in which only nice functions exist.