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.


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.


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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.