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.